About this episode
We welcome Franziskus and Karthik from Cryspen to discuss their new high-assurance implementation of ML-KEM (the final form of Kyber), discussing how formal methods can both help provide correctness guarantees, security assurances, and performance wins for your crypto code!Transcript: https://securitycryptographywhatever.com/2024/01/29/high-assurance-kyber/Links:- https://cryspen.com/post/ml-kem-implementation/- https://github.com/cryspen/libcrux/- https://github.com/formosa-crypto/libjade- https://cryspen.com/post/pqxdh/- https://eprint.iacr.org/2023/1933.pdf- Franziskus Kiefer: https://franziskuskiefer.de/- Karthik Bhargavan: https://bhargavan.info/"Security Cryptography Whatever" is hosted by Deirdre Connolly (@durumcrustulum), Thomas Ptacek (@tqbf), and David Adrian (@davidcadrian)
