tfaoliveira/mlkem-crypto24 repository overview

This image contains a prepared environment to use the artifact of the paper: Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt: https://eprint.iacr.org/2024/843⁠

To use this artifact:

$ docker pull tfaoliveira/mlkem-crypto24
$ docker run -it tfaoliveira/mlkem-crypto24 bash
$ less README.md
$ make check
$ make test
$ make bench
$ make example

The command less README.md allows you to inspect the README.md file, which contains some notes on how the proofs are organized.

The command make check lets you check the corresponding EasyCrypt proofs. This process takes around 1.5 hours on common CPUs (for example, eight cores, relatively recent Intel i7), and progress is shown on the terminal.

You can also find the artifact at https://artifacts.formosa-crypto.org/⁠