Show simple item record

dc.contributor.authorHess, AV
dc.contributor.authorMödersheim, SA
dc.contributor.authorBrucker, AD
dc.date.accessioned2022-12-14T14:39:36Z
dc.date.issued2023-01-25
dc.date.updated2022-12-14T14:16:57Z
dc.description.abstractCommunication 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. 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—without having to re-prove anything about the other components. This paper has three contributions over previous work in parallel compositionality. First, we extend the compositionality paradigm to stateful systems: while previous approaches work only for simple protocols that only have a local session state, our result supports participants who maintain long-term databases that can be shared among several protocols. This includes a paradigm for declassification of shared secrets. This result is in fact so general that it also covers many forms of sequential composition 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, 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.en_GB
dc.description.sponsorshipDanish Council for Independent Researchen_GB
dc.description.sponsorshipEuropean Union Horizon 2020en_GB
dc.identifier.citationPublished online 25 January 2023en_GB
dc.identifier.doi10.1145/3577020
dc.identifier.grantnumber4184-00334Ben_GB
dc.identifier.grantnumber830929en_GB
dc.identifier.urihttp://hdl.handle.net/10871/132034
dc.identifierORCID: 0000-0002-6355-1200 (Brucker, Achim D)
dc.language.isoenen_GB
dc.publisherAssociation for Computing Machinery (ACM)en_GB
dc.rights©2023 Copyright held by the owner/author(s). Publication rights licensed to ACM.
dc.subjectprotocol compositionen_GB
dc.subjectstateful security protocolen_GB
dc.subjectIsabelle/HOLen_GB
dc.titleStateful protocol composition in Isabelle/HOLen_GB
dc.typeArticleen_GB
dc.date.available2022-12-14T14:39:36Z
dc.identifier.issn2471-2566
dc.descriptionThis is the author accepted manuscript. The final version is available from ACM via the DOI in this recorden_GB
dc.identifier.eissn2471-2574
dc.identifier.journalACM Transactions on Privacy and Securityen_GB
dc.relation.ispartofACM Transactions on Privacy and Security
dc.rights.urihttp://www.rioxx.net/licenses/all-rights-reserveden_GB
dcterms.dateAccepted2022-11-28
rioxxterms.versionAMen_GB
rioxxterms.typeJournal Article/Reviewen_GB
refterms.dateFCD2022-12-14T14:30:23Z
refterms.versionFCDAM
refterms.dateFOA2023-03-09T15:41:29Z
refterms.panelBen_GB


Files in this item

This item appears in the following Collection(s)

Show simple item record