Stateful Protocol Composition (Extended Version)

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 analyzing the component protocols in isolation is sufficient to prove security of the more complex composition. Our main contribution is an extension of the compositionality paradigm to stateful protocols where participants main- tain shared databases. We also 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, Security Protocol, Compositionality

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/

Please cite this work as follows:
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/

BibTeX
@TechReport{ hess.ea:tr-stateful-protocol:2018,
  author      = {Andreas V. Hess and Sebastian A. M{\"o}dersheim and Achim D.
                 Brucker},
  institution = {DTU Compute, Technical University Denmark},
  language    = {USenglish},
  title       = {Stateful Protocol Composition (Extended Version)},
  areas       = {formal methods, security},
  keywords    = {Protocol Composition, Security Protocol, Compositionality},
  year        = {2018},
  number      = {2018-03},
  num_pages   = {28},
  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 analyzing the component protocols in
                 isolation is sufficient to prove security of the more complex
                 composition. Our main contribution is an extension of the
                 compositionality paradigm to stateful protocols where
                 participants main- tain shared databases. We also 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.},
  issn        = {1601-2321},
  obsoletedby = {hess.ea:stateful-protocol-composition:2023},
  note        = {Author copy: \url{https://logicalhacking.com/publications/hess.ea-tr-stateful-protocol-2018/}},
  pdf         = {https://logicalhacking.com/publications/hess.ea-tr-stateful-protocol-2018/hess.ea-tr-stateful-protocol-2018.pdf},
}