Key exchange and group key establishment

Research topics / Key exchange and group key establishment

Key exchange protocols allow parties to establish shared keys over an insecure network. Their guarantees depend on how peers are authenticated, which secrets may be compromised, and how the resulting keys are used. We study these questions through security definitions, protocol constructions, attacks, and proofs.

Our work includes two-party handshakes such as TLS and Signal’s initial key agreement, as well as group key establishment and updates in ART and Messaging Layer Security (MLS). We also study password-authenticated key exchange and post-quantum protocols. Forward secrecy protects earlier communication after later compromise; post-compromise security concerns recovery for future communication under suitable conditions.

The papers below connect these guarantees to concrete protocol designs and their assumptions. They include both computational proofs and symbolic analysis, and examine how key establishment interacts with certification, session handling, and the composition of protocols.

Suggested reading

Start with the security models, or choose a protocol family below. The papers cover initial key establishment, subsequent key updates, and the assumptions needed to protect both.

Security models and guarantees

Key exchange security depends on which secrets an adversary can learn and when. Security models make these assumptions explicit and distinguish guarantees such as forward secrecy and recovery after compromise.

Examining Indistinguishability-Based Security Models for Key Exchange Protocols: The case of CK, CK-HMQV, and eCKExamining Indistinguishability-Based Security Models for Key Exchange Protocols: The case of CK, CK-HMQV, and eCK
Many recent key exchange (KE) protocols have been proven secure in the CK, CK-HMQV, or eCK security models. The exact relation between these security models, and hence the relation between the security guarantees provided by the protocols, is unclear. We show first that the CK, CK-HMQV, and eCK security models are formally incomparable. Second, we show that these models are also practically incomparable, by providing for each model attacks on protocols from the literature that are not considered by the other models. Third, our analysis enables us to find previously unreported flaws in protocol security proofs from the literature. We identify the causes of these flaws and show how they can be avoided.
Details
Cas Cremers.
ASIACCS 2011, Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security, Hong Kong, China.
[pdf] [bibtex]
We show that the CK, CK-HMQV, and eCK models are incomparable, and identify attacks covered by one model but not another. This illustrates why the details of a key exchange definition matter.

Research: Applied cryptography; Key exchange and group key establishment
ASICS: Authenticated Key Exchange Security Incorporating Certification SystemsASICS: Authenticated Key Exchange Security Incorporating Certification Systems
Most security models for authenticated key exchange (AKE) do not explicitly model the associated certification system, which includes the certification authority (CA) and its behaviour. However, there are several well-known and realistic attacks on AKE protocols which exploit various forms of malicious key registration and which therefore lie outside the scope of these models.

We provide the first systematic analysis of AKE security incorporating certification systems (ASICS). We define a family of security models that, in addition to allowing different sets of standard AKE adversary queries, also permit the adversary to register arbitrary bitstrings as keys. For this model family we prove generic results that enable the design and verification of protocols that achieve security even if some keys have been produced maliciously. Our approach is applicable to a wide range of models and protocols; as a concrete illustration of its power, we apply it to the CMQV protocol in the natural strengthening of the eCK model to the ASICS setting.
Details
Colin Boyd, Cas Cremers, Michèle Feltz, Kenny Paterson, Bertram Poettering, and Douglas Stebila.
International Journal of Information Security, 2016.
[pdf] [bibtex]
We extend key exchange models to include certification systems and malicious key registration. We give generic security results and apply them to CMQV in an extension of the eCK model.

Research: Applied cryptography; Key exchange and group key establishment
On Post-Compromise SecurityOn Post-Compromise Security
In this work we study communication with a party whose secrets have already been compromised. At first sight, it may seem impossible to provide any type of security in this scenario. However, under some conditions, practically relevant guarantees can still be achieved. We call such guarantees ``post-compromise security''.

We provide the first informal and formal definitions for post-compromise security, and show that it can be achieved in several scenarios. At a technical level, we instantiate our informal definitions in the setting of authenticated key exchange (AKE) protocols, and develop two new strong security models for two different threat models. We show that both of these security models can be satisfied, by proposing two concrete protocol constructions and proving they are secure in the models.

Our work leads to crucial insights on how post-compromise security can (and cannot) be achieved, paving the way for applications in other domains.
Details
Katriel Cohn-Gordon, Cas Cremers, and Luke Garratt.
IEEE CSF 2016, Proc. of the 29th IEEE Computer Security Foundations Symposium, 2016.
[Long version] [bibtex]
We introduce post-compromise security and instantiate it in two computational key exchange models. We give constructions and proofs showing how security can be recovered under different compromise assumptions.

Research: Post-compromise security; Applied cryptography; Key exchange and group key establishment
A Formal Treatment of the Limits of Authenticated Key Exchange Security Details
Michèle Feltz and Cas Cremers.
Juggling Formal Methods and Security. Essays Dedicated to Sjouke Mauw on the Occasion of His 65th Birthday.
[bibtex]
We formalize limits on key exchange security for different classes of stateless and stateful protocols. From these impossibility results, we derive security models and give protocols that satisfy them.

Research: Applied cryptography; Key exchange and group key establishment

Deployed key exchange

Protocols such as TLS and Noise combine authentication and key establishment in several handshake modes. Their analysis must account for interactions between these modes and the use of previously established keys.

Automated Analysis of TLS 1.3: 0-RTT, Resumption and Delayed AuthenticationAutomated Analysis of TLS 1.3: 0-RTT, Resumption and Delayed Authentication
After a development process of many months, the TLS 1.3 specification is nearly complete. To prevent past mistakes, this crucial security protocol must be thoroughly scrutinised prior to deployment.

In this work we model and analyse revision 10 of the TLS 1.3 specification using the Tamarin prover, a tool for the automated analysis of security protocols. We specify and analyse the interaction of various handshake modes for an unbounded number of concurrent TLS connections. We show that revision 10 meets the goals of authenticated key exchange in both the unilateral and mutual authentication cases.

We extend our model to incorporate the desired delayed client authentication mechanism, a feature that is likely to be included in the next revision of the specification, and uncover a potential attack in which an adversary is able to successfully impersonate a client during a PSK-resumption handshake. This observation was reported to, and confirmed by, the IETF TLS Working Group.

Our work not only provides the first supporting evidence for the security of several complex protocol mode interactions in TLS 1.3, but also shows the strict necessity of recent suggestions to include more information in the protocol’s signature contents.
Details
Cas Cremers, Marko Horvat, Sam Scott, and Thyla van der Merwe.
IEEE Symposium on Security and Privacy(Oakland), San Jose, CA, May 2016.
This work contributed to the development of the IETF "Transport Layer Security" (TLS) 1.3 standard.
[pdf] [further information and sources] [bibtex] [RFC 8446]
We analyze draft 10 of TLS 1.3 using Tamarin, including interactions between handshake modes. Extending the model with proposed delayed client authentication reveals an impersonation attack during PSK resumption.

Research: Formal verification of security protocols; Security protocol standards; Key exchange and group key establishment
A Comprehensive Symbolic Analysis of TLS 1.3 Details
Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe.
ACM CCS 2017: Proceedings of the 24th ACM Conference on Computer and Communications Security, Dallas, USA, 2017.
This work contributed to the development of the IETF "Transport Layer Security" (TLS) 1.3 standard.
[pdf] [bibtex] [further information and sources] [RFC 8446]
We analyze draft 21 of TLS 1.3 using Tamarin, considering interactions between its handshake modes. This work contributed to the development of the standard.

Research: Formal verification of security protocols; Security protocol standards; Key exchange and group key establishment
A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols Details
Guillaume Girol, Lucca Hirschi, Ralf Sasse, Dennis Jackson, Cas Cremers, and David Basin.
USENIX 2020, Boston, USA, August 2020.
Artifact Evaluated
[pdf] [bibtex]
We systematically compare the security guarantees of Noise handshake patterns under different threat models. Our analysis identifies missing assumptions and differences between patterns.

Research: Security protocol standards; Key exchange and group key establishment

Messaging and group key establishment

Messaging protocols establish keys when participants may be offline and update them as conversations continue. Group protocols must also account for changes in membership and the compromise of individual members.

A Formal Security Analysis of the Signal Messaging ProtocolA Formal Security Analysis of the Signal Messaging Protocol
Signal is a new security protocol that provides end-to-end encryption for instant messaging. It has recently been adopted by WhatsApp, Facebook Messenger and Google Allo among many others; the first two of these have at least 1 billion active users. Signal includes several uncommon security properties (such as ``future secrecy'' or ``post-compromise security''), enabled by a novel technique called ratcheting in which session keys are updated with every message sent. Despite its importance and novelty, there has been little to no academic analysis of the Signal protocol.

We conduct the first security analysis of Signal's Key Agreement and Double Ratchet as a multi-stage key exchange protocol. We extract from the implementation a formal description of the abstract protocol, define a security model which can capture the ``ratcheting'' key update structure, and prove the security of Signal's core in our model. Our presentation and results can serve as a starting point for other analyses of this widely adopted protocol.
Details
Katriel Cohn-Gordon, Cas Cremers, Benjamin Dowling, Luke Garratt, and Douglas Stebila.
IEEE EuroS&P 2017.
[full version (eprint)] [bibtex]
We analyze Signal's initial key agreement and Double Ratchet as a multi-stage key exchange protocol, and prove security of the protocol core in our model.

Research: Secure messaging; Post-compromise security; Applied cryptography; Key exchange and group key establishment
Automated verification of group key agreement protocolsAutomated verification of group key agreement protocols
We advance the state-of-the-art in automated symbolic cryptographic protocol analysis by providing the first algorithm that can handle Diffie-Hellman exponentiation, bilinear pairing, and AC-operators. Our support for AC-operators enables protocol specifications to use multisets, natural numbers, and finite maps. We implement the algorithm in the TAMARIN prover and provide the first symbolic correctness proofs for group key agreement protocols that use Diffie-Hellman or bilinear pairing, loops, and recursion, while at the same time supporting advanced security properties, such as perfect forward secrecy or eCK-security. We automatically verify a set of protocols, including the STR, group Joux, and GDH protocols, thereby demonstrating the effectiveness of our approach.
Details
Benedikt Schmidt, Ralf Sasse, Cas Cremers, and David Basin.
IEEE Symposium on Security and Privacy(Oakland), San Jose, CA, May 2014.
[preprint] [bibtex]
We extend automated verification to group key agreement protocols using Diffie-Hellman exponentiation or bilinear pairings, loops, and recursion. Case studies include STR, group Joux, and GDH protocols.

Research: Formal verification of security protocols; Key exchange and group key establishment
On Ends-to-Ends Encryption: Asynchronous Group Messaging with Strong Security Guarantees Details
Katriel Cohn-Gordon, Cas Cremers, Luke Garratt, Jon Millican, and Kevin Milner.
ACM CCS 2018: Proceedings of the 25th ACM Conference on Computer and Communications Security, Toronto, Canada, 2018.
[pdf] [bibtex]
We introduce Asynchronous Ratcheting Trees (ART), which establish and update a group key without requiring participants to be online at the same time. We study post-compromise security through computational proofs and symbolic verification.

Research: Secure messaging; Post-compromise security; Security protocol standards; Applied cryptography; Key exchange and group key establishment
ETK: External-Operations TreeKEM and the Security of MLS in RFC 9420 Details
Cas Cremers, Esra Günsay, Vera Wesselkamp, and Mang Zhao.
Eurocrypt 2026, Rome, May 2026.
[eprint]
We define an ideal functionality for group key agreement with external operations and prove that ETK realizes it. The analysis covers the core of MLS in RFC 9420 and clarifies its post-compromise security guarantees.

Research: Secure messaging; Post-compromise security; Security protocol standards; Applied cryptography; Key exchange and group key establishment
Formal Security Analysis of the Olvid Messenger Details
Noemi Terzo, Cas Cremers, Ruben Gonzalez, Peter Schwabe, Yuval Yarom, and Zhiyuan Zhang.
ACM CCS 2026, The Hague, November 2026.
[eprint]
We formally analyze Olvid's authenticated key exchange and continuous key agreement protocols. We establish core security guarantees in our models and identify limitations under stronger compromise models, including eCK.

Research: Secure messaging; Applied cryptography; Key exchange and group key establishment

Password-authenticated key exchange

Password-authenticated key exchange (PAKE) establishes keys using a shared password. Its security goals include preventing an intercepted exchange from enabling offline password guessing.

CHIP and CRISP: Protecting All Parties Against Compromise through Identity-Binding PAKEs Details
Cas Cremers, Moni Naor, Shahar Paz, and Eyal Ronen.
CRYPTO 2022, Santa Barbara, USA, August 2022.
[eprint] [bibtex]
We define identity-binding PAKEs in the UC model and give constructions that protect stored passwords against compromise of any party. The definitions extend protection to settings where all parties share a password and can communicate with each other.

Research: Applied cryptography; Key exchange and group key establishment
Multi-Stage Group Key Distribution and PAKEs: Securing Zoom Groups against Malicious Servers without New Security Elements Details
Cas Cremers, Eyal Ronen, and Mang Zhao.
IEEE Symposium on Security & Privacy (Oakland), May 2024.
[eprint] [bibtex]
We define security models for multi-stage group key distribution and analyze Zoom. We show how integrating PAKEs can strengthen security against malicious servers using the existing meeting passcodes.

Research: Secure messaging; Applied cryptography; Key exchange and group key establishment

Verification and primitive assumptions

Key exchange proofs depend on the guarantees of their cryptographic building blocks. Formal methods help make these dependencies explicit, including for protocols intended to resist quantum attackers.

A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols Details
Cas Cremers, Caroline Fontaine, and Charlie Jacomme.
IEEE Symposium on Security & Privacy (Oakland), May 2022
[eprint] [bibtex]
We develop a computational logic sound against quantum attackers and implement it in PQ-Squirrel. Case studies give mechanized post-quantum security proofs for key exchange constructions and a proposed variant of Signal's X3DH.

Research: Formal verification of security protocols; Applied cryptography; Key exchange and group key establishment
Keeping Up with the KEMs: Stronger Security Notions for KEMs and automated analysis of KEM-based protocols Details
Cas Cremers, Alexander Dax, and Niklas Medinger.CCS Distinguished Artifact Award SpringerOpen Cybersecurity Best Theoretical Paper Award
ACM CCS 2024, Salt Lake City, October 2024.
[eprint] [bibtex]
Key Encapsulation Mechanisms (KEMs) can be regarded as a simple form of key establishment. We define binding properties for key encapsulation mechanisms and develop corresponding symbolic models. These models help identify which properties a key exchange protocol requires from its KEM.

Research: Cryptographic primitives; Applied cryptography; Key exchange and group key establishment

Tools and resources

Complete chronological publication list