International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Formally verifying Kyber: Episode IV: Implementation correctness

Authors:
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
Download:
DOI: 10.46586/tches.v2023.i3.164-193
URL: https://tches.iacr.org/index.php/TCHES/article/view/10960
Search ePrint
Search Google
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.
BibTeX
@article{tches-2023-33286,
  title={Formally verifying Kyber: Episode IV: Implementation correctness},
  journal={IACR Transactions on Cryptographic Hardware and Embedded Systems},
  publisher={Ruhr-Universität Bochum},
  volume={2023, Issue 3},
  pages={164-193},
  url={https://tches.iacr.org/index.php/TCHES/article/view/10960},
  doi={10.46586/tches.v2023.i3.164-193},
  author={José Bacelar Almeida and Manuel Barbosa and Gilles Barthe and Benjamin Grégoire and Vincent Laporte and Jean-Christophe Léchenet and Tiago Oliveira and Hugo Pacheco and Miguel Quaresma and Peter Schwabe and Antoine Séré and Pierre-Yves Strub},
  year=2023
}