|Title||EasyPQC: Verifying Post-Quantum Cryptography|
|Publication Type||Journal Article|
|Year of Publication||2021|
|Authors||Barbosa, M, Barthe, G, Fan, X, Grégoire, B, Hung, S-H, Katz, J, Strub, P-Y, Wu, X, Zhou, L|
|Journal||ACM CCS 2021|
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.