Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Lecture notes in computer science

Formal Verification Techniques for Post-quantum Cryptography: A Systematic Review

Yuexi Xu, Zhenyuan Li, Naipeng Dong, Veronika Kuchta, Zhé Hóu, Dongxi Liu

Published Sep 28, 2024• 6 citations
Publisher
DOI
10.1007/978-3-031-66456-4_19

Related papers

Post-Quantum Cryptography: A Systematic Review of Algorithms, Standardization, Challenges, and Future Research Directions

Aritrik Ghosh

•Jan 1, 2026•0 citations

Post-Quantum Cryptography for Satellite and Space Security: A Protocol-Centred Systematic Literature Review

Abubakar Ahmad

This is a systematic literature review for space and satellite cyber security with focus on the protocols of post-quantum cryptography. The review aims to answer 5 research questions that covers primitives, protocols, evaluation evidence, threats/security models, and constraints/maturity.

•Oct 18, 2026•0 citations

Analysis of Post-Quantum Cryptographic Algorithms: A Systematic Literature Review

Francisco Javier de la Puente Secades, Gonzalo Esteban, Adrián Campazas +3 more

Lecture notes in networks and systems•Jan 1, 2024•2 citations

Formal methods for quantum cryptography

Ellie D’Hondt

•Jan 1, 2008•0 citations

EasyPQC: Verifying Post-Quantum Cryptography

Manuel Barbosa, Gilles Barthe, Xiong Fan +6 more

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.

ACM SIGSAC Conference on Computer and Communications Security (CCS)•Nov 12, 2021•30 citations

Post Quantum Cryptography Algorithms: A Review and Applications

Bikram Paul, Gaurav Trivedi

Lecture notes in networks and systems•Jan 1, 2023•7 citations
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.