Welcome to the resource topic for 2023/027
Title:
Verification of the (1–δ)-Correctness Proof of CRYSTALS-KYBER with Number Theoretic Transform
Authors: Katharina Kreuzer
Abstract:This paper describes a formalization of the specification and the algorithm of the cryptographic scheme CRYSTALS-KYBER as well as the verification of its (1 − δ)-correctness proof. During the formalization, a problem in the correctness proof was uncovered. In order to amend this
issue, a necessary property on the modulus parameter of the CRYSTALS-KYBER algorithm was introduced. This property is already implicitly fulfilled by the structure of the modulus prime used in the number theoretic transform (NTT). The NTT and its convolution theorem
in the case of CRYSTALS-KYBER was formalized as well. The formalization was realized in the theorem prover Isabelle.
ePrint: https://eprint.iacr.org/2023/027
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .