José Bacelar Almeida
Universidade do Minho, Braga, Portugal; University of Porto (FCUP), Porto, Portugal

Manuel Barbosa
University of Porto (FCUP), Porto, Portugal; INESC TEC, Porto, Portugal

Gilles Barthe
Max Planck Institute for Security and Privacy, Bochum, Germany; IMDEA Software Institute, Madrid, Spain

Benjamin Grégoire
Université Côte d’Azur, Inria, France

Vincent Laporte
Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

Jean-Christophe Léchenet
Université Côte d’Azur, Inria, France

Tiago Oliveira
Max Planck Institute for Security and Privacy, Bochum, Germany

Hugo Pacheco
University of Porto (FCUP), Porto, Portugal; INESC TEC, Porto, Portugal

Miguel Quaresma
Max Planck Institute for Security and Privacy, Bochum, Germany

Peter Schwabe
Max Planck Institute for Security and Privacy, Bochum, Germany; Radboud University, Nijmegen, The Netherlands

Antoine Séré
École Polytechnique, Paris, France

Pierre-Yves Strub
Meta, Paris, France

Keywords: High-assurance cryptography, lattice-based KEMs, NIST PQC, Jasmin, EasyCrypt

Abstract

In this paper we 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 give a (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. We present high-assurance open-source implementations of Kyber written in the Jasmin language, along with machine-checked proofs that they are functionally correct with respect to the EasyCrypt specification. We describe a number of improvements to the EasyCrypt and Jasmin frameworks that were needed for this implementation and verification effort, and we present detailed benchmarks of our implementations, showing that our code achieves performance close to existing hand-optimized implementations in C and assembly.