High-assurance Post-Quantum Crypto with Franziskus Kiefer and Karthik Bhargavan

Security Cryptography Whatever

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)

Chapter

1. High-assurance Post-Quantum Crypto with Franziskus Kiefer and Karthik Bhargavan (00:00:00)

2. ML-KEM Implementation in Rust (00:00:12)

3. High-assurance Software Development (00:11:55)

4. Understanding Secret Independence and Crypto Proofs (00:19:07)

5. Vulnerabilities in ML-KEM Encryption Process (00:30:45)

6. Protocol Design (00:43:02)

7. Transitioning to Rust and Post-Quantum Cryptography (00:49:17)