Verification of the (1–δ)-Correctness Proof of CRYSTALS-KYBER with Number Theoretic Transform

Katharina Kreuzer

Paper 2023/027

Verification of the (1–δ)-Correctness Proof of CRYSTALS-KYBER with Number Theoretic Transform

Katharina Kreuzer

, Technical University of Munich

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.
Keywords: PQC Kyber verification
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},
      url = {https://eprint.iacr.org/2023/027}
}