Paper 2023/1933

Keeping Up with the KEMs: Stronger Security Notions for KEMs and automated analysis of KEM-based protocols

Cas Cremers, Helmholtz Center for Information Security
Alexander Dax, Helmholtz Center for Information Security
Niklas Medinger, Helmholtz Center for Information Security

Key Encapsulation Mechanisms (KEMs) are a critical building block for hybrid encryption and modern security protocols, notably in the post-quantum setting. Given the asymmetric public key of a recipient, the primitive establishes a shared secret key between sender and recipient. In recent years, a large number of abstract designs and concrete implementations of KEMs have been proposed, e.g., in the context of the NIST process for post-quantum primitives. In this work, we (i) establish stronger security notions for KEMs, and (ii) develop a symbolic analysis method to analyze security protocols that use KEMs. First, we generalize existing security notions for KEMs in the computational setting, introduce several stronger security notions, and prove their relations. Our new properties formalize in which sense outputs of the KEM uniquely determine, i.e., bind, other values. Our new binding properties can be used, e.g., to prove the absence of attacks that were not captured by prior security notions, such as re-encapsulation attacks. Second, we develop a family of fine-grained symbolic models that correspond to our hierarchy of computational security notions, and are suitable for the automated analysis of KEM-based security protocols. We encode our models as a library in the framework of the Tamarin prover. Given a KEM-based protocol, our approach can automatically derive the minimal binding properties required from the KEM; or, if also given a concrete KEM, can analyze if the protocols meets its security goals. In case studies, Tamarin automatically discovers, e.g., that the key exchange protocol proposed in the original Kyber paper requires stronger properties from the KEM than were proven in the paper.

Available format(s)
Public-key cryptography
Publication info
KEMKey Encapsulation MechanismAKEKey ExchangeRobustnessBindingSymbolic ModelTamarinAutomated Analysis
Contact author(s)
cremers @ cispa de
alexander dax @ cispa de
niklas medinger @ cispa de
2024-04-03: last of 9 revisions
2023-12-20: received
See all versions
Short URL
Creative Commons Attribution-ShareAlike


      author = {Cas Cremers and Alexander Dax and Niklas Medinger},
      title = {Keeping Up with the KEMs: Stronger Security Notions for KEMs and automated analysis of KEM-based protocols},
      howpublished = {Cryptology ePrint Archive, Paper 2023/1933},
      year = {2023},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.