Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/89763
Título: | Formally verifying Kyber. Episode IV: implementation correctness |
Autor(es): | Almeida, José Bacelar Barbosa, Manuel Barthe, Gilles Grégoire, Benjamin Laporte, Vincent Léchenet, Jean-Christophe Oliveira, Tiago Pacheco, Hugo Quaresma, Miguel Schwabe, Peter Séré, Antoine Strub, Pierre-Yves |
Palavras-chave: | High-assurance cryptography lattice-based KEMs NIST PQC Jasmin EasyCrypt |
Data: | Set-2023 |
Editora: | Ruhr-Universität Bochum |
Revista: | IACR Transactions on Cryptographic Hardware and Embedded Systems |
Resumo(s): | 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. |
Tipo: | Artigo |
URI: | https://hdl.handle.net/1822/89763 |
DOI: | 10.46586/tches.v2023.i3.164-193 |
ISSN: | 2569-2925 |
Versão da editora: | https://tches.iacr.org/index.php/TCHES/article/view/10960 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | HASLab - Artigos em revistas internacionais |
Este trabalho está licenciado sob uma Licença Creative Commons