TY - JOUR T1 - EasyPQC: Verifying Post-Quantum Cryptography JF - ACM CCS 2021 Y1 - 2021 A1 - Manuel Barbosa A1 - Gilles Barthe A1 - Xiong Fan A1 - Benjamin Grégoire A1 - Shih-Han Hung A1 - Jonathan Katz A1 - Pierre-Yves Strub A1 - Xiaodi Wu A1 - Li Zhou AB -

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.

U5 - https://dx.doi.org/10.1145/3460120.3484567 ER -