Machine-Checking Post-Quantum Cryptography

Explore the challenges and ongoing projects in machine-checking security proofs and implementations of post-quantum cryptography (PQC) in this 31-minute talk by Andreas Hülsing, Associate Professor at Eindhoven University of Technology. Delve into the new aspects introduced by PQC, including novel mathematical structures, security proof techniques, and implementation requirements. Examine the increased complexity of mathematical proofs and the need to protect against additional attack vectors. Learn about the use of computer-assisted verification to enhance reliability and security guarantees in PQC development. Discover current initiatives within the Formosa Crypto consortium, focusing on machine-checking security proofs and implementations using tools like EasyCrypt and Jasmine.