Stateful Protocol Composition

Andreas V. Hess, Sebastian A. Mödersheim und Achim D. Brucker

Cover for hess.ea:stateful:2018.We prove a parallel compositionality result for protocols with a shared mutable state, i.e., stateful protocols. For protocols satisfying certain compositionality conditions our result shows that verifying the component protocols in isolation is sufficient to prove security of their composition. Our main contribution is an extension of the compositionality paradigm to stateful protocols where participants maintain shared databases. Because of the generality of our result we also cover many forms of sequential composition as a special case of stateful parallel composition. Moreover, we support declassification of shared secrets. As a final contribution we prove the core of our result in Isabelle/HOL, providing a strong correctness guarantee of our proofs.

Schlüsselwörter: protocol composition, parallel composition, sequential composition, Isabelle/HOL
Kategorien: ,
Dokumente: (Artikel als PDF Datei)

QR Code for hess.ea:stateful:2018.Bitte zitieren sie diesen Artikel wie folgt:
Andreas V. Hess, Sebastian A. Mödersheim und Achim D. Brucker. Stateful Protocol Composition. In ESORICS. Lecture Notes in Computer Science (11098), pages 427-446, Springer-Verlag, 2018.
Schlüsselwörter: protocol composition, parallel composition, sequential composition, Isabelle/HOL
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-319-99073-6) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@InCollection{ hess.ea:stateful:2018,
abstract = {We prove a parallel compositionality result for protocols with a shared mutable state, i.e., stateful protocols. For protocols satisfying certain compositionality conditions our result shows that verifying the component protocols in isolation is sufficient to prove security of their composition. Our main contribution is an extension of the compositionality paradigm to stateful protocols where participants maintain shared databases. Because of the generality of our result we also cover many forms of sequential composition as a special case of stateful parallel composition. Moreover, we support declassification of shared secrets. As a final contribution we prove the core of our result in Isabelle/HOL, providing a strong correctness guarantee of our proofs.},
address = {Heidelberg},
author = {Andreas V. Hess and Sebastian A. M{\"o}dersheim and Achim D. Brucker},
booktitle = {ESORICS},
doi = {10.1007/978-3-319-99073-6},
editor = {Javier Lopez and Jianying Zhou},
isbn = {978-3-319-99072-9},
keywords = {protocol composition, parallel composition, sequential composition, Isabelle/HOL},
language = {USenglish},
location = {Barcelona, Spain},
number = {11098},
pages = {427--446},
pdf = {https://www.brucker.ch/bibliography/download/2018/hess.ea-stateful-2018.pdf},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {Stateful Protocol Composition},
url = {https://www.brucker.ch/bibliography/abstract/hess.ea-stateful-2018},
year = {2018},
}