TY - JOUR
T1 - Formally verifying Kyber Episode IV
T2 - Implementation correctness
AU - Almeida, José Bacelar
AU - Barbosa, Manuel
AU - Barthe, Gilles
AU - Grégoire, Benjamin
AU - Laporte, Vincent
AU - Léchenet, Jean Christophe
AU - Oliveira, Tiago
AU - Pacheco, Hugo
AU - Quaresma, Miguel
AU - Schwabe, Peter
AU - Séré, Antoine
AU - Strub, Pierre Yves
N1 - Publisher Copyright:
© 2023 Ruhr-University of Bochum.
PY - 2023/6/9
Y1 - 2023/6/9
N2 - 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.
AB - 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.
KW - EasyCrypt
KW - High-assurance cryptography
KW - Jasmin
KW - NIST PQC
KW - lattice-based KEMs
U2 - 10.46586/tches.v2023.i3.164-193
DO - 10.46586/tches.v2023.i3.164-193
M3 - Article
AN - SCOPUS:85163223028
SN - 2569-2925
VL - 2023
SP - 164
EP - 193
JO - IACR Transactions on Cryptographic Hardware and Embedded Systems
JF - IACR Transactions on Cryptographic Hardware and Embedded Systems
IS - 3
ER -