Cas Cremers

Research topics / Cryptographic primitives

We study the security properties of cryptographic primitives and how these properties affect the protocols that use them. Our work includes signatures, key encapsulation mechanisms (KEMs), Diffie-Hellman groups, authenticated encryption with associated data (AEAD), and hash functions.

A protocol may require properties beyond a primitive’s usual security definition. For example, unforgeability alone does not guarantee all the binding properties that a protocol may expect from a signature. We develop definitions, proofs, and symbolic models that make these distinctions explicit, and use them to analyze protocols with concrete choices of primitives.

Suggested reading

The following papers study the guarantees offered by different primitives and how to account for them in protocol analysis, and introduce novel security properties.

Signatures

  1. Seems Legit: Automated Analysis of Subtle Attacks on Protocols that use Signatures Details
    Dennis Jackson, Cas Cremers, Katriel Cohn-Gordon, and Ralf Sasse.
    ACM CCS 2019, London, UK, November 2019.
    [full version] [bibtex]

    Unforgeability alone does not provide all the signature properties that a protocol may require. We develop symbolic models that capture these differences and use Tamarin to find attacks missed by traditional models.

    Research: Cryptographic primitives; Applied cryptography
  2. BUFFing signature schemes beyond unforgeability and the case of post-quantum signatures Details
    Cas Cremers, Samed Düzlü, Rune Fiedler, Marc Fischlin, and Christian Janson.
    IEEE Symposium on Security & Privacy (Oakland), May 2021.
    [pdf] [eprint] [bibtex]

    We study signature properties beyond unforgeability, provide cryptographic definitions, and give transformations that provide stronger guarantees. We also analyze these properties for post-quantum signature candidates.

    Research: Cryptographic primitives; Applied cryptography
  3. 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 security proofs for variants of Ed25519, accounting for their encoding and verification details. The analysis clarifies which guarantees the different variants provide to protocols that use them.

    Research: Cryptographic primitives; Applied cryptography
  4. An Extended Hierarchy of Security Notions for Threshold Signature Schemes and Automated Analysis of Protocols That Use Them Details
    Cas Cremers, Aleksi Peltonen, and Mang Zhao.
    ACM CCS 2026, The Hague, November 2026.
    [eprint]

    We develop a hierarchy of security notions for threshold signatures, including corruption and malicious key generation. We use this hierarchy to analyze protocols that depend on different threshold signature guarantees.

    Research: Cryptographic primitives; Applied cryptography

Key encapsulation mechanisms (KEMs)

  1. 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 binding properties for KEMs and establish their relationships. Corresponding symbolic models allow Tamarin to identify which binding properties a protocol requires from its KEM.

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

Diffie-Hellman groups

  1. Prime, Order Please! Revisiting Small Subgroup and Invalid Curve Attacks on Protocols using Diffie-Hellman Details
    Cas Cremers and Dennis Jackson.CSF Distinguished Paper Award
    IEEE CSF 2019, 32nd IEEE Computer Security Foundations Symposium, Hoboken, NJ, USA, June 2019.
    [pdf] [bibtex]

    We model group structure beyond the usual prime-order abstraction, including small subgroups and invalid curve points. This enables automated analysis of attacks and proposed countermeasures in protocols that use Diffie-Hellman.

    Research: Formal verification of security protocols; Cryptographic primitives; Key exchange and group key establishment

Authenticated encryption (AEAD)

  1. Automated Analysis of Protocols that use Authenticated Encryption: How Subtle AEAD Differences can impact Protocol Security Details
    Cas Cremers, Alexander Dax, Charlie Jacomme, and Mang Zhao.USENIX Distinguished Paper Award
    USENIX 2023, August 2023.
    [eprint] [pdf] [bibtex]

    We develop symbolic models that distinguish the guarantees of different AEAD schemes. These models allow automated analysis of protocol attacks that exploit the choice of authenticated encryption scheme.

    Research: Cryptographic primitives; Applied cryptography

Hash functions

  1. Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses Details
    Vincent Cheval, Cas Cremers, Alexander Dax, Lucca Hirschi, Charlie Jacomme, and Steve Kremer.USENIX Distinguished Paper Award
    USENIX 2023, August 2023.
    [eprint] [pdf] [bibtex]

    We model weaknesses in hash functions and their effects on protocol security. Extensions to Tamarin and ProVerif enable automated discovery of attacks that idealized hash models can miss.

    Research: Cryptographic primitives; Applied cryptography

Further reading

Tools and resources

Complete chronological publication list