Paper 2023/027 Original: eprint.iacr.org/2023/027 ↗
Verification of the (1–δ)-Correctness Proof of CRYSTALS-KYBER with Number Theoretic Transform
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.
Metadata
- Available format(s)
PDF- Category
- Public-key cryptography
- Publication info
- Preprint.
- History
- 2023-01-09: last updated
- 2023-01-09: published
- Short URL
- https://ia.cr/2023/027
- License
- https://creativecommons.org/licenses/by/4.0/
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},
url = {https://eprint.iacr.org/2023/027}
}