Formally verifying Kyber Part I: Implementation Correctness.
José Bacelar AlmeidaManuel BarbosaGilles BartheBenjamin GrégoireVincent LaporteJean-Christophe LéchenetTiago OliveiraHugo PachecoMiguel QuaresmaPeter SchwabeAntoine SéréPierre-Yves StrubPublished in: IACR Cryptol. ePrint Arch. (2023)