Cas Cremers

Research topics / Applied cryptography

We develop and analyze cryptographic protocols using computational security definitions and proofs. Our work includes authenticated key exchange, secure messaging, password-based authentication, cryptographic primitives, and post-quantum protocols.

We also study how security models relate to one another, which assumptions their proofs require, and where their guarantees have limits. The papers below include work on computational proofs and security definitions, as well as analyses that connect these definitions to symbolic methods.

Suggested reading

Start with the security models and key exchange papers, or choose an application below. The final group covers tools and methods for mechanizing computational proofs.

Security models and key exchange

  1. 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 security definition matter.

    Research: Applied cryptography; Key exchange and group key establishment
  2. 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
  3. 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 examine how choices such as partnering and the number of Test queries affect key exchange definitions. We establish composition results and show how these choices affect the tightness of security reductions.

    Research: Applied cryptography; Protocol composition; Key exchange and group key establishment
  4. 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

Secure messaging and recovery after compromise

  1. 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
  2. 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 model Signal's key agreement and Double Ratchet as a multi-stage key exchange protocol. We define a security model for its ratcheting structure and prove security of the protocol core in that model.

    Research: Secure messaging; Post-compromise security; Applied cryptography; Key exchange and group key establishment
  3. 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

Password-based authentication

  1. 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
  2. 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

Security of cryptographic primitives

  1. The Provable Security of Ed25519: Theory and Practice Details
    Jacqueline Brendel, Cas Cremers, Dennis Jackson, and Mang Zhao.
    IEEE Symposium on Security & Privacy (Oakland), May 2021
    [eprint] [bibtex]

    We give detailed security proofs for variants of Ed25519, accounting for their encoding and verification rules. This establishes which signature guarantees can be used in proofs of protocols that rely on these variants.

    Research: Cryptographic primitives; Applied cryptography
  2. 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]

    We define computational binding properties for KEMs and prove relationships between them. Corresponding symbolic models help determine which properties a protocol requires from its KEM.

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

Cryptocurrency protocols

  1. A Holistic Security Analysis of Monero Transactions Details
    Cas Cremers, Julian Loss, and Benedikt Wagner.
    Eurocrypt 2024, May 2024.
    [eprint] [bibtex]

    We give a security model and modular proof for Monero's RingCT transaction system. We identify the properties required of its building blocks and prove that the concrete constructions meet these requirements in our models.

    Research: Applied cryptography

Computational verification and post-quantum security

  1. SoK: Computer-Aided Cryptography Details
    Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno.
    IEEE Symposium on Security & Privacy (Oakland), May 2021
    [pdf] [eprint] [bibtex]

    We survey computer-aided cryptography, including computational and symbolic security proofs, implementation correctness, and side-channel resistance. The comparison explains the scope and limitations of the different approaches.

    Research: Applied cryptography
  2. 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

Further reading

Complete chronological publication list