{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T18:55:04Z","timestamp":1784314504703,"version":"3.55.0"},"reference-count":47,"publisher":"SAGE Publications","issue":"6","license":[{"start":{"date-parts":[[2025,8,18]],"date-time":"2025-08-18T00:00:00Z","timestamp":1755475200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"},{"start":{"date-parts":[[2025,8,18]],"date-time":"2025-08-18T00:00:00Z","timestamp":1755475200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"funder":[{"DOI":"10.13039\/100018693","name":"HORIZON EUROPE Framework Programme","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100018693","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Danish Industry Foundation"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer Security"],"published-print":{"date-parts":[[2025,11]]},"abstract":"<jats:p>In protocol verification, we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants such as Isabelle\/HOL. The latter provides overwhelmingly high assurance of the correctness, which automated methods often cannot: due to their complexity, bugs in such automated verification tools are likely, and thus the risk of erroneously verifying a flawed protocol is nonnegligible. There are a few works that try to combine the advantages from both ends of the spectrum: a high degree of automation and assurance. We present here a first step toward achieving this for a more challenging class of protocols, namely those that work with a mutable long-term state. To our knowledge, this is the first approach that achieves fully automated verification of stateful protocols in an LCF-style theorem prover. The approach also includes a simple user-friendly transaction-based protocol specification language embedded into Isabelle, and can also leverage a number of existing results, such as the soundness of a typed model.<\/jats:p>","DOI":"10.1177\/0926227x251358741","type":"journal-article","created":{"date-parts":[[2025,8,18]],"date-time":"2025-08-18T08:16:42Z","timestamp":1755505002000},"page":"425-469","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":1,"title":["PSPSP: A tool for automated verification of stateful protocols in Isabelle\/HOL"],"prefix":"10.1177","volume":"33","author":[{"given":"Andreas Viktor","family":"Hess","sequence":"first","affiliation":[{"name":"DTU Compute, Technical University of Denmark, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sebastian Alexander","family":"M\u00f6dersheim","sequence":"additional","affiliation":[{"name":"DTU Compute, Technical University of Denmark, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6355-1200","authenticated-orcid":false,"given":"Achim D","family":"Brucker","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Exeter, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anders","family":"Schlichtkrull","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Aalborg University Copenhagen, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"179","published-online":{"date-parts":[[2025,8,18]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3577020"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1998-61-205"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68136-6"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/322510.322530"},{"key":"e_1_3_3_6_2","doi-asserted-by":"crossref","unstructured":"Goubault-Larrecq J. Towards producing formally checkable security proofs automatically. In: 2008 21st IEEE computer security foundations symposium Pittsburgh PA USA 2008 pp. 224\u2013238.","DOI":"10.1109\/CSF.2008.21"},{"key":"e_1_3_3_7_2","doi-asserted-by":"crossref","unstructured":"Blanchet B. An efficient cryptographic protocol verifier based on Prolog rules. In: Computer Proceedings. 14th IEEE Computer security foundations workshop 2001 Cape Breton NS Canada 2001 pp.82\u201396.","DOI":"10.1109\/CSFW.2001.930138"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2012-0455"},{"key":"e_1_3_3_9_2","unstructured":"Cremers C. Scyther: Semantics and verification of security protocols. PhD Thesis Eindhoven University of Technology 2006."},{"key":"e_1_3_3_10_2","doi-asserted-by":"crossref","unstructured":"M\u00f6dersheim SA. Abstraction by set-membership: verifying security protocols and web services with databases. In: Proceedings of the 17th ACM conference on computer and communications security (CCS'10) 2010 pp. 351\u2013360. New York NY: Association for Computing Machinery.","DOI":"10.1145\/1866307.1866348"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-140501"},{"key":"e_1_3_3_12_2","doi-asserted-by":"crossref","unstructured":"Cheval V Cortier V Turuani M. A little more conversation a little less action a lot more satisfaction: Global states in ProVerif. In: 2018 IEEE 31st Computer security foundations symposium (CSF) Oxford UK 2018 pp.344\u2013358.","DOI":"10.1109\/CSF.2018.00032"},{"key":"e_1_3_3_13_2","doi-asserted-by":"crossref","unstructured":"Meier S Schmidt B Cremers C et\u00a0al. The TAMARIN prover for the symbolic analysis of security protocols. In: Computer aided verification 2013 pp.696\u2013701.","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_3_3_14_2","doi-asserted-by":"crossref","unstructured":"Hess AV M\u00f6dersheim SA Brucker AD. Stateful protocol composition. In: Lopez J Zhou J Soriano M eds. Computer security. ESORICS 2018. Lecture Notes in Computer Science vol 11098. Cham: Springer 2018.","DOI":"10.1007\/978-3-319-99073-6_21"},{"key":"e_1_3_3_15_2","doi-asserted-by":"crossref","unstructured":"Hess A M\u00f6dersheim S. A typing result for stateful protocols. In: 2018 IEEE 31st computer security foundations symposium (CSF) Oxford UK 2018 pp.374\u2013388.","DOI":"10.1109\/CSF.2018.00034"},{"key":"e_1_3_3_16_2","doi-asserted-by":"crossref","unstructured":"M\u00f6dersheim S Bruni A. AIF-\u03c9: set-based protocol abstraction with countable families. In: Piessens F and Vigan\u00f2 L (eds) Principles of security and trust. POST 2016. Lecture Notes in Computer Science vol 9635. Berlin Heidelberg: Springer 2016.","DOI":"10.1007\/978-3-662-49635-0_12"},{"key":"e_1_3_3_17_2","doi-asserted-by":"crossref","unstructured":"Bruni A M\u00f6dersheim S Nielson F et\u00a0al. Set-\u03c0: set membership p-calculus. In: Proceedings of the 2015 IEEE 28th computer security foundations symposium (CSF'15) USA 2015 pp.185\u2013198. IEEE Computer Society.","DOI":"10.1109\/CSF.2015.20"},{"key":"e_1_3_3_18_2","doi-asserted-by":"crossref","unstructured":"Hess AV M\u00f6dersheim S Brucker AD et\u00a0al. Performing security proofs of stateful protocols. In: 2021 IEEE 34th computer security foundations symposium (CSF) Dubrovnik Croatia 2021 pp. 1\u201316.","DOI":"10.1109\/CSF51468.2021.00006"},{"key":"e_1_3_3_19_2","unstructured":"Hess AV M\u00f6dersheim S Brucker AD et\u00a0al. Automated stateful protocol verification. Archive of Formal Proofs Formal Proof Development http:\/\/isa-afp.org\/entries\/Automated_Stateful_Protocol_Verification.html (2020) accessed 18 July 2025."},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-9018-6"},{"key":"e_1_3_3_21_2","doi-asserted-by":"crossref","unstructured":"Brucker AD M\u00f6dersheim S. Integrating automated and interactive protocol verification. In: Formal aspects in security and trust 2009 pp.248\u2013262.","DOI":"10.1007\/978-3-642-12459-4_18"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3343507"},{"key":"e_1_3_3_23_2","doi-asserted-by":"crossref","unstructured":"Almousa O M\u00f6dersheim S Modesti P et\u00a0al. Typing and compositionality for security protocols: A generalization to the geometric fragment. In: Pernul G Y A Ryan P Weippl E (eds) Computer security \u2013 ESORICS 2015. Lecture Notes in Computer Science vol 9327. Cham: Springer.","DOI":"10.1007\/978-3-319-24177-7_11"},{"key":"e_1_3_3_24_2","doi-asserted-by":"crossref","unstructured":"Hess AV M\u00f6dersheim S. Formalizing and proving a typing result for security protocols in Isabelle\/HOL. In: IEEE 30th computer security foundations symposium (CSF) Santa Barbara CA USA 2017 pp.451\u2013463.","DOI":"10.1109\/CSF.2017.27"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2003-11204"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.09.003"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.10.005"},{"key":"e_1_3_3_28_2","unstructured":"Comon-Lundh H Cortier V. Security properties: Two agents are sufficient. In: Programming languages and systems 12th European symposium on programming ESOP 2003 held as part of the joint European conferences on theory and practice of software ETAPS 2003 (ed. P Degano) Warsaw Poland April 7\u201311 2003 proceedings lecture notes in computer science vol.\u00a02618 2003 pp.99\u2013113. Berlin: Springer."},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2003.12.002"},{"key":"e_1_3_3_30_2","unstructured":"Haftmann F Bulwahn L. Code generation from Isabelle\/HOL theories. http:\/\/isabelle.in.tum.de\/doc\/codegen.pdf (2020 accessed 18 July 2025)."},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00492-1"},{"key":"e_1_3_3_32_2","doi-asserted-by":"crossref","unstructured":"Wenzel M Wolff B. Building formal method tools in the Isabelle\/Isar framework. In: Schneider K and Brandt J (eds) TPHOLs 2007. Lecture notes in computer science vol. 4732 Berlin: Springer 2007 pp.352\u2013367.","DOI":"10.1007\/978-3-540-74591-4_26"},{"key":"e_1_3_3_33_2","unstructured":"Hess AV M\u00f6dersheim S Brucker AD. Stateful protocol composition and typing. Archive of formal proofs. Formal proof development https:\/\/isa-afp.org\/entries\/Stateful_Protocol_Composition_and_Typing.html (2020 accessed 18 July 2025)."},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9360-2"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511811326"},{"key":"e_1_3_3_36_2","doi-asserted-by":"crossref","unstructured":"Lowe G. A hierarchy of authentication specifications. In: Proceedings 10th computer security foundations workshop Rockport MA USA 1997 pp.31\u201344.","DOI":"10.1109\/CSFW.1997.596782"},{"key":"e_1_3_3_37_2","unstructured":"Boichut Y H\u00e9am PC Kouchnarenko O et\u00a0al. Improvements on the Genet and Klay technique to automatically verify security protocols. In: Proceedings of the 3rd international workshop on automated verification of infinite states systems (AVIS'04) 2004 pp.1\u201311."},{"key":"e_1_3_3_38_2","doi-asserted-by":"crossref","unstructured":"Chevalier Y Vigneron L. Automated unbounded verification of security protocols. In: Brinksma E and Larsen KG (eds) Computer aided verification. CAV 2002. Lecture Notes in Computer Science vol 2404. Berlin Heidelberg: Springer 2002.","DOI":"10.1007\/3-540-45657-0_24"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0055-7"},{"key":"e_1_3_3_40_2","unstructured":"Butin DF. Inductive analysis of security protocols in Isabelle\/HOL with applications to electronic voting. PhD Thesis Dublin City University 2012."},{"key":"e_1_3_3_41_2","doi-asserted-by":"crossref","unstructured":"Bella G Butin D Gray D. Holistic analysis of mix protocols. In: 2011 7th international conference on information assurance and security (IAS) Melacca Malaysia 2011 pp.338\u2013343.","DOI":"10.1109\/ISIAS.2011.6122843"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_3_43_2","doi-asserted-by":"crossref","unstructured":"Meier S Cremers C Basin D. Strong invariants for the efficient construction of machine-checked protocol security proofs. In: 2010 23rd IEEE computer security foundations symposium Edinburgh UK 2010 pp.231\u2013245.","DOI":"10.1109\/CSF.2010.23"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_3_45_2","doi-asserted-by":"crossref","unstructured":"Weidenbach C Dimova D Fietzke A et\u00a0al. SPASS version 3.5. In: Conference on automated deduction 2009 pp.140\u2013145.","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-210053"},{"key":"e_1_3_3_47_2","unstructured":"Doghmi SF Guttman JD Thayer FJ. Searching for shapes in cryptographic protocols. In: Grumberg O and Huth M. (eds) Tools and algorithms for the construction and analysis of systems. TACAS 2007 Lecture Notes in Computer Science vol 4424. Berlin Heidelberg: Springer."},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-016-0319-z"}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/0926227X251358741","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.1177\/0926227X251358741","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/0926227X251358741","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T20:45:55Z","timestamp":1777495555000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.1177\/0926227X251358741"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,18]]},"references-count":47,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,11]]}},"alternative-id":["10.1177\/0926227X251358741"],"URL":"https:\/\/doi.org\/10.1177\/0926227x251358741","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"value":"0926-227X","type":"print"},{"value":"1875-8924","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,18]]}}}