Verifying classic McEliece: examining the role of formal methods in post-quantum cryptography standardisation

DOI10.1007/978-3-031-29689-5_2MaRDI QIDQ6132744zbMATHOpenAlexFDO

Authors Martin Brain, Carlos Cid, Rachel Player, Wrenna Robson

Publication date 17 August 2023

Published in Code-Based Cryptography (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-29689-5_2

zbMATH Keywords

code-based cryptography

Mathematics Subject Classification ID

Cryptography (94A60) Quantum cryptography (quantum-theoretic aspects) (81P94)

Recommendations

• Formal verification of Saber's public-key encryption scheme in easycrypt
• SoK: how (not) to design and implement post-quantum cryptography
• Practical Formal Methods for Real World Cryptography (Invited Talk)
• Error-correcting codes and post-quantum cryptography
• Moderate classical McEliece keys from quasi-centrosymmetric Goppa codes

Cites work

• CSIDH on the surface
• McBits revisited
• McBits: fast constant-time code-based cryptography
• The Lean 4 theorem prover and programming language
• Verified cryptographic code for everybody

Cited in

(1)

• Formal verification of Saber's public-key encryption scheme in easycrypt

This page was built for publication: Verifying classic McEliece: examining the role of formal methods in post-quantum cryptography standardisation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6132744)