Email Gateway (Sep 08 2022 at 15:58): Email Gateway (Sep 08 2022 at 15:58):From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to report a new entry, CRYSTALS-Kyber, by Katharina Kreuzer:
This article formalizes the specification and the algorithm of the cryptographic scheme CRYSTALS-KYBER with multiplication using the Number Theoretic Transform and verifies its (1-δ)-correctness proof. CRYSTALS-KYBER is a key encapsulation mechanism in lattice-based post-quantum cryptography. This entry formalizes the key generation, encryption and decryption algorithms and shows that the algorithm decodes correctly under a highly probable assumption ((1-δ)-correctness). Moreover, the Number Theoretic Transform (NTT) in the case of Kyber and the convolution theorem thereon is formalized.
Looks impressive in its own right. It’s also yet another application of the big Berlekamp and Zassenhaus development.
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC