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)

Podden och tillhörande omslagsbild på den här sidan tillhör Deirdre Connolly, Thomas Ptacek, David Adrian. Innehållet i podden är skapat av Deirdre Connolly, Thomas Ptacek, David Adrian och inte av, eller tillsammans med, Poddtoppen.