tfaoliveira/hakyber-ches23 repository overview

This image contains a prepared environment to use the artifact of the paper: Formally verifying Kyber Episode IV: Implementation correctness: https://eprint.iacr.org/2023/215.pdf⁠

To use this artifact:

$ docker pull tfaoliveira/hakyber-ches23
$ docker run -it tfaoliveira/hakyber-ches23 bash
$ cd hakyber/
$ less README.md
$ make check

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

The command make check lets you check the corresponding EasyCrypt proofs. This process takes around 70 minutes 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/⁠