



@article {2881,
	title = {EasyPQC: Verifying Post-Quantum Cryptography},
	journal = {ACM CCS 2021},
	year = {2021},
	month = {9/20/2021},
	abstract = {<p>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.</p>},
	doi = {https://dx.doi.org/10.1145/3460120.3484567},
	author = {Manuel Barbosa and Gilles Barthe and Xiong Fan and Benjamin Gr{\'e}goire and Shih-Han Hung and Jonathan Katz and Pierre-Yves Strub and Xiaodi Wu and Li Zhou}
}
