Katharina Kreuzer 📧

September 8, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session CRYSTALS-Kyber