EasyPQC: Verifying Post-Quantum Cryptography

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

Paper 2021/1253

EasyPQC: Verifying Post-Quantum Cryptography

Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, 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.

Metadata

Available format(s): PDF
Category: Public-key cryptography
Publication info: Published elsewhere. Major revision. ACM CCS 2021
DOI: 10.1145/3460120.3484567
Keywords: Formal verification post-quantum cryptography
Contact author(s): leofanxiong @ gmail com
History: 2021-09-21: received
Short URL: https://ia.cr/2021/1253
License: CC BY

BibTeX

@misc{cryptoeprint:2021/1253,
      author = {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},
      title = {EasyPQC: Verifying Post-Quantum Cryptography},
      howpublished = {Cryptology ePrint Archive, Paper 2021/1253},
      year = {2021},
      doi = {10.1145/3460120.3484567},
      note = {\url{https://eprint.iacr.org/2021/1253}},
      url = {https://eprint.iacr.org/2021/1253}
}