EasyPQC: Verifying Post-Quantum Cryptography
Part Of
Proceedings of the ACM Conference on Computer and Communications Security
Start Page
2564
End Page
2586
ISBN (of the container)
978-145038454-4
Date Issued
2021-11-12
Author(s)
Manuel Barbosa
Gilles Barthe
Xiong Fan
Benjamin Grégoire
Jonathan Katz
Pierre-Yves Strub
Xiaodi Wu
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 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.
Event(s)
27th ACM Annual Conference on Computer and Communication Security
SDGs
Publisher
ACM
Type
conference paper