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...
| Main Authors: | , , , , , , , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ruhr-Universität Bochum
2023-06-01
|
| Series: | Transactions on Cryptographic Hardware and Embedded Systems |
| Subjects: | |
| Online Access: | https://tches.iacr.org/index.php/TCHES/article/view/10960 |
| _version_ | 1797807407396552704 |
|---|---|
| author | 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 |
| author_facet | 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 |
| author_sort | José Bacelar Almeida |
| collection | DOAJ |
| description |
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.
|
| first_indexed | 2024-03-13T06:22:01Z |
| format | Article |
| id | doaj.art-c082783eb324437292b239d88846e0e8 |
| institution | Directory Open Access Journal |
| issn | 2569-2925 |
| language | English |
| last_indexed | 2024-03-13T06:22:01Z |
| publishDate | 2023-06-01 |
| publisher | Ruhr-Universität Bochum |
| record_format | Article |
| series | Transactions on Cryptographic Hardware and Embedded Systems |
| spelling | doaj.art-c082783eb324437292b239d88846e0e82023-06-09T15:49:38ZengRuhr-Universität BochumTransactions on Cryptographic Hardware and Embedded Systems2569-29252023-06-012023310.46586/tches.v2023.i3.164-193Formally verifying KyberJosé Bacelar Almeida0Manuel Barbosa1Gilles Barthe2Benjamin Grégoire3Vincent Laporte4Jean-Christophe Léchenet5Tiago Oliveira6Hugo Pacheco7Miguel Quaresma8Peter Schwabe9Antoine Séré10Pierre-Yves Strub11Universidade do Minho, Braga, Portugal; University of Porto (FCUP), Porto, PortugalUniversity of Porto (FCUP), Porto, Portugal; INESC TEC, Porto, PortugalMax Planck Institute for Security and Privacy, Bochum, Germany; IMDEA Software Institute, Madrid, SpainUniversité Côte d’Azur, Inria, FranceUniversité de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, FranceUniversité Côte d’Azur, Inria, FranceMax Planck Institute for Security and Privacy, Bochum, GermanyUniversity of Porto (FCUP), Porto, Portugal; INESC TEC, Porto, PortugalMax Planck Institute for Security and Privacy, Bochum, GermanyMax Planck Institute for Security and Privacy, Bochum, Germany; Radboud University, Nijmegen, The NetherlandsÉcole Polytechnique, Paris, FranceMeta, Paris, France 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. https://tches.iacr.org/index.php/TCHES/article/view/10960High-assurance cryptographylattice-based KEMsNIST PQCJasminEasyCrypt |
| spellingShingle | 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 Formally verifying Kyber Transactions on Cryptographic Hardware and Embedded Systems High-assurance cryptography lattice-based KEMs NIST PQC Jasmin EasyCrypt |
| title | Formally verifying Kyber |
| title_full | Formally verifying Kyber |
| title_fullStr | Formally verifying Kyber |
| title_full_unstemmed | Formally verifying Kyber |
| title_short | Formally verifying Kyber |
| title_sort | formally verifying kyber |
| topic | High-assurance cryptography lattice-based KEMs NIST PQC Jasmin EasyCrypt |
| url | https://tches.iacr.org/index.php/TCHES/article/view/10960 |
| work_keys_str_mv | AT josebacelaralmeida formallyverifyingkyber AT manuelbarbosa formallyverifyingkyber AT gillesbarthe formallyverifyingkyber AT benjamingregoire formallyverifyingkyber AT vincentlaporte formallyverifyingkyber AT jeanchristophelechenet formallyverifyingkyber AT tiagooliveira formallyverifyingkyber AT hugopacheco formallyverifyingkyber AT miguelquaresma formallyverifyingkyber AT peterschwabe formallyverifyingkyber AT antoinesere formallyverifyingkyber AT pierreyvesstrub formallyverifyingkyber |