Post-Quantum Provable Security and Formal Verification

Project funded by Fundação para a Ciência e a Tecnologia, I.P. (FCT), grant 2025.00728.BD. Runs 2025-10-01 to 2028-09-30. Source: OpenAIRE Graph, from the funder's project data (collected by OpenAIRE on 2026-06-24); national funding data, not CORDIS. Abstract given by the source: The possibility of the existence of large-scale quantum computers in the future threatens the security of public-key cryptosystems that underlie communication at a global level, which motivated the inception of post-quantum cryptography. This project aims to address some prominent open challenges in the field of post-quantum provable security, with a focus on computer-aided cryptography based on the EasyCrypt proof assistant. This includes solving technical issues regarding arguing about quantum interaction with cryptographic tools (such as permutations) and conceptual matters related to the definition of frameworks of security in the quantum setting (namely, the UC framework). Moreover, the underlying logic of EasyCrypt will be extended with the intent of capturing the established results and others from the literature. The effectiveness and practicality of the developed techniques and tools will be demonstrated by application to candidate protocols to the NIST post-quantum competition, namely presenting post-quantum security proofs and formally verifying them.

Original source.

Source: OpenAIRE Graph: projects of national funders, OpenAIRE, from the project data of Fundação para a Ciência e a Tecnologia, I.P. (FCT). Retrieved 2026-10-22. Licence: Creative Commons Attribution 4.0 (OpenAIRE Graph). Selected metadata, adapted presentation; the publisher's record is authoritative. No endorsement by the source is implied. Licence: Creative Commons Attribution 4.0 (CC BY 4.0).

AI-assisted summary: The project "Post-Quantum Provable Security and Formal Verification" is funded by FCT and runs from 2025-10-01 to 2028-09-30. It aims to address challenges in post-quantum cryptography, focusing on computer-aided cryptography using the EasyCrypt proof assistant. Suggested technology pillar: communication. Generated by AI from the public source text; it may contain errors and the original source is authoritative.