Machine-checking post-quantum cryptography
summary
Post-quantum proofs are machine-checked using a toolchain that extracts a formal model from implementation code and proves security in EasyCrypt while compiling verified code from Jasmine, with a goal of a verified PQC library in Formosa Crypto. 64 NIST candidates and ~40 signature proposals motivate this; past errors appear in XMSS and Sphinx and several Kyber/Dilithium proofs needed fixes. A full-stack, machine-checked Kyber proof plus verified implementation exists after three+ years and ~30–40 core contributors, but tooling still requires expert work.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 1:08Machine-checking cryptographic proofs
- 4:00Traditional cryptanalysis limits
- 6:13Verifying paper proofs challenges
- 8:44Flawed proofs in post-quantum schemes
- 13:46FOSAD crypto project
- 15:57Formal verification for security proofs
- 18:49Rare fully verified submissions
- 21:15Current state and future work
- 22:19Q&A: Auditing auditors and tool flaws
- 24:48Q&A: Proof assistants interaction
- 26:21Q&A: Modeling leakage in verification
- 27:26Q&A: Compilation limits
- 28:30Q&A: Dilithium verification progress
related talks
50mPost‑Quantum Cryptography for dummies. Challenges and opportunities
32mCybersecurity in Post Quantum Era
45mPost‑Quantum Cryptography: The Fundamentals of Tomorrow's Digital World
26mThe ABCs (Accelerated, Better and Cheaper) to Cryptographic Resilience
53mPanel: Migrating to Post-Quantum Schemes
14mWhy post-quantum cryptography?
58mPQC Integration in HSMs: From Standards to Strategy
44mQuantum Cyber Risk: How Deep and How Wide?