EasyPQC: Verifying Post-Quantum Cryptography

被引：12

作者：

Barbosa, Manuel ^{[1
,2
]}

Barthe, Gilles ^{[3
,4
]}

Fan, Xiong ^{[5
]}

Gregoire, Benjamin ^{[6
]}

Hung, Shih-Han ^{[7
]}

Katz, Jonathan ^{[8
]}

Strub, Pierre-Yves ^{[9
]}

Wu, Xiaodi ^{[8
]}

Zhou, Li ^{[3
]}

机构：

[1] Univ Porto FCUP, Porto, Portugal

[2] INESC TEC, Porto, Portugal

[3] MPI SP, Bochum, Germany

[4] IMDEA Software Inst, Bochum, Germany

[5] Algorand Inc, Boston, MA USA

[6] INRIA, Sophia Antipolis, France

[7] Univ Texas Austin, Austin, TX 78712 USA

[8] Univ Maryland, College Pk, MD 20742 USA

[9] Ecole Polytech, Paris, France

来源：

CCS '21: PROCEEDINGS OF THE 2021 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY | 2021年

关键词：

Formal verification; post-quantum cryptography; EXACT SECURITY;

D O I：

10.1145/3460120.3484567

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical attackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of post-quantum cryptography proofs, settling a question raised by (Unruh, POPL 2019). Leveraging our positive result, we implement EasyPQC, an extension of EasyCrypt for post-quantum security proofs, and use EasyPQC to verify post-quantum security of three classic constructions: PRF-based MAC, Full Domain Hash and GPV08 identity-based encryption.

引用

页码：2564 / 2586

页数：23

共 50 条

[1] Post-Quantum Cryptography
Monroe, Don
COMMUNICATIONS OF THE ACM, 2023, 66 (02) : 15 - 17
[2] Post-quantum cryptography
Bernstein, Daniel J.
Lange, Tanja
NATURE, 2017, 549 (7671) : 188 - 194
[3] Post-quantum cryptography
Daniel J. Bernstein
Tanja Lange
Nature, 2017, 549 : 188 - 194
[4] Post-Quantum Crystography: A Combination of Post-Quantum Cryptography and Steganography
Gabriel, A. J.
Alese, B. K.
Adetunmbi, A. O.
Adewale, O. S.
2013 8TH INTERNATIONAL CONFERENCE FOR INTERNET TECHNOLOGY AND SECURED TRANSACTIONS (ICITST), 2013, : 449 - +
[5] Applications of Post-Quantum Cryptography
Bagirovs, Emils
Provodin, Grigory
Sipola, Tuomo
Hautamaki, Jari
PROCEEDINGS OF THE 23RD EUROPEAN CONFERENCE ON CYBER WARFARE AND SECURITY, ECCWS 2024, 2024, 23 : 49 - 57
[6] Verifying Classic McEliece: Examining the Role of Formal Methods in Post-Quantum Cryptography Standardisation
Brain, Martin
Cid, Carlos
Player, Rachel
Robson, Wrenna
CODE-BASED CRYPTOGRAPHY, CBCRYPTO 2022, 2023, 13839 : 21 - 36
[7] A note on quantum security for post-quantum cryptography
Song, Fang
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, 8772 : 246 - 265
[8] A Note on Quantum Security for Post-Quantum Cryptography
Song, Fang
POST-QUANTUM CRYPTOGRAPHY, PQCRYPTO 2014, 2014, 8772 : 246 - 265
[9] Post-quantum cryptography and the quantum future of cybersecurity
Liu, Yi-Kai
Moody, Dustin
PHYSICAL REVIEW APPLIED, 2024, 21 (04):
[10] A Mathematical Perspective on Post-Quantum Cryptography
Richter, Maximilian
Bertram, Magdalena
Seidensticker, Jasper
Tschache, Alexander
MATHEMATICS, 2022, 10 (15)

← 1 2 3 4 5 →