Paper 2024/843
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt
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 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}
}