Cryptology ePrint Archive: Report 2021/1253

EasyPQC: Verifying Post-Quantum Cryptography

Manuel Barbosa and Gilles Barthe and Xiong Fan and Benjamin Grégoire and Shih-Han Hung and Jonathan Katz and Pierre-Yves Strub and Xiaodi Wu and Li Zhou

Abstract: 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.

Category / Keywords: public-key cryptography / Formal verification, post-quantum cryptography

Original Publication (with major differences): ACM CCS 2021
DOI:
10.1145/3460120.3484567

Date: received 20 Sep 2021

Contact author: leofanxiong at gmail com

Available format(s): PDF | BibTeX Citation

Version: 20210921:115228 (All versions of this report)

Short URL: ia.cr/2021/1253


[ Cryptology ePrint archive ]