Research topics / Secure messaging

We study the security of messaging protocols, including Signal and group messaging protocols. A central question is how to define their security guarantees in the presence of an adversary who can compromise devices and interfere with communication. Our work includes the first proofs of Signal’s key agreement and Double Ratchet, and research on asynchronous group messaging and Messaging Layer Security (MLS).

Security of a messaging application depends on more than its key exchange and encryption algorithms. For example, the application may maintain several sessions between the same two users. We analyze how these sessions are combined into conversations, and how session handling affects recovery after compromise. For the foundations and limits of such recovery, see our work on post-compromise security.

Suggested reading

The following papers cover the security of individual sessions, their use in conversations, and the extension to group messaging.

1. 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 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
2. Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations Details
   Cas Cremers, Charlie Jacomme, and Aurora Naska.
   USENIX 2023, August 2023.
   [eprint] [pdf] [bibtex]

   We study how session handling affects the security of a conversation. Our analysis of Signal's Sesame layer shows that post-compromise security of individual ratcheting chains does not suffice.

   Research: Secure messaging; Post-compromise security; Formal verification of security protocols; Key exchange and group key establishment
3. 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
4. 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]

   This work studies asynchronous group messaging, extending the problem beyond communication between two parties. It was part of the research that motivated the development of IETF's MLS.

   Research: Secure messaging; Post-compromise security; Security protocol standards; Applied cryptography; Key exchange and group key establishment
5. 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 analyze the core of MLS in RFC 9420, including external commits and proposals. These operations affect the post-compromise security guarantees that the protocol can provide.

   Research: Secure messaging; Post-compromise security; Security protocol standards; Applied cryptography; Key exchange and group key establishment
6. Impossibility Results for Post-Compromise Security in Real-World Communication Systems Details
   Cas Cremers, Niklas Medinger, and Aurora Naska.
   IEEE Symposium on Security & Privacy, San Francisco, May 2025.
   [eprint] [bibtex]

   We identify conditions under which resilience to state loss prevents full post-compromise security for end-users. These limits concern the communication system, beyond its underlying ratchet.

   Research: Secure messaging; Post-compromise security

Further reading

• 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]
  Research: Secure messaging; Applied cryptography; Key exchange and group key establishment
• Secure Messaging with Strong Compromise Resilience, Temporal Privacy, and Immediate Decryption Details
  Cas Cremers and Mang Zhao.
  IEEE Symposium on Security & Privacy (Oakland), May 2024.
  [eprint] [bibtex]
  Research: Secure messaging; Post-compromise security; Applied cryptography; Key exchange and group key establishment
• The Complexities of Healing in Secure Group Messaging: Why Cross-Group Effects Matter Details
  Cas Cremers, Britta Hale, and Konrad Kohbrok.
  USENIX 2021, Virtual, August 2021.
  [pdf] [bibtex]
  Research: Secure messaging; Post-compromise security; Key exchange and group key establishment
• Clone Detection in Secure Messaging: Improving Post-Compromise Security in Practice Details
  Cas Cremers, Jaiden Fairoze, Benjamin Kiesl, and Aurora Naska.
  ACM CCS 2020, Virtual, November 2020.
  [pdf] [bibtex] [Tamarin models]
  Research: Secure messaging; Post-compromise security; Formal verification of security protocols
• 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.
  Journal of Cryptology, 2020.
  [Springer] [bibtex]
  Research: Secure messaging; Post-compromise security; Applied cryptography; Key exchange and group key establishment
• DECIM: Detecting Endpoint Compromise In MessagingDECIM: Detecting Endpoint Compromise In Messaging

  We present DECIM, an approach to solve the challenge of detecting endpoint compromise in messaging. DECIM manages and refreshes encryption/decryption keys in an automatic and transparent way: it makes it necessary for uses of the key to be inserted in an append-only log, which the device owner can interrogate in order to detect misuse.

  We propose a multi-device messaging protocol that exploits our concept to allow users to detect unauthorised usage of their device keys. It is co-designed with a formal model, and we verify its core security property using the Tamarin prover. We present a proof-of-concept implementation providing the main features required for deployment. We find that DECIM messaging is efficient even for millions of users.

  The methods we introduce are not intended to replace existing methods used to keep keys safe (such as hardware devices, careful procedures, or key refreshment techniques). Rather, our methods provide a useful and effective additional layer of security.

  Details
  Jiangshan Yu, Mark Ryan, and Cas Cremers.
  IEEE Transactions on Information Forensics & Security, 2017.
  [bibtex]
  Research: Secure messaging; Formal verification of security protocols
• Automatically Detecting the Misuse of Secrets: Foundations, Design Principles, and ApplicationsAutomatically Detecting the Misuse of Secrets: Foundations, Design Principles, and Applications

  We develop foundations and several constructions for security protocols that can automatically detect, without false positives, if a secret (such as a key or password) has been misused. Such constructions can be used, e.g., to automatically shut down compromised services, or to automatically revoke misused secrets to minimize the effects of compromise. Our threat model includes malicious agents, (temporarily or permanently) compromised agents, and clones.

  Previous works have studied domain-specific partial solutions to this problem. For example, Google's Certificate Transparency aims to provide infrastructure to detect the misuse of a certificate authority's signing key, logs have been used for detecting endpoint compromise, and protocols have been proposed to detect cloned RFID/smart cards. Contrary to these existing approaches, for which the designs are interwoven with domain-specific considerations and which usually do not enable fully automatic response (i.e., they need human assessment), our approach shows where automatic action is possible. Our results unify, provide design rationales, and suggest improvements for the existing domain-specific solutions.

  Based on our analysis, we construct several mechanisms for the detection of misuse. Our mechanisms enable automatic response, such as revoking keys or shutting down services, thereby substantially limiting the impact of a compromise.

  In several case studies, we show how our mechanisms can be used to substantially increase the security guarantees of a wide range of systems, such as web logins, payment systems, or electronic door locks. For example, we propose and formally verify an improved version of Cloudflare's Keyless SSL protocol that enables key misuse detection.

  Details
  Kevin Milner, Cas Cremers, Jiangshan Yu, and Mark Ryan.
  IEEE CSF 2017, Proc. of the 30th IEEE Computer Security Foundations Symposium, 2017.
  [full version (eprint)] [bibtex]
  Research: Secure messaging; Formal verification of security protocols

Tools and resources

• Clone-detection Tamarin models
• Security standardisation contributions, including MLS

Related research

• Key exchange and group key establishment
• Post-compromise security

Complete chronological publication list