Verifying Classic McEliece: Examining the Role of Formal Methods in Post-Quantum Cryptography Standardisation

Verifying Classic McEliece: Examining the Role of Formal Methods in Post-Quantum Cryptography Standardisation

연구 분야: Cryptography

학회: Code-Based Cryptography Workshop

Developers of computer-aided cryptographic tools are optimistic that formal methods will become a vital part of developing new cryptographic systems. We study the use of such tools to specify and verify the implementation of Classic McEliece, one of the code-based cryptography candidates in the fourth round of the NIST Post-Quantum standardisation Process. From our case study we draw conclusions about the practical applicability of these methods to the development of novel cryptography.