Provably Secure Protocols and High-Assurance Software for the Post-Quantum Transition
Karthik Bhargavan (Cryspen, Chief Research Scientist)
Since the standardization of TLS 1.3, formal verification has become an important requirement for any new cryptographic mechanism or protocol. This is even more the case for the PQC migration, which requires a comprehensive update of the algorithms, constructions, and protocols used in all connected systems. At the IETF, at Apple and at Signal, formal protocol analysis tools are being used to show that new post-quantum protocols are secure against both classical and quantum adversaries, and that they are not vulnerable to new vulnerabilities, such as downgrade attacks. Mainstream software vendors like Google, Microsoft, and Mozilla are developing and deploying formally verified post-quantum cryptography implementations. In this talk, I will survey recent and ongoing work on the use of formal verification in the PQC migration of several projects, highlighting both successes and challenges. I will argue that the PQC migration presents us a unique opportunity to upgrade all the cryptographic mechanisms we rely on to use provably secure designs and high-assurance implementations.