@inproceedings{62551ab71d864953864b39373792446d,
title = "EasyPQC: Verifying Post-Quantum Cryptography",
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 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.",
keywords = "formal verification, post-quantum cryptography",
author = "Manuel Barbosa and Gilles Barthe and Xiong Fan and Benjamin Gr{\'e}goire and Hung, \{Shih Han\} and Jonathan Katz and Strub, \{Pierre Yves\} and Xiaodi Wu and Li Zhou",
note = "Publisher Copyright: {\textcopyright} 2021 ACM.; 27th ACM Annual Conference on Computer and Communication Security, CCS 2021 ; Conference date: 15-11-2021 Through 19-11-2021",
year = "2021",
month = nov,
day = "13",
doi = "10.1145/3460120.3484567",
language = "English",
series = "Proceedings of the ACM Conference on Computer and Communications Security",
publisher = "Association for Computing Machinery",
pages = "2564--2586",
booktitle = "CCS 2021 - Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security",
}