Email Gateway (Jan 16 2024 at 14:41): Email Gateway (Jan 16 2024 at 14:41):From: Tobias Nipkow <nipkow@in.tum.de>
CRYSTALS-Kyber_Security
Katharina Kreuzer
This article builds upon the formalization of the deterministic part of the
original Kyber algorithms (see the CRYSTALS-Kyber entry). The correctness proof
is expanded to cover both the deterministic part from the previous formalization
and the probabilistic part of randomly chosen inputs. Indeed, the probabilistic
version of the delta-correctness in the original paper was flawed and could only
be formalized for a modified delta'. The authors of Kyber also remarked, that
the security proof against indistinguishability under chosen plaintext attack
(IND-CPA) does not hold for the original version of Kyber. Thus, the newer
version (round 2 and 3 of NIST standarisation process) was formalized as well,
including the adapted deterministic and probabilistic correctness theorems.
Moreover, the IND-CPA security proof against the new version of Kyber has been
verified using the CryptHOL library. Since the new version also included a
change of parameters, the Kyber algorithms have been instantiated with the new
parameter set as well.
https://www.isa-afp.org/entries/CRYSTALS-Kyber_Security.html
Enjoy!
Last updated: Apr 28 2024 at 20:16 UTC