Formally verifying Kyber

Formally verifying Kyber

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...

Full description

Bibliographic Details
Main Authors: 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
Format: Article
Language:English
Published: Ruhr-Universität Bochum 2023-06-01
Series:Transactions on Cryptographic Hardware and Embedded Systems
Subjects:
High-assurance cryptography
lattice-based KEMs
NIST PQC
Jasmin
EasyCrypt
Online Access:https://tches.iacr.org/index.php/TCHES/article/view/10960

Internet

https://tches.iacr.org/index.php/TCHES/article/view/10960

Similar Items