Research topics / Protocol composition
Protocol composition
Security protocols often run alongside other protocols, share keys, or use the output of one protocol as the input to another. Security of each component in isolation does not guarantee security of the combined system. Messages from one protocol may, for example, be accepted by another in an unintended way.
We study conditions under which protocols can be composed securely, and how to use these conditions to verify larger systems from smaller components. Our work includes symbolic composition frameworks, analysis of multi-protocol attacks, and computational results for composing key exchange with symmetric-key protocols. In recent work, we considers dynamic corruption and applies compositional verification to forward secrecy in TLS 1.3 with Encrypted Client Hello (ECH), see also Erik Pallas’ blog post.
Suggested reading
These papers explain why composition requires care and develop conditions under which security proofs for individual protocols can be combined.
-
Secure Protocol Composition under Dynamic Corruption: Scaling Up Symbolic Analysis for Real-World Security Properties
Details
Cas Cremers, Erik Pallas, and Aleksi Peltonen.
USENIX 2026, August 2026.
To appear.
[eprint] [blog post]We prove a symbolic composition result that allows dynamic corruption under a disjointness requirement. We apply it to the analysis of forward secrecy in TLS 1.3 with Encrypted Client Hello.
-
Falsifiability, Composability, and Comparability of Game-Based Security Models for Key Exchange Protocols
Details
Chris Brzuska, Cas Cremers, Håkon Jacobsen, Douglas Stebila, and Bogdan Warinschi.
Information Security in a Connected World (LNCS 15600), Springer, 2025.
[eprint] [bibtex]We study how choices in computational key exchange definitions affect composition with symmetric-key protocols. Models with multiple Test queries permit tighter composition bounds than models with a single Test query.
-
Compositionality of security protocols: a research agendaCompositionality of security protocols: a research agenda
The application of formal methods to security protocol analysis has been extensively researched during the last 25 years. Several formalisms and (semi-)automatic tools for the verification of security protocols have been developed. However, their applicability is limited to relatively small protocols that run in isolation. Many of the protocols that are in use today cannot be verified using these methods. One of the main reasons for this is that these protocols are composed of several sub-protocols. Such a composition of protocols is not addressed in the majority of formalisms. In this paper we identify a number of issues that are relevant to applying formal methods to the problem of security protocol composition. Additionally, we describe what research needs to be done to meet this challenge.
Details
Cas Cremers.
VODCA 2004, ENTCS Vol. 142(3), Bertinoro, Italy, 2006.
[pdf] [bibtex]We identify the challenges that arise when security protocols are built from smaller components and outline a research agenda for compositional analysis.
Research: Protocol composition -
Feasibility of multi-protocol attacksFeasibility of multi-protocol attacks
Formal modeling and verification of security protocols typically assumes that a protocol is executed in isolation, without other protocols sharing the network. We investigate the existence of multi-protocol attacks on protocols described in literature. Given two or more protocols, that share key structures and are executed in the same environment, are new attacks possible? Out of 30 protocols from literature, we find that 23 are vulnerable to multi-protocol attacks. We identify two likely attack patterns and sketch a tagging scheme to prevent multi-protocol attacks.
Details
Cas Cremers.
ARES 2006, Proc. of the first international conference on availability, reliability and security, Vienna, Austria, April 2006, IEEE.
[pdf] [bibtex]We study attacks that arise when protocols share key structures and run in the same environment. The analysis illustrates why security in isolation need not imply security alongside other protocols.
Research: Protocol composition -
A framework for compositional verification of security protocolsA framework for compositional verification of security protocols
Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach. We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verification of large structured security protocols. Our approach is to verify properties of component protocols in a multi-protocol environment, then deduce properties about the composed protocol. To reduce the complexity of multi-protocol verification, we introduce a notion of protocol independence and prove a number of theorems that enable analysis of independent component protocols in isolation. To illustrate the applicability of our framework to real-world protocols, we study a key establishment sequence in WiMAX consisting of three subprotocols. Except for a small amount of trivial reasoning, the analysis is done using automatic tools.
Details
Suzana Andova, Cas Cremers, Kristian Gjøsteen, Sjouke Mauw, Stig F. Mjølsnes, and Saša Radomirović.
Information and Computation, Special issue on Computer Security: Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459, Elsevier, 2008.
[pdf] [bibtex]We develop a framework for deriving security properties of composed protocols from their components. Protocol independence permits analysis in isolation; a WiMAX key establishment sequence illustrates the approach.