Stateful Protocol Composition in Isabelle/HOL

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

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.

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.

Keywords:
Protocol Composition, Stateful Security Protocol, Isabelle/HOL

Supplementary material:
[  Formalization (AFP)  ]

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

BibTeX
@Article{ hess.ea:stateful-protocol-composition:2023,
  author          = {Andreas V. Hess and Sebastian A. M{\"o}dersheim and Achim D.
                     Brucker},
  title           = {Stateful Protocol Composition in {Isabelle/HOL}},
  journal         = {ACM Transactions on Privacy and Security},
  year            = {2023},
  areas           = {formal methods, security},
  abstract        = {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.
                     
                     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 \emph{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 \emph{databases} that can be
                     \emph{shared} among several protocols. This includes a
                     paradigm for \emph{declassification of shared secrets}. This
                     result is in fact so general that it also covers many forms of
                     \emph{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.},
  publisher       = {ACM Press },
  address         = {New York, NY, USA },
  doi             = {10.1145/3577020},
  keywords        = {Protocol Composition, Stateful Security Protocol,
                     Isabelle/HOL},
  supplabel01     = {Formalization (AFP)},
  supplementary01 = {https://www.isa-afp.org/entries/Stateful_Protocol_Composition_and_Typing.html},
  note            = {Author copy: \url{https://logicalhacking.com/publications/hess.ea-stateful-protocol-composition-2023/}},
  pdf             = {https://logicalhacking.com/publications/hess.ea-stateful-protocol-composition-2023/hess.ea-stateful-protocol-composition-2023.pdf},
}