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

DOI:

https://doi.org/10.46586/tches.v2023.i3.164-193

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.

Downloads

Published

2023-06-09

How to Cite

Bacelar Almeida, J., Barbosa, M., Barthe, G., Grégoire, B., Laporte, V., Léchenet, J.-C., … Strub, P.-Y. (2023). Formally verifying Kyber: Episode IV: Implementation correctness. IACR Transactions on Cryptographic Hardware and Embedded Systems, 2023(3), 164–193. https://doi.org/10.46586/tches.v2023.i3.164-193

Issue

Vol. 2023 No. 3

Section

Articles

License

Copyright (c) 2023 José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.