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

Back
Categories: Research Papers
Date: 04/06/2024
Venue: Crypto 2024
Authors: Pierre-Yves Strub, PQShield, France, José Bacelar Almeida, Universidade do Minho, Portugal, INESC TEC, Porto, Portugal, Santiago Arranz Olmos, Max Planck Institute for Security and Privacy, Bochum, Germany, Manuel Barbosa, University of Porto (FCUP), Portugal, INESC TEC, Porto, Portugal, Max Planck Institute for Security and Privacy, Bochum, Germany, Gilles Barthe, Max Planck Institute for Security and Privacy, Bochum, Germany, IMDEA Software Institute, Spain, François Dupressoir, University of Bristol, UK, Benjamin Grégoire, 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, SandboxAQ, USA, Hugo Pacheco, University of Porto (FCUP), Portugal, INESC TEC, Porto, Portugal, Miguel Quaresma, Max Planck Institute for Security and Privacy, Bochum, Germany, Peter Schwabe, Max Planck Institute for Security and Privacy, Bochum, Germany, Radboud University, Nijmegen, The Netherlands

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.

Preprint