Abstract. In this talk we will present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We will first briefly look at the tool chain used in the development, including a short description of Jasmin and EasyCrypt and how we used them in this work. We will then present the (readable) formal specification of Kyber in the EasyCrypt proof assistant, which is syntactically very close to the pseudocode description of the scheme as given in the most recent version of the NIST submission (and we expect also close to a future standard or RFC for Kyber). We then describe the high-assurance open-source implementations of Kyber written in the Jasmin language, along with a high-level view of the machine-checked proofs that the low-level code is functionally correct with respect to the EasyCrypt specification. We will conclude the talk with a discussion of lessons learned during this project.
The talk is based on joint work with José Bacelar Almeida, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré and Pierre-Yves Strub.
Suggested readings: ia.cr/2023/215, ia.cr/2022/1270, ia.cr/2019/1155, formosa-crypto.org, doi.org/10.1109/SP40000.2020.00028
