Cas Cremers

Research topics / Security protocol standards

We use formal methods and cryptographic analysis to evaluate and improve security protocol standards. Our work includes TLS 1.3, Messaging Layer Security (MLS), SPDM, and the ISO/IEC standards for entity authentication and key establishment. We also study authentication in mobile networks (5G-AKA), wireless networks (WPA2), industrial control systems (DNP3), and the web (FIDO2). Related work includes the design and deployment of DP-3T for privacy-preserving contact tracing.

We analyze both the guarantees provided by a protocol and the assumptions it makes about its environment. Interactions between protocol modes, shared keys, and underlying communication channels can affect these guarantees. Our work includes analyses during standardisation, identification of weaknesses, and verified repairs.

Contributions to security standards

Our standardisation work includes co-authoring guidance, helping initiate new protocols, and contributing analyses and repairs during standards development.

  1. RFC 8937: co-authorship

    Cremers co-authored Randomness Improvements for Security Protocols, which builds on our research on limiting the impact of unreliable randomness.

  2. Messaging Layer Security (MLS): initiation and contributions

    Cremers was a co-initiator and is a listed contributor to MLS (RFC 9420 and RFC 9750). Our work on asynchronous group messaging helped motivate its development; subsequent work analyzes the security of the resulting protocol.

  3. TLS 1.3: analysis during development

    Cas Cremers is a listed contributor to RFC 8446. Our formal analyses of drafts helped identify weaknesses and informed the standard’s development.

  4. SPDM: verified repairs

    Our analysis of SPDM 1.2 identified a cross-protocol attack on pre-shared-key authentication and provided a verified repair adopted in the standard. See the security advisory and CVE-2023-31127.

  5. ISO/IEC 9798 and ISO/IEC 11770: improvements to authentication and key establishment

    Our analyses identified weaknesses and incorrect security claims, and contributed repairs and improvements to these standards.

The reading guide below explains the research behind these contributions. The standardisation record on the publications page also collects supporting papers and historical material.

Suggested reading

Start with the overview of security standardisation, or choose a protocol or standard below. Further reading includes earlier analyses, journal versions, and additional case studies.

Overview

Security protocol standards let independently developed systems authenticate peers and protect their communications. Their security depends on precise specifications of the protocol, its goals, and the adversary’s capabilities.

  1. Improving the Security of Cryptographic Protocol StandardsImproving the Security of Cryptographic Protocol Standards

    Despite being carefully designed, cryptographic protocol standards often turn out to be flawed. Integrating unambiguous security properties, clear threat models, and formal methods into the standardization process can improve protocol security.

     Details
    David Basin, Cas Cremers, Kunihiko Miyazaki, Saša Radomirović, and Dai Watanabe.
    IEEE Security & Privacy, 2015.
    [preprint] [bibtex]

    We discuss how explicit security properties, clear threat models, and formal methods can improve the standardisation process.

    Research: Security protocol standards

TLS 1.3

TLS 1.3 (RFC 8446) establishes authenticated, encrypted channels between applications. It protects HTTPS connections and other Internet traffic against eavesdropping and tampering.

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

Messaging Layer Security (MLS)

MLS (RFC 9420) is an IETF protocol for establishing and updating group keys for end-to-end encrypted messaging. GSMA’s RCS specification uses MLS for end-to-end encryption between Apple Messages and Google Messages, which began rolling out in May 2026 on supported devices and carriers.

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

SPDM

DMTF’s Security Protocol and Data Model (SPDM) supports authentication, attestation, and key exchange between hardware components. It is part of the PCI Express security stack, providing authentication and key exchange for securing communication with devices.

  1. Breaking and Provably Restoring Authentication: A Formal Analysis of SPDM 1.2 including Cross-Protocol Attacks Details
    Cas Cremers, Alexander Dax, and Aurora Naska.
    ACM CCS 2025, Taipei, October 2025.
    [eprint] [bibtex]

    We analyze interactions between SPDM 1.2's modes and find a cross-protocol attack on pre-shared-key authentication. We prove a repair in our model; the fix was adopted in the standard.

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

FIDO2 and WebAuthn

FIDO2 combines W3C’s WebAuthn interface with the FIDO Alliance’s Client to Authenticator Protocol (CTAP) for public-key user authentication. These specifications underpin passkeys and security-key authentication, enabling phishing-resistant sign-in without sending a reusable password to the service.

  1. FIDO2, CTAP 2.1, and WebAuthn 2: Provable Security and Post-Quantum Instantiation Details
    Nina Bindel, Cas Cremers, and Mang Zhao.
    IEEE Symposium on Security & Privacy (Oakland), May 2023.
    [eprint] [bibtex]

    We analyze FIDO2's CTAP 2.1 and WebAuthn 2, including token binding and user verification. We also study conditions and extensions for post-quantum instantiation.

    Research: Security protocol standards; Applied cryptography

5G-AKA

5G-AKA is an authentication and key agreement protocol in 3GPP’s 5G security architecture. It authenticates subscribers and networks and establishes key material used to protect mobile communications, including when a subscriber is roaming.

  1. Component-Based Formal Analysis of 5G-AKA: Channel Assumptions and Session ConfusionComponent-Based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion

    The 5G mobile telephony standards are nearing completion; upon adoption these will be used by billions across the globe. Ensuring the security of 5G communication is of the utmost importance, building trust in a critical component of everyday life and national infrastructure.We perform fine-grained formal analysis of 5G's main authentication and key agreement protocol (AKA), and provide the first models to explicitly consider all parties defined by the protocol specification. Our analysis reveals that the security of 5G-AKA critically relies on unstated assumptions on the inner workings of the underlying channels. In practice this means that following the 5G-AKA specification, a provider can easily and `correctly' implement the standard insecurely, leaving the protocol vulnerable to a security-critical race condition. We provide the first models and analysis considering component and channel compromise in 5G, whose results further demonstrate the fragility and subtle trust assumptions of the \aka protocol.We propose formally verified fixes to the encountered issues, and have worked with 3GPP to ensure these fixes are adopted.

     Details
    Cas Cremers and Martin Dehnel-Wild.
    NDSS 2019, The Network and Distributed System Security Symposium, San Diego, February 2019.
    [pdf] [bibtex]

    We show that 5G-AKA relies on unstated channel assumptions, exposing implementations to a session-confusion attack. We propose formally verified fixes and worked with 3GPP on their adoption.

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

DNP3

DNP3 (IEEE 1815) connects control stations and field devices in electricity grids and other critical infrastructure, including water utilities and transport systems. Its Secure Authentication protocol protects critical control messages against forgery, making its security relevant to the operation of physical systems.

  1. Secure Authentication in the Grid: A Formal Analysis of DNP3 SAv5Secure Authentication in the Grid: A Formal Analysis of DNP3 SAv5

    Most of the world’s power grids are controlled remotely. Their control messages are sent over potentially insecure channels, driving the need for an authentication mechanism. The main communication mechanism for power grids and other utilities is defined by an IEEE standard, referred to as DNP3; this includes the Secure Authentication v5 (SAv5) protocol, which aims to ensure that messages are authenticated.

    We provide the first security analysis of the complete DNP3: SAv5 protocol. Previous work has considered the message-passing sub-protocol of SAv5 in isolation, and considered some aspects of the intended security properties. In contrast, we formally model and analyse the complex composition of the protocol’s sub-protocols. In doing so, we consider the full state machine, the protocol’s asymmetric mode, and the possibility of cross-protocol attacks. Furthermore, we model fine-grained security properties that closely match the standard’s intended security properties. For our analysis, we leverage the TAMARIN prover for the symbolic analysis of security protocols.

    Our analysis shows that the core DNP3: SAv5 design meets its intended security properties. Notably, we show that a previously reported attack does not apply to the standard. However, our analysis also leads to several concrete recommendations for improving future versions of the standard.

     Details
    Cas Cremers, Martin Dehnel-Wild, and Kevin Milner.
    Journal of Computer Security, 2018.
    [pdf] [bibtex]

    We analyze DNP3 SAv5 using Tamarin, including its asymmetric mode and interactions between sub-protocols. The core design meets its intended security properties in our model; we also give recommendations for future versions.

    Research: Security protocol standards

Contact tracing (DP-3T)

DP-3T is a decentralized proximity-tracing design in which phones exchange temporary Bluetooth identifiers and assess possible exposure locally. Developed during the COVID-19 pandemic, its approach also informed Apple and Google’s Exposure Notification system, connecting protocol privacy to public-health deployment.

  1. Decentralized Privacy-Preserving Proximity Tracing Details
    Carmela Troncoso, Mathias Payer, Jean-Pierre Hubaux, Marcel Salathé, James R. Larus, Edouard Bugnion, Wouter Lueks, Theresa Stadler, Apostolos Pyrgelis, Daniele Antonioli, Ludovic Barman, Sylvain Chatel, Kenny Paterson, Srdjan Čapkun, David Basin, Jan Beutel, Dennis Jackson, Marc Roeschlin, Patrick Leu, Bart Preneel, Nigel Smart, Aysajan Abidin, Seda Gürses, Michael Veale, Cas Cremers, Michael Backes, Nils Ole Tippenhauer, Reuben Binns, Ciro Cattuto, Alain Barrat, Dario Fiore, Manuel Barbosa, Rui Oliveira, and José Pereira.
    [DP-3T project webpage] [Arxiv page of whitepaper] [pdf] [bibtex]

    We describe and analyze DP-3T, a decentralized system for privacy-preserving proximity tracing. Phones exchange ephemeral identifiers and assess exposure locally, reducing the information disclosed to a central server.

    Research: Security protocol standards
  2. Deploying decentralized, privacy-preserving proximity tracing Details
    Carmela Troncoso, Dan Bogdanov, Edouard Bugnion, Sylvain Chatel, Cas Cremers, Seda Gürses, Jean-Pierre Hubaux, Dennis Jackson, James R. Larus, Wouter Lueks, Rui Oliveira, Mathias Payer, Bart Preneel, Apostolos Pyrgelis, Marcel Salathé, Theresa Stadler, and Michael Veale.
    Communications of the ACM, September 2022
    [pdf] [bibtex] [online with video]

    We discuss lessons from deploying decentralized, privacy-preserving proximity tracing during the COVID-19 pandemic. This complements the protocol design with experience from deployment.

    Research: Security protocol standards

ISO/IEC authentication and key management

ISO/IEC 9798 specifies mechanisms for entity authentication, while ISO/IEC 11770 covers key management. These families provide reusable mechanisms for establishing who a peer is and managing the keys needed for secure communication.

  1. Provably Repairing the ISO/IEC 9798 Standard for Entity AuthenticationProvably Repairing the ISO/IEC 9798 Standard for Entity Authentication

    We formally analyze the family of entity authentication protocols defined by the ISO/IEC 9798 standard and find numerous weaknesses, both old and new, including some that violate even the most basic authentication guarantees. We analyze the cause of these weaknesses, propose repaired versions of the protocols, and provide automated, machine-checked proofs of the correctness of the resulting protocols. From an engineering perspective, we propose two design principles for security protocols that suffice to prevent all the weaknesses. Moreover, we show how modern verification tools can be used for falsification and certified verification of security standards. Based on our findings, the ISO working group responsible for the ISO/IEC 9798 standard has released an updated version of the standard.

     Details
    David Basin, Cas Cremers, and Simon Meier.
    Journal of Computer Security, 2013.
    [preprint] [pdf] [bibtex]

    We identify weaknesses in ISO/IEC 9798's entity authentication protocols and give repairs with machine-checked proofs. Our recommendations led to updates to the standard.

    Research: Security protocol standards
  2. Improving the ISO/IEC 11770 standard for key management techniquesImproving the ISO/IEC 11770 standard for key management techniques

    We provide the first systematic analysis of the ISO/IEC 11770 standard for key management techniques (2009, 2009), which describes a set of key establishment, key agreement, and key transport protocols. We analyse the claimed security properties, as well as additional modern requirements on key management protocols, for over 30 protocols and their variants. Our formal, tool-supported analysis of the protocols uncovers several incorrect claims in the standard. We provide concrete suggestions for improving the standard.

     Details
    Cas Cremers and Marko Horvat.
    International Journal of Information Security, 2015.
    [pdf] [bibtex]

    We analyze over 30 key management protocols and variants from ISO/IEC 11770, identify incorrect security claims, and propose improvements.

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

Randomness improvements (RFC 8937)

RFC 8937 describes how to strengthen random-number generation using long-term private keys. This IRTF guidance aims to reduce the impact of weak or subverted randomness in implementations of TLS and related security protocols.

  1. Limiting the impact of unreliable randomness in deployed security protocols Details
    Liliya Akhmetzyanova, Cas Cremers, Luke Garratt, Stanislav Smyshlyaev, and Nick Sullivan.
    IEEE CSF 2020, Boston, USA, June 2020.
    This work is the foundation of the IETF "Randomness Improvements for Security Protocols" standard.
    [full version] [bibtex] [RFC 8937]

    We develop a construction to reduce the impact of unreliable randomness in deployed protocols. This work forms the basis of RFC 8937, Randomness Improvements for Security Protocols.

    Research: Security protocol standards; Applied cryptography

Noise

The Noise Protocol Framework constructs Diffie-Hellman key exchange protocols from reusable handshake patterns. Its protocols are used in systems including WireGuard, WhatsApp, and Lightning, with different patterns offering different authentication and privacy guarantees.

  1. 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 gives formal meaning to the specification's security levels and identifies missing assumptions and differences between patterns.

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

Further reading

Tools and resources

Complete chronological publication list