Ensuring Correctness and Security in High-Speed Post-Quantum Cryptography: Leveraging Formal Verification Tools (G12b)
This talk highlights the urgent need for secure and efficient post-quantum cryptographic systems, given quantum computing’s potential to compromise traditional encryption. It explores how formal verification tools can ensure the correctness, security, and reliability of these systems through rigorous analysis of cryptographic algorithms. The talk introduces key concepts of formal verification, emphasizing its advantages over traditional testing methods, and examines a specific case study: the formal verification of a high-speed implementation of the NIST-standardized ML-KEM scheme. By demonstrating techniques such as theorem proving and automated reasoning, the talk underscores the importance of formal verification in developing robust post-quantum cryptographic systems.