{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T15:54:58Z","timestamp":1783007698048,"version":"3.54.5"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2023,4,14]],"date-time":"2023-04-14T00:00:00Z","timestamp":1681430400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Priv. Secur."],"published-print":{"date-parts":[[2023,8,30]]},"abstract":"<jats:p>Communication networks like the Internet form a large distributed system where a huge number of components run in parallel, such as security protocols and distributed web applications. For what concerns security, it is obviously infeasible to verify them all at once as one monolithic entity; rather, one has to verify individual components in isolation.<\/jats:p>\n          <jats:p>While many typical components like TLS have been studied intensively, there exists much less research on analyzing and ensuring the security of the composition of security protocols. This is a problem since the composition of systems that are secure in isolation can easily be insecure. The main goal of compositionality is thus a theorem of the form: given a set of components that are already proved secure in isolation and that satisfy a number of easy-to-check conditions, then also their parallel composition is secure. Said conditions should of course also be realistic in practice, or better yet, already be satisfied for many existing components. Another benefit of compositionality is that when one would like to exchange a component with another one, all that is needed is the proof that the new component is secure in isolation and satisfies the composition conditions\u2014without having to re-prove anything about the other components.<\/jats:p>\n          <jats:p>\n            This article has three contributions over previous work in parallel compositionality. First, we extend the compositionality paradigm to\n            <jats:italic>stateful systems<\/jats:italic>\n            : while previous approaches work only for simple protocols that only have a local session state, our result supports participants who maintain long-term\n            <jats:italic>databases<\/jats:italic>\n            that can be\n            <jats:italic>shared<\/jats:italic>\n            among several protocols. This includes a paradigm for\n            <jats:italic>declassification of shared secrets<\/jats:italic>\n            . This result is in fact so general that it also covers many forms of\n            <jats:italic>sequential composition<\/jats:italic>\n            as a special case of stateful parallel composition. Second, our compositionality result is formalized and proved in Isabelle\/HOL, providing a strong correctness guarantee of our proofs. This also means that one can prove, without gaps, the security of an entire system in Isabelle\/HOL, namely the security of components in isolation and the composition conditions, and thus derive the security of the entire system as an Isabelle theorem. For the components one can also make use of our tool PSPSP that can perform automatic proofs for many stateful protocols. Third, for the compositionality conditions we have also implemented an automated check procedure in Isabelle.\n          <\/jats:p>","DOI":"10.1145\/3577020","type":"journal-article","created":{"date-parts":[[2023,1,25]],"date-time":"2023-01-25T11:54:43Z","timestamp":1674647683000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Stateful Protocol Composition in Isabelle\/HOL"],"prefix":"10.1145","volume":"26","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6312-6311","authenticated-orcid":false,"given":"Andreas V.","family":"Hess","sequence":"first","affiliation":[{"name":"DTU Compute, Technical University of Denmark, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6901-8319","authenticated-orcid":false,"given":"Sebastian A.","family":"M\u00d6dersheim","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":"University of Exeter, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,4,14]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"1","volume-title":"CSF","author":"Abate Carmine","year":"2021","unstructured":"Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Th\u00e9o Winterhalter, Catalin Hritcu, Kenji Maillard, and Bas Spitters. 2021. SSProve: A foundational framework for modular cryptographic proofs in Coq. In CSF. IEEE, 1\u201315."},{"key":"e_1_3_2_3_2","first-page":"209","volume-title":"ESORICS (LNCS)","author":"Almousa Omar","year":"2015","unstructured":"Omar Almousa, Sebastian M\u00f6dersheim, Paolo Modesti, and Luca Vigan\u00f2. 2015. Typing and compositionality for security protocols. In ESORICS (LNCS), Vol. 9327. Springer, Berlin, 209\u2013229."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.07.002"},{"key":"e_1_3_2_5_2","first-page":"324","volume-title":"POST","author":"Arapinis Myrto","year":"2015","unstructured":"Myrto Arapinis, Vincent Cheval, and St\u00e9phanie Delaune. 2015. Composing security protocols: From confidentiality to privacy. In POST, Riccardo Focardi and Andrew Myers (Eds.). Springer, Berlin, 324\u2013343."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.09.003"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.05.002"},{"key":"e_1_3_2_8_2","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/BFb0052096","volume-title":"Foundations of Computer Science (LNCS)","author":"Broy Manfred","year":"1997","unstructured":"Manfred Broy. 1997. Interactive and reactive systems: States, observations, experiments, input, output, nondeterminism, compositionality and all that. In Foundations of Computer Science (LNCS), Christian Freksa, Matthias Jantzen, and R\u00fcdiger Valk (Eds.), Vol. 1337. Springer, Berlin, 279\u2013286."},{"key":"e_1_3_2_9_2","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/s10817-008-9108-3","article-title":"An extensible encoding of object-oriented data models in HOL","volume":"41","author":"Brucker Achim D.","year":"2008","unstructured":"Achim D. Brucker and Burkhart Wolff. 2008. An extensible encoding of object-oriented data models in HOL. Journal of Automated Reasoning 41, 3 (2008), 219\u2013249.","journal-title":"Journal of Automated Reasoning"},{"key":"e_1_3_2_10_2","article-title":"State-Separating proofs: A reduction methodology for real-world protocols","volume":"306","author":"Brzuska Chris","year":"2018","unstructured":"Chris Brzuska, Antoine Delignat-Lavaud, Konrad Kohbrok, and Markulf Kohlweiss. 2018. State-Separating proofs: A reduction methodology for real-world protocols. IACR Cryptol. ePrint Arch. 306 (2018).","journal-title":"IACR Cryptol. ePrint Arch."},{"key":"e_1_3_2_11_2","volume-title":"Inductive Analysis of Security Protocols in Isabelle\/HOL with Applications to Electronic Voting","author":"Butin Denis Fr\u00e9d\u00e9ric","year":"2012","unstructured":"Denis Fr\u00e9d\u00e9ric Butin. 2012. Inductive Analysis of Security Protocols in Isabelle\/HOL with Applications to Electronic Voting. Ph.D. Dissertation. Dublin City University."},{"key":"e_1_3_2_12_2","first-page":"144","volume-title":"CSF","author":"Cheval V.","year":"2017","unstructured":"V. Cheval, V. Cortier, and B. Warinschi. 2017. Secure composition of PKIs with public key protocols. In CSF. IEEE, 144\u2013158."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0184-6"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3343507"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0059-4"},{"key":"e_1_3_2_16_2","first-page":"322","volume-title":"CSF","author":"Ciob\u00e2c\u0103 \u015etefan","year":"2010","unstructured":"\u015etefan Ciob\u00e2c\u0103 and V\u00e9ronique Cortier. 2010. Protocol composition for arbitrary primitives. In CSF. IEEE, 322\u2013336."},{"key":"e_1_3_2_17_2","volume-title":"Concurrency Verification: Introduction to Compositional and Non-compositional Methods","author":"Roever Willem-Paul de","year":"2012","unstructured":"Willem-Paul de Roever, Frank de Boer, Ulrich Hanneman, Jozef Hooman, Yassine Lakhnech, Mannes Poel, and Job Zwiers. 2012. Concurrency Verification: Introduction to Compositional and Non-compositional Methods. Cambridge University Press."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/35.5.460"},{"key":"e_1_3_2_19_2","first-page":"303","volume-title":"ESORICS","author":"Escobar Santiago","year":"2010","unstructured":"Santiago Escobar, Catherine A. Meadows, Jos\u00e9 Meseguer, and Sonia Santiago. 2010. Sequential protocol composition in Maude-NPA. In ESORICS. Springer, Berlin, 303\u2013318."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00038"},{"key":"e_1_3_2_21_2","first-page":"235","volume-title":"CSF","author":"Gro\u00df T.","year":"2011","unstructured":"T. Gro\u00df and S. M\u00f6dersheim. 2011. Vertical protocol composition. In CSF. IEEE, 235\u2013250."},{"key":"e_1_3_2_22_2","first-page":"303","volume-title":"FOSSACS","author":"Guttman Joshua D.","year":"2009","unstructured":"Joshua D. Guttman. 2009. Cryptographic protocol composition via the authentication tests. In FOSSACS. Springer, Berlin, 303\u2013317."},{"key":"e_1_3_2_23_2","first-page":"24","volume-title":"CSFW","author":"Guttman Joshua D.","year":"2000","unstructured":"Joshua D. Guttman and F. Javier Thayer. 2000. Protocol independence through disjoint encryption. In CSFW. IEEE Computer Society, 24\u201334. https:\/\/ieeexplore.ieee.org\/xpl\/conhome\/6924\/proceeding."},{"key":"e_1_3_2_24_2","first-page":"2","volume-title":"Security and Privacy","author":"Heintze N.","year":"1994","unstructured":"N. Heintze and J. D. Tygart. 1994. A model for secure protocols and their compositions. In Security and Privacy. IEEE, 2\u201313."},{"key":"e_1_3_2_25_2","volume-title":"Typing and Compositionality for Stateful Security Protocols","author":"Hess Andreas Viktor","year":"2019","unstructured":"Andreas Viktor Hess. 2019. Typing and Compositionality for Stateful Security Protocols. Ph.D. Dissertation. Technical University Denmark."},{"key":"e_1_3_2_26_2","first-page":"1","volume-title":"CSF","author":"Hess Andreas Viktor","year":"2021","unstructured":"Andreas Viktor Hess, Sebastian Alexander M\u00f6dersheim, Achim D. Brucker, and Anders Schlichtkrull. 2021. Performing security proofs of stateful protocols. In CSF. IEEE, 1\u201316."},{"key":"e_1_3_2_27_2","first-page":"451","volume-title":"CSF","author":"Hess Andreas Viktor","year":"2017","unstructured":"Andreas Viktor Hess and Sebastian M\u00f6dersheim. 2017. Formalizing and proving a typing result for security protocols in Isabelle\/HOL. In CSF. IEEE, 451\u2013463."},{"key":"e_1_3_2_28_2","first-page":"374","volume-title":"CSF","author":"Hess Andreas Viktor","year":"2018","unstructured":"Andreas Viktor Hess and Sebastian M\u00f6dersheim. 2018. A typing result for stateful protocols. In CSF. IEEE, 374\u2013388."},{"key":"e_1_3_2_29_2","article-title":"Stateful protocol composition and typing","author":"Hess Andreas V.","year":"2020","unstructured":"Andreas V. Hess, Sebastian M\u00f6dersheim, and Achim D. Brucker. 2020. Stateful protocol composition and typing. Archive of Formal Proofs (April 2020). https:\/\/isa-afp.org\/entries\/Stateful_Protocol_Composition_and_Typing.html.","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_2_30_2","unstructured":"Andreas V. Hess Sebastian M\u00f6dersheim and Achim D. Brucker. 2022. Stateful Protocol Composition in Isabelle\/HOL - Supplementary Material. (May 2022). https:\/\/people.compute.dtu.dk\/samo\/StateParCompAdditionalMaterial.tgz."},{"key":"e_1_3_2_31_2","article-title":"Automated stateful protocol verification","author":"Hess Andreas V.","year":"2020","unstructured":"Andreas V. Hess, Sebastian M\u00f6dersheim, Achim D. Brucker, and Anders Schlichtkrull. 2020. Automated stateful protocol verification. Archive of Formal Proofs (April 2020). https:\/\/isa-afp.org\/entries\/Automated_Stateful_Protocol_Verification.html.","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_2_32_2","first-page":"427","volume-title":"ESORICS 2018 (LNCS)","author":"Hess Andreas Viktor","year":"2018","unstructured":"Andreas Viktor Hess, Sebastian Alexander M\u00f6dersheim, and Achim D. Brucker. 2018. Stateful protocol composition. In ESORICS 2018 (LNCS), Vol. 11098. Springer, Berlin, 427\u2013446. Extended version [32]."},{"key":"e_1_3_2_33_2","volume-title":"Stateful Protocol Composition (Extended Version)","author":"Hess A. V.","year":"2018","unstructured":"A. V. Hess, S. A. M\u00f6dersheim, and A. D. Brucker. 2018. Stateful Protocol Composition (Extended Version). Technical Report. DTU Compute. Technical Report-2018-03. https:\/\/people.compute.dtu.dk\/samo\/."},{"key":"e_1_3_2_34_2","first-page":"41","volume-title":"CCS","author":"K\u00fcsters Ralf","year":"2011","unstructured":"Ralf K\u00fcsters and Max Tuengerthal. 2011. Composition theorems without pre-established session identifiers. In CCS. ACM, New York, NY, 41\u201350."},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-020-09352-1"},{"key":"e_1_3_2_36_2","first-page":"31","volume-title":"CSFW","author":"Lowe Gavin","year":"1997","unstructured":"Gavin Lowe. 1997. A hierarchy of authentication specifications. In CSFW. IEEE, 31\u201344."},{"key":"e_1_3_2_37_2","volume-title":"Communication and Concurrency","author":"Milner Robin","year":"1989","unstructured":"Robin Milner. 1989. Communication and Concurrency. Prentice Hall, Saddle River, NJ."},{"key":"e_1_3_2_38_2","first-page":"259","volume-title":"CSF","author":"M\u00f6dersheim Sebastian","year":"2014","unstructured":"Sebastian M\u00f6dersheim and Georgios Katsoris. 2014. A sound abstraction of the parsing problem. In CSF. IEEE, 259\u2013273."},{"key":"e_1_3_2_39_2","first-page":"337","volume-title":"ESORICS (LNCS)","author":"M\u00f6dersheim S.","year":"2009","unstructured":"S. M\u00f6dersheim and L. Vigan\u00f2. 2009. Secure pseudonymous channels. In ESORICS (LNCS), Vol. 5789. Springer, Berlin, 337\u2013354."},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/24592.24594"}],"container-title":["ACM Transactions on Privacy and Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3577020","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3577020","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:51:11Z","timestamp":1750182671000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3577020"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,14]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,8,30]]}},"alternative-id":["10.1145\/3577020"],"URL":"https:\/\/doi.org\/10.1145\/3577020","relation":{},"ISSN":["2471-2566","2471-2574"],"issn-type":[{"value":"2471-2566","type":"print"},{"value":"2471-2574","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4,14]]},"assertion":[{"value":"2021-10-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-11-28","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-04-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}