Paper 2023/027
Verification of the (1–δ)-Correctness Proof of CRYSTALS-KYBER with Number Theoretic Transform
, Technical University of MunichAbstract
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.
Metadata
- Available format(s)
-
PDF
- Category
- Public-key cryptography
- Publication info
- Preprint.
- Keywords
- PQCKyberverification
- Contact author(s)
- k kreuzer @ tum de
- History
- 2023-01-09: approved
- 2023-01-09: received
- See all versions
- Short URL
- https://ia.cr/2023/027
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2023/027,
author = {Katharina Kreuzer},
title = {Verification of the (1–δ)-Correctness Proof of CRYSTALS-KYBER with Number Theoretic Transform},
howpublished = {Cryptology ePrint Archive, Paper 2023/027},
year = {2023},
note = {\url{https://eprint.iacr.org/2023/027}},
url = {https://eprint.iacr.org/2023/027}
}
