Welcome to the resource topic for 2023/087
Title:
Verification of Correctness and Security Properties for CRYSTALS-KYBER
Authors: Katharina Kreuzer
Abstract: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 .