Formally Verified (Post-Quantum) Cryptography, by Gilles Barthe (MPI-SP)

The NIST Post-Quantum Standardization program (2016-ongoing) aims to standardize a new generation of cryptographic algorithms resistant against quantum attackers.The talk will report and reflect on our long-term efforts to develop formally verified implementations of ML-KEM and ML-DSA, that were selected for standardization by NIST in 2022 and finally standardized in 2024.

Bio: Gilles Barthe is a scientific director at Max Planck Institute for Security and Privacy, Bochum, Germany and a part-time research professor at IMDEA Software Institute, Madrid, Spain. His research interests include programming languages and program verification, security and privacy, and cryptography.