Name
Abstract | ||
|---|---|---|
ABSTRACTEasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical at- tackers, 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. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1145/3460120.3484567 | Computer and Communications Security |
Keywords | DocType | Citations |
Formal verification, post-quantum cryptography | Conference | 1 |
PageRank | References | Authors |
0.35 | 0 | 9 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Manuel Barbosa | 1 | 1 | 0.35 |
| Gilles Barthe | 2 | 2337 | 152.36 |
| Xiong Fan | 3 | 1 | 0.35 |
| Benjamin Grégoire | 4 | 817 | 48.93 |
| Shih-Han Hung | 5 | 1 | 0.35 |
| Jonathan Katz | 6 | 7579 | 347.97 |
| Pierre-Yves Strub | 7 | 1 | 0.35 |
| Xiaodi Wu | 8 | 49 | 9.39 |
| li zhou | 9 | 58 | 10.92 |