International Association for Cryptologic Research

International Association
for Cryptologic Research

Crypto 2024

Formally Verifying Kyber:

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


README

Header

This is the artifact for the following IACR CRYPTO 2024 publication.

Title:

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

Authors:

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, 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.

Contents

The artifact is structered as follows:

Locations of theorems in paper:

Section 4: K-PKE correctness and IND-CPA security

The following theorems state the proved security and correctness properties
for the PKE underlying ML-KEM. They can be instantiated with any parameter set.

Section 5: Formalizing the FO Transform used in ML-KEM

The following theorems state the proved security and correctness properties
for the Fujisaki-Okamoto transformation used in ML-KEM.
They can be instantiated with any parameter set.

Section 6: Main result: Security of ML-KEM

The following theorems show that the general results above apply to the ML-KEM-768 specification.

Section 7:

The following theorems show that the ML-KEM-768 specification is functionally equivalent to the two
Jasmin implementations, which means that these implementations inherit the security properties
of the specification.

Checking the EasyCrypt's formal proofs

Easycrypt is an automated proof assistant for constructing and
verifying game-based cryptographic proofs.

Installing EasyCrypt

Easycrypt can be installed using one of two ways:

We strongly suggest using the Docker image file.

Using Docker

This artifact contains a Dockerfile which sets up a container with
Easycrypt along with the contents of the artifact.For information on
the installation of Docker see https://docs.docker.com/get-docker/.

To setup Easycrypt using Docker, run:

docker build -t episode_v .

You can then run the Docker image with:

docker run -it episode_v
make check
make test
make bench
make example

The previous commands do the following:
* make check extracts from Jasmin to EasyCrypt and checks the proofs.
* make test executes the available tests for both implementations, reference and avx2
* make bench executes the available benchmarks
* make example builds two example executables that show how the these implementations can be integrated in other libraries. The relevant files are in directories ./code/jasmin/mlkem_ref/example/ and ./code/jasmin/mlkem_avx2/example/: in there, you can find an api.h header file; an example.c file; and Makefile. Running make on the directores builds the corresponding jkem.s file (the formally verified assembly code) and an executable named example, which prints an example execution trace to the terminal. The main Makefile just runs make in said directories.

Remarks: please note that running benchmarks inside a container
will impact the running time.

Using Nix & OPAM (manual mode)

For information on the installation of the Nix package manager see
https://nixos.org/download.

Via Nix & OPAM (inside the artifact directory):

# 1. If you do not have opam configured already:

## On Debian and derivatives
apt install opam gcc clang

## On Mac:
brew install opam

## Then, on all platforms:

# 2. Install EasyCrypt
cd easycrypt
make nix-build
install -D result/bin/easycrypt /usr/local/bin/
install -D result/bin/why3 /usr/local/bin/

opam install -y opam-depext

# 3. Install external provers for EasyCrypt
opam init --disable-sandboxing

## Alt-Ergo
opam pin add -n alt-ergo 2.5.3
opam depext -y alt-ergo.2.5.3
opam install -y alt-ergo.2.5.3

## Z3
opam depext -y z3.4.8.17
opam install -y z3.4.8.17

eval $(opam env)

## CVC4

### On Debian and derivatives
apt install cvc4

### On macOS (intel)
brew tap cvc4/cvc4
brew install cvc4/cvc4/cvc4

### On macOS (Silicon), you have to download it directly from
###   https://cvc4.github.io/
### at version 1/8
###
### You have to download the x64 version and configure Rosetta 2
### to make it executable on macOS Silicon

# 4. Configure EasyCrypt
# (you have to run it each time you add/change an external prover)

easycrypt why3config

Checking the proofs

Requirements: install Easycrypt

The proof directory contains the correctness and equivalence proofs,
which can be checked by running make checkec from this directory.