Paper 2023/087

Verification of Correctness and Security Properties for CRYSTALS-KYBER

Katharina Kreuzer, Technical University of Munich

Since the post-quantum crypto system CRYSTALS-KYBER has been chosen for standardization by the National Institute for Standards and Technology (US), a formal verification of its correctness and security properties becomes even more relevant. Using the automated theorem prover Isabelle, we are able to formalize the algorithm specifications and parameter sets of Kyber's public key encryption scheme and verify the $\delta$-correctness and indistinguishability under chosen plaintext attack property. However, during the formalization process, several gaps in the pen-and-paper proofs were discovered. All but one gap concerning the error bound $\delta$ could be filled. Calculations in smaller dimensions give examples where the bound $\delta$ is less than the actual error term, violating the correctness property. Since the correctness proof could be formalized up to an application of the module-Learning-with-Errors assumption, we believe that the discrepancy of the original error bound and the formalized version is relatively small. Thus the correctness could be formalized up to a minimal change to the error bound.

Available format(s)
Public-key cryptography
Publication info
post-quantum cryptographyKybersecurityverificationIsabelle
Contact author(s)
k kreuzer @ tum de
2024-02-05: last of 2 revisions
2023-01-24: received
See all versions
Short URL
Creative Commons Attribution


      author = {Katharina Kreuzer},
      title = {Verification of Correctness and Security Properties for {CRYSTALS}-{KYBER}},
      howpublished = {Cryptology ePrint Archive, Paper 2023/087},
      year = {2023},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.