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

Martin Brain; Carlos Cid; Rachel Player; Wrenna Robson

Paper 2023/010

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

Martin Brain

, City, University of London

Carlos Cid

, Simula UiB, Okinawa Institute of Science and Technology Graduate University

Rachel Player

, Royal Holloway University of London

Wrenna Robson

, Royal Holloway University of London

Abstract

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.

Note: Acknowledgement of EPRSC and UK Government funding added.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Published elsewhere. Minor revision. CBCrypto 2022
Keywords: computer-aided cryptography post-quantum cryptography formal methods verification
Contact author(s): martin brain @ city ac uk
carlos cid @ oist jp
rachel player @ rhul ac uk
wrenna robson 2019 @ live rhul ac uk
History: 2023-11-16: revised; 2023-01-03: received; See all versions
Short URL: https://ia.cr/2023/010
License: CC BY

BibTeX

@misc{cryptoeprint:2023/010,
      author = {Martin Brain and Carlos Cid and Rachel Player and Wrenna Robson},
      title = {Verifying Classic {McEliece}: examining the role of formal methods in post-quantum cryptography standardisation},
      howpublished = {Cryptology {ePrint} Archive, Paper 2023/010},
      year = {2023},
      url = {https://eprint.iacr.org/2023/010}
}