Usually, networks such as the Internet run many security protocols (e.g., TLS, IPSec, DNSSEC) in parallel. While the security properties of many of these protocols have been analyzed in great detail, much less research has been devoted to their parallel composition. It is far from self-evident that the parallel composition of secure protocols is still secure, in fact one can systematically construct counter-examples.

One such problem is if protocols have similar message structures of different meaning, so that an attacker may be able to abuse messages, or parts thereof, that he has learned in the context of one protocol, and use them in the context of another where the same structure has a different meaning.

We address this problem in our ESORICS 2018 paper, entitled “Stateful Protocol Composition” [1]. In particular, we extend the compositionality paradigm to stateful protocols, where participants may maintain a database (e.g., a list of valid public keys) independent of sessions. Such databases do not necessarily grow monotonically during protocol execution: we allow, for instance, negative membership checks and deletion of elements from databases. Moreover, we allow for such 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 interferences, 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.

The proof of the main result is by a reduction to a problem finding solutions for intruder constraints: given a satisfiable constraint representing an attack on the composition, we show that the projection of the constraints to the individual protocols are satisfiable. This particular tricky part of the proof has been formalized in the interactive theorem prover Isabelle/HOL.

For details, read our ESORICS paper [1] or the extended version [2], which includes the pen-and-paper proofs and short explanations of the Isabelle proofs.

Update: The formalization is now available in the Archive of Formal Proofs: “Stateful Protocol Composition and Typing” [3].

References