Paper 2023/215

Formally verifying Kyber Episode IV: Implementation Correctness

José Bacelar Almeida, Universidade do Minho, INESC TEC
Manuel Barbosa, University of Porto (FCUP), INESC TEC
Gilles Barthe, Max Planck Institute for Security and Privacy, IMDEA Software
Benjamin Grégoire, Université Côte dAzur, French Institute for Research in Computer Science and Automation
Vincent Laporte, Université de Lorraine, French National Centre for Scientific Research, French Institute for Research in Computer Science and Automation
Jean-Christophe Léchenet, Université Côte d’Azur, French Institute for Research in Computer Science and Automation
Tiago Oliveira, Max Planck Institute for Security and Privacy
Hugo Pacheco, Universidade do Minho, INESC TEC
Miguel Quaresma, Max Planck Institute for Security and Privacy
Peter Schwabe, Max Planck Institute for Security and Privacy, Radboud University Nijmegen
Antoine Séré, École Polytechnique
Pierre-Yves Strub
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.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Published by the IACR in TCHES 2023
Keywords
High-assurance cryptographylattice-based KEMsNIST PQCJasminEasyCrypt
Contact author(s)
jba @ di uminho pt
mbb @ fc up pt
gilles barthe @ mpi-sp org
benjamin gregoire @ inria fr
vincent laporte @ inria fr
jean-christophe lechenet @ inria fr
tiago oliveira @ mpi-sp org
hpacheco @ fc up pt
miguel quaresma @ mpi-sp org
peter @ cryptojedi org
antoine sere @ protonmail com
pierre-yves @ strub nu
History
2023-04-24: revised
2023-02-17: received
See all versions
Short URL
https://ia.cr/2023/215
License
No rights reserved
CC0

BibTeX

@misc{cryptoeprint:2023/215,
      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},
      title = {Formally verifying Kyber Episode {IV}: Implementation Correctness},
      howpublished = {Cryptology {ePrint} Archive, Paper 2023/215},
      year = {2023},
      url = {https://eprint.iacr.org/2023/215}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.