Official websites use .gov
A .gov website belongs to an official government organization in the United States.

Secure .gov websites use HTTPS
A lock ( ) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.


Formally Verifying Kyber Part I: Functional Correctness

April 19, 2023


Manuel Barbosa - University of Porto (FCUP); INESC TEC


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

Presented at

Crypto Reading Club talk on 2023-Apr-19

Parent Project

See: Crypto Reading Club

Related Topics

Security and Privacy: cryptography

Created April 05, 2023, Updated April 20, 2023