Formally verifying Kyber: Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt - Université de Lorraine
Communication Dans Un Congrès Année : 2024

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

Vincent Laporte
Cameron Low
  • Fonction : Auteur
  • PersonId : 1387673
Tiago Oliveira
  • Fonction : Auteur
  • PersonId : 1387674
Pierre-Yves Strub
  • Fonction : Auteur
  • PersonId : 1387676

Résumé

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.
Fichier principal
Vignette du fichier
2024-843.pdf (1.41 Mo) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)
Licence

Dates et versions

hal-04595591 , version 1 (31-05-2024)
hal-04595591 , version 2 (05-09-2024)

Licence

Identifiants

Citer

José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, et al.. Formally verifying Kyber: Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. Crypto 2024, International Association for Cryptologic Research, Aug 2024, Santa Barbara (CA), United States. ⟨10.1007/978-3-031-68379-4_12⟩. ⟨hal-04595591v2⟩
224 Consultations
131 Téléchargements

Altmetric

Partager

More