Stateful Protocol Composition

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

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.

Keywords:
Protocol Composition, Parallel Composition, Sequential Composition, Isabelle/HOL

Obsoleted by:
This publication has been obsoleted by the following publication:
A. V. Hess, S. A. Mödersheim, and A. D. Brucker, “Stateful protocol composition in Isabelle/HOL,” ACM Transactions on Privacy and Security, 2023, doi: 10.1145/3577020. Author copy: https://logicalhacking.com/publications/hess.ea-stateful-protocol-composition-2023/

Extended by:
An extended version is available as:
A. V. Hess, S. A. Mödersheim, and A. D. Brucker, “Stateful protocol composition (extended version),” DTU Compute, Technical University Denmark, 2018-03, 2018. Author copy: https://logicalhacking.com/publications/hess.ea-tr-stateful-protocol-2018/

Please cite this work as follows:
A. V. Hess, S. A. Mödersheim, and A. D. Brucker, “Stateful protocol composition,” in ESORICS, J. Lopez and J. Zhou, Eds. Heidelberg: Springer-Verlag, 2018, pp. 427–446. doi: 10.1007/978-3-319-99073-6. Author copy: https://logicalhacking.com/publications/hess.ea-stateful-2018/

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.},
  keywords    = {Protocol Composition, Parallel Composition, Sequential
                 Composition, Isabelle/HOL},
  location    = {Barcelona, Spain},
  author      = {Andreas V. Hess and Sebastian A. M{\"o}dersheim and Achim D.
                 Brucker},
  booktitle   = {ESORICS},
  language    = {USenglish},
  publisher   = {Springer-Verlag },
  address     = {Heidelberg },
  series      = {Lecture Notes in Computer Science },
  number      = {11098},
  editor      = {Javier Lopez and Jianying Zhou},
  title       = {Stateful Protocol Composition},
  areas       = {formal methods, security},
  year        = {2018},
  doi         = {10.1007/978-3-319-99073-6},
  pages       = {427--446},
  isbn        = {978-3-319-99072-9},
  obsoletedby = {hess.ea:stateful-protocol-composition:2023},
  extendedby  = {hess.ea:tr-stateful-protocol:2018},
  note        = {Author copy: \url{https://logicalhacking.com/publications/hess.ea-stateful-2018/}},
  pdf         = {https://logicalhacking.com/publications/hess.ea-stateful-2018/hess.ea-stateful-2018.pdf},
}