[Resource Topic] 2023/087: Verification of Correctness and Security Properties for CRYSTALS-KYBER

Welcome to the resource topic for 2023/087

Verification of Correctness and Security Properties for CRYSTALS-KYBER

Authors: Katharina Kreuzer


This paper describes a formalization of the specification and the algorithm of the public key encryption scheme CRYSTALS-KYBER as well as the verification of its \delta-correctness and indistinguishability under chosen plaintext attack (IND-CPA) security proof. The algorithms and proofs were formalized with only minimal assumptions in a modular way to verify the proofs for all possible parameter sets. During the formalization in this flexible setting, problems in the correctness proof were uncovered. Furthermore, the security of CRYSTALS-KYBER under IND-CPA was verified using a game-based approach. As the security property does not hold for the original version of CRYSTALS-KYBER, we only show the IND-CPA security for the latest versions. The security proof was verified under the hardness assumption of the module Learning-with-Errors Problem. The formalization was realized in the theorem prover Isabelle and is foundational.

ePrint: https://eprint.iacr.org/2023/087

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 .