CryptoDB
Using Formally Verified Post-Quantum Algorithms at Scale
| Authors: | |
|---|---|
| Download: | |
| Presentation: | Slides |
| Abstract: | In an attempt to provide organizations with access to correct and bug-free implementations of the new NIST-selected PQC algorithms, Cryspen and Google have joined forces to produce formally verified, open source implementations of these algorithms. In this talk we will cover our cutting-edge approach to formally verifying ML-KEM, the challenges encountered during the verification process, and the timing side channel attack uncovered by the process. We will also discuss the way forward for formal verification of PQC algorithms, the impact of formal verification on the development workflow, and the subsequent deployment of secure and optimized PQC implementations. |
| Video: | https://youtu.be/DBXb2uJDB5w |
BibTeX
@misc{rwc-2025-35870,
title={Using Formally Verified Post-Quantum Algorithms at Scale},
note={Video at \url{https://youtu.be/DBXb2uJDB5w}},
howpublished={Talk given at RWC 2025},
author={Thyla van der Merwe and Karthikeyan Bhargavan and Lucas Franceschino and Franziskus Kiefer and Andres Erbsen},
year=2025
}