Formally verifying Kyber Episode IV: Implementation correctness

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira 0004, Hugo Pacheco 0001, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub. Formally verifying Kyber Episode IV: Implementation correctness. IACR Trans. Cryptogr. Hardw. Embed. Syst., 2023(3):164-193, 2023. [doi]

Abstract

Abstract is missing.