Paper 2024/843
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt
, Universidade do Minho, Portugal, INESC TEC, Porto, Portugal, University of Porto (FCUP), Portugal, INESC TEC, Porto, Portugal, Max Planck Institute for Security and Privacy, Bochum, Germany, Max Planck Institute for Security and Privacy, Bochum, Germany, IMDEA Software Institute, Spain, University of Bristol, UK, Université Côte d’Azur, Inria, France, Université de Lorraine, CNRS, Inria, LORIA, France, Université Côte d’Azur, Inria, France, SandboxAQ, USA, University of Porto (FCUP), Portugal, INESC TEC, Porto, Portugal, Max Planck Institute for Security and Privacy, Bochum, Germany, PQShield, FranceAbstract
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 MLKEM down to (a variant of) Module-LWE. We discuss how they are built modularly by leveraging various EasyCrypt features.
Metadata
- Available format(s)
-
PDF
- Category
- Public-key cryptography
- Publication info
- A major revision of an IACR publication in CRYPTO 2024
- Keywords
- Formal verificationML-KEMKyberIND-CCAFunctional Correctness
- Contact author(s)
-
jba @ di uminho pt
santiago arranz-olmos @ mpi-sp org
mbb @ fc up pt
gilles barthe @ mpi-sp org
f dupressoir @ bristol ac uk
benjamin gregoire @ inria fr
vincent laporte @ inria fr
jean-christophe lechenet @ inria fr
cameron low 2018 @ bristol ac uk
tiago oliveira @ sandboxquantum com
hpacheco @ fc up pt
miguel quaresma @ mpi-sp org
peter @ cryptojedi org
pierre-yves strub @ pqshield com - History
- 2024-05-31: approved
- 2024-05-29: received
- See all versions
- Short URL
- https://ia.cr/2024/843
- License
-
CC0
BibTeX
@misc{cryptoeprint:2024/843,
author = {José Bacelar Almeida and Santiago Arranz Olmos and Manuel Barbosa and Gilles Barthe and François Dupressoir and Benjamin Grégoire 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},
title = {Formally verifying Kyber Episode V: Machine-checked {IND}-{CCA} security and correctness of {ML}-{KEM} in {EasyCrypt}},
howpublished = {Cryptology {ePrint} Archive, Paper 2024/843},
year = {2024},
url = {https://eprint.iacr.org/2024/843}
}
