International Association
for Cryptologic Research

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.