International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Formally Verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt

Authors:
José Bacelar Almeida , Universidade do Minho and INESC TEC
Santiago Arranz Olmos , Max Planck Institute for Security and Privacy
Manuel Barbosa , University of Porto (FCUP) and INESC TEC and Max Planck Institute for Security and Privacy
Gilles Barthe , Max Planck Institute for Security and Privacy and IMDEA Software Institute
Francois Dupressoir , University of Bristol
Benjamin Gregoire , Université Côte d’Azur, Inria, France
Vincent Laporte , Université de Lorraine, CNRS, Inria, LORIA, Nancy, France
Jean-Christophe Léchenet , Université Côte d’Azur, Inria, France
Cameron Low , University of Bristol
Tiago Oliveira , SandboxAQ
Hugo Pacheco , University of Porto (FCUP) and INESC TEC
Miguel Quaresma , Max Planck Institute for Security and Privacy
Peter Schwabe , Max Planck Institute for Security and Privacy and Radboud University
Pierre-Yves Strub , PQShield SAS
Download:
DOI: 10.1007/978-3-031-68379-4_12 (login may be required)
Search ePrint
Search Google
Presentation: Slides
Conference: CRYPTO 2024
Abstract: We present a formally verified proof of the correctness and IND-CCA security of ML-KEM, the Kyber-based Key Encapsulation Mechanism (KEM) undergoing standardization by NIST. The proof is machine-checked in EasyCrypt and it includes: 1) A formalization of the correctness (decryption failure probability) and IND-CPA security of the Kyber base public-key encryption scheme, following Bos et al. at Euro S&P 2018; 2) A formalization of the relevant variant of the Fujisaki-Okamoto transform in the Random Oracle Model (ROM), which follows closely (but not exactly) Hofheinz, Hovelmanns and Kiltz at TCC 2017; 3) A proof that the IND-CCA security of the ML-KEM specification and its correctness as a KEM follows from the previous results; 4) Two formally verified implementations of ML-KEM written in Jasmin that are provably constant-time, functionally equivalent to the ML-KEM specification and, for this reason, inherit the provable security guarantees established in the previous points. The top-level theorems give self-contained concrete bounds for the correctness and security of ML-KEM down to (a variant of) Module-LWE. We discuss how they are built modularly by leveraging various EasyCrypt features.
BibTeX
@inproceedings{crypto-2024-34226,
  title={Formally Verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt},
  publisher={Springer-Verlag},
  doi={10.1007/978-3-031-68379-4_12},
  author={José Bacelar Almeida and Santiago Arranz Olmos and Manuel Barbosa and Gilles Barthe and Francois Dupressoir and Benjamin Gregoire and Vincent Laporte and Jean-Christophe Léchenet and Cameron Low and Tiago Oliveira and Hugo Pacheco and Miguel Quaresma and Peter Schwabe and Pierre-Yves Strub},
  year=2024
}