Usually, security protocols are not executed in isolation. Actually, manny different security protocols usually run in parallel. Still, while the security properties of many of these protocols, e.g., TLS, have been analyzed in great detail, much less research has been devoted to their parallel composition. And, it is far from self-evident that the parallel composition of secure protocols is still secure.

For example, different protocols may have a similar message structures of different meaning, so that an attacker may be able to abuse messages, or parts thereof, that they have learned in the context of one protocol, and use them in the context of another where the same structure has a different meaning. Thus, we have to exclude that the protocols in some sense “interfere” with each other. However, it is unreasonable to require that the developers of the different protocols have to work together and synchronize with each other. Similarly, we do not want to reason about the composition of several protocols as a whole, neither in manual nor automated verification. Instead, we want a set of sufficient conditions and a composition theorem of the form: every set of protocols that satisfies the conditions yields a secure composition, provided that each protocol is secure in isolation. The conditions should be realistic so that many existing protocols like TLS actually satisfy them, and they should be simple, in the sense that checking them is a static task that does not involve considering the reachable states.

In our recent paper [1] in the ACM Transactions on Privacy and Security, we present a formalization of stateful protocol composition in Isabelle/HOL, together with a formal verification approach also implemented in Isabelle/HOL. We extend the compositionality paradigm to stateful protocols, where participants may maintain a database (e.g., a list of valid public keys). Such databases do not necessarily grow monotonically during protocol execution—we allow, e.g., negative membership checks and deletion of elements from databases. Moreover, we allow databases to be shared between the protocols to be composed. For instance, in the example of public keys, there could be several protocols for registering, certifying, and revoking keys that all work on the same public-key database. Since such a shared database can potentially be exploited by the intruder to trigger harmful interference, an important part of our result is a clear coordination of the ways in which each protocol is allowed to access the database. This coordination is based on assumptions and guarantees on the transactions that involve the database. Moreover, this also allows us to support protocols with the declassification of long-term secrets (e.g., that the private key to a revoked public key may be learned by the intruder without breaking the security goals). The result is so general that it actually also covers many forms of sequential composition as a special case, since one can for instance model that one protocol inserts keys into a database of fresh session keys, and another protocol “consumes” and uses them. Our main contributions are:

1. We extend the compositionality paradigm to stateful protocols. In particular, our result supports participants who maintain long-term databases that can be shared among several protocols, and a paradigm for declassification of shared secrets. Our result is so general that it also covers various forms of sequential composition as a special case.
2. Our compositionality result is formalized and proved in the interactive theorem prover Isabelle/HOL, providing a strong correctness guarantee of our proofs. This means that one can prove the security of a composed protocol in Isabelle by proving the security of the components in isolation and checking the compositionality conditions, and thus derive the security of the composition as an Isabelle theorem.
3. We implemented checks for the compositionality conditions in Isabelle/HOL, so that they can be checked automatically.
4. We have connected the compositionality result to our tool PSPSP [2] that can perform automatic proofs for many stateful protocols in Isabelle. This extends PSPSP (for protocols supported by PSPSP) with a composable verification method.

All of our theory and proofs are published and maintained in the Archive of Formal Proofs (AFP) [2], [3]. The overall formalization is over 27000 lines of code (over 8000 more lines than the conference version) and took about 36 person months to develop.

References