José Bacelar Almeida
Universidade do Minho

Santiago Arranz Olmos
MPI-SP

Manuel Barbosa
U. Porto & MPI-SP

Gilles Barthe
MPI-SP & IMDEA Software Institute

Francois Dupressoir
University of Bristol, UK

Benjamin Gregoire
Université Côte d’Azur, Inria, France

Vincent Laporte
Université de Lorraine, CNRS, Inria, LORIA, France

Jean-Christophe Léchenet
Université Côte d’Azur, Inria, France

Cameron Low
University of Bristol, UK

Tiago Oliveira
MPI-SP

Hugo Pacheco
U. Porto

Miguel Quaresma
MPI-SP

Peter Schwabe
MPI-SP & Radboud University

Pierre-Yves Strub
PQShield SAS

Keywords: Formal verification, ML-KEM, Kyber, IND-CCA, Functional Correctness

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 FujisakiOkamoto transform in the Random Oracle Model (ROM), which follows closely (but not exactly) Hofheinz, Hövelmanns 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.