Formally verifying Kyber Episode IV: Implementation correctness.
José Bacelar AlmeidaManuel BarbosaGilles BartheBenjamin GrégoireVincent LaporteJean-Christophe LéchenetTiago OliveiraHugo PachecoMiguel QuaresmaPeter SchwabeAntoine SéréPierre-Yves StrubPublished in: IACR Trans. Cryptogr. Hardw. Embed. Syst. (2023)