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

Martin Brain; Carlos Cid; Rachel Player; Wrenna Robson

doi:10.1007/978-3-031-29689-5_2

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

Martin Brain, Carlos Cid, Rachel Player, Wrenna Robson^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

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.

Original language	English
Title of host publication	Code-Based Cryptography
Publisher	Springer
ISBN (Electronic)	9783031296895
ISBN (Print)	9783031296888
DOIs	https://doi.org/10.1007/978-3-031-29689-5_2
Publication status	Published - 29 Mar 2023

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-031-29689-5_2Licence: Unspecified

https://eprint.iacr.org/2023/010Licence: CC BY

Handle.net

Persistent link

Cite this

Brain, M., Cid, C., Player, R., & Robson, W. (2023). Verifying Classic McEliece: Examining the Role of Formal Methods in Post-Quantum Cryptography Standardisation. In Code-Based Cryptography (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Springer. https://doi.org/10.1007/978-3-031-29689-5_2

@inproceedings{6dfec551c9e1429cb817a6c9d48aa912,

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

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.",

author = "Martin Brain and Carlos Cid and Rachel Player and Wrenna Robson",

year = "2023",

month = mar,

day = "29",

doi = "10.1007/978-3-031-29689-5_2",

language = "English",

isbn = "9783031296888",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

booktitle = "Code-Based Cryptography",

}

Brain, M, Cid, C, Player, R & Robson, W 2023, Verifying Classic McEliece: Examining the Role of Formal Methods in Post-Quantum Cryptography Standardisation. in Code-Based Cryptography. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer. https://doi.org/10.1007/978-3-031-29689-5_2

Verifying Classic McEliece: Examining the Role of Formal Methods in Post-Quantum Cryptography Standardisation. / Brain, Martin; Cid, Carlos; Player, Rachel et al.
Code-Based Cryptography. Springer, 2023. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

TY - GEN

T1 - Verifying Classic McEliece

T2 - Examining the Role of Formal Methods in Post-Quantum Cryptography Standardisation

AU - Brain, Martin

AU - Cid, Carlos

AU - Player, Rachel

AU - Robson, Wrenna

PY - 2023/3/29

Y1 - 2023/3/29

N2 - 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.

AB - 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.

UR - http://dx.doi.org/10.1007/978-3-031-29689-5_2

U2 - 10.1007/978-3-031-29689-5_2

DO - 10.1007/978-3-031-29689-5_2

M3 - Conference Contribution (Conference Proceeding)

SN - 9783031296888

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

BT - Code-Based Cryptography

PB - Springer

ER -