{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T10:24:22Z","timestamp":1779099862524,"version":"3.51.4"},"reference-count":36,"publisher":"IEEE","license":[{"start":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T00:00:00Z","timestamp":1622505600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-009"},{"start":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T00:00:00Z","timestamp":1622505600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-001"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,6]]},"DOI":"10.1109\/csf51468.2021.00006","type":"proceedings-article","created":{"date-parts":[[2021,8,10]],"date-time":"2021-08-10T20:47:26Z","timestamp":1628628446000},"page":"1-16","source":"Crossref","is-referenced-by-count":6,"title":["Performing Security Proofs of Stateful Protocols"],"prefix":"10.1109","author":[{"given":"Andreas V.","family":"Hess","sequence":"first","affiliation":[{"name":"Technical University of Denmark,DTU Compute,Lyngby,Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"M\u00f6dersheim","sequence":"additional","affiliation":[{"name":"Technical University of Denmark,DTU Compute,Lyngby,Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Achim D.","family":"Brucker","sequence":"additional","affiliation":[{"name":"University of Exeter,Department of Computer Science,Exeter,United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anders","family":"Schlichtkrull","sequence":"additional","affiliation":[{"name":"Aalborg University,Department of Computer Science,Copenhagen,Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_41"},{"key":"ref13","first-page":"185","article-title":"Set-?: Set membership ?-calculus","author":"bruni","year":"2015","journal-title":"Computer Security Foundations Symposium"},{"key":"ref34","first-page":"1","article-title":"Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers","author":"paulson","year":"2010","journal-title":"8th International Workshop on the Implementation of Logics"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00034"},{"key":"ref15","article-title":"Automated stateful protocol verification","author":"hess","year":"2020","journal-title":"Archive of Formal Proofs"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-016-0319-z"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49635-0_12"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.23"},{"key":"ref30","article-title":"Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions","author":"bertot","year":"2004","journal-title":"Texts in Theoretical Computer Science An EATCS Series"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99073-6_21"},{"key":"ref10","first-page":"696","article-title":"The TAMARIN prover for the symbolic analysis of security protocols","author":"meier","year":"2013","journal-title":"Computer Aided Verification"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68136-6_2"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1998-61-205"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/3343507"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-9018-6"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.27"},{"key":"ref18","first-page":"209","article-title":"Typing and compositionality for security protocols: A generalization to the geometric fragment","author":"almousa","year":"2015","journal-title":"European symposium on research in computer security"},{"key":"ref24","author":"haftmann","year":"2020","journal-title":"Code generation from Isabelle\/HOL theories"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2001.930138"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_24"},{"key":"ref25","first-page":"1","article-title":"Improvements on the Genet and Klay technique to automatically verify security protocols","author":"boichut","year":"2004","journal-title":"Automated Verification of Infinite-State Systems"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2003-11204"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866348"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.09.003"},{"key":"ref28","author":"butin","year":"2012","journal-title":"Inductive analysis of security protocols in Isabelle\/HOL with applications to electronic voting"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0055-7"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/ISIAS.2011.6122843"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-140501"},{"key":"ref7","author":"cremers","year":"2006","journal-title":"Semantics and Verification of Security Protocols"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00032"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.21"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/322510.322530"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2012-0455"},{"key":"ref5","first-page":"248","article-title":"Integrating automated and interactive protocol verification","author":"brucker","year":"2009","journal-title":"Formal Aspects in Security and Trust"}],"event":{"name":"2021 IEEE 34th Computer Security Foundations Symposium (CSF)","location":"Dubrovnik, Croatia","start":{"date-parts":[[2021,6,21]]},"end":{"date-parts":[[2021,6,25]]}},"container-title":["2021 IEEE 34th Computer Security Foundations Symposium (CSF)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9504607\/9505172\/09505200.pdf?arnumber=9505200","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,8]],"date-time":"2023-11-08T23:12:10Z","timestamp":1699485130000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9505200\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6]]},"references-count":36,"URL":"https:\/\/doi.org\/10.1109\/csf51468.2021.00006","relation":{},"subject":[],"published":{"date-parts":[[2021,6]]}}}