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

Interface-First Formal Verification for Hybrid Cryptography: Verified Scaffolding for QKD + Post-Quantum KEM Composition in Lean 4

Apoth3osis R&d, Richard Goodman

Published Jan 1, 2026• 0 citations
Publisher
DOI
10.13140/rg.2.2.20255.83362

Related papers

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

Yuexi Xu, Zhenyuan Li, Naipeng Dong +3 more

Lecture notes in computer science•Sep 28, 2024•6 citations

Formal Specification and Analysis of Post-quantum OpenPGP Protocol in CafeOBJ

Trong Binh Hoang, Duong Dinh Tran, Canh Minh Do +1 more

The Post-quantum OpenPGP (PQ OpenPGP) protocol extends OpenPGP with hybrid cryptography, combining classical and post-quantum algorithms.It aims to ensure longterm security against attacks by quantum-capable adversaries.This paper presents a formal specification and verification of the PQ OpenPGP protocol using the algebraic specification language CafeOBJ.Our specification captures key aspects of the protocol, including hybrid key encapsulation using post-quantum ML-KEM and classical ECDH-KEM, dual digital signatures from post-quantum ML-DSA and classical EdDSA, and a quantumcapable Dolev-Yao attacker model.We then focus on verifying the secrecy of the session key property under this attacker model.To facilitate the verification process, we employ the IPSG tool, which automatically generates formal proofs for desired properties based on a formal specification and auxiliary lemmas.

Proceedings/Proceedings of the ... International Conference on Software Engineering and Knowledge Engineering•Sep 29, 2025•0 citations

Quantum Safety: How Do We Know? Formal Verification of Cryptographic Protocols

Ilias Cherkaoui

•Oct 27, 2026•0 citations

ScaffML: A Quantum Behavioral Interface Specification Language for Scaffold

Tiancheng Jin, Jianjun Zhao

Ensuring the correctness of quantum programs is crucial for quantum software quality assurance. Although various effective verification methods exist for classical programs, they cannot be applied to quantum programs due to the fundamental differences in their execution logic, such as quantum superposition and entanglement. This calls for new methods to verify the correctness of quantum programs. In this paper, we present a behavioral interface specification language (BISL) called ScaffML for the quantum programming language Scaffold. ScaffML allows the specification of pre- and post-conditions for Scaffold modules and enables the mixing of assertions with Scaffold code, thereby facilitating debugging and verification of quantum programs. This paper discusses the goals and overall approach of ScaffML and describes the basic features of the language through examples. ScaffML provides an easy-to-use specification language for quantum programmers, supporting static analysis, run-time checking, and formal verification of Scaffold programs. Finally, we present several instances to illustrate the workflow and functionalities of ScaffML.

arXiv:2306.06468•IEEE International Conference on Quantum Software (QSW)•Jul 1, 2023•6 citations

Combining Post-Quantum Cryptography and Quantum Key Distribution: Taxonomy, Constructions, Proofs, Standards, Deployments and Open Problems

Mona Alotaibi, Noora Fetais, Saif M. Al-Kuwari

Post-quantum cryptography (PQC) and quantum key distribution (QKD) address the quantum threat from opposite directions: PQC replaces vulnerable public-key algorithms with schemes believed to resist quantum cryptanalysis, while QKD derives keys whose secrecy rests on physical assumptions rather than computational ones. Because each approach has a distinct failure mode, a growing body of work combines them so that a session key remains secure if either component holds. We first establish the deployed baseline, hybrid classical-plus-PQC key exchange, against which QKD-augmented designs must be judged. We then propose a taxonomy of hybrid PQC-QKD designs along eight dimensions (integration layer, combiner construction, authentication scope and source, QKD topology, trusted entities, key-delivery interface, classical component, and evidence type), and use it to compare published protocols, including Muckle and its successors, MACsec and TLS integrations, and IKEv2 mechanisms standardised in RFCs 8784, 9370, and 9867. We examine key-combiner constructions in light of the KEM-combiner literature and of NIST, ETSI, and ITU-T guidance, and map the security arguments for hybrid PQC-QKD protocols onto a common grid of security model, assumptions, permitted compromise, established guarantee, and limitations. We synthesise deployment evidence from metropolitan and national QKD networks, distinguishing the few testbeds that have run PQC in the key path from pure-QKD deployments, and summarise the standards and policy landscape, including the positions of national security agencies that recommend against relying on QKD alone. We close with open problems: authentication of the QKD classical channel, shared-infrastructure threat models, device certification versus formal proofs, formal verification of hybrid handshakes, and the lack of peer-reviewed deployment economics.

arXiv:2610.19039•Oct 13, 2026•0 citations

Post-quantum Cryptography in Practice: A Survey of Algorithms, Applications, and Deployment Challenges

Sharlene Anna Pereira, Melsa Magdalene Fernandes, E. A. Mary Anita +1 more

Lecture notes in networks and systems•Nov 17, 2025•0 citations
The Post-quantum OpenPGP (PQ OpenPGP) protocol extends OpenPGP with hybrid cryptography, combining classical and post-quantum algorithms.It aims to ensure longterm security against attacks by quantum-capable adversaries.This paper presents a formal specification and verification of the PQ OpenPGP protocol using the algebraic specification language CafeOBJ.Our specification captures key aspects of the protocol, including hybrid key encapsulation using post-quantum ML-KEM and classical ECDH-KEM, dual digital signatures from post-quantum ML-DSA and classical EdDSA, and a quantumcapable Dolev-Yao attacker model.We then focus on verifying the secrecy of the session key property under this attacker model.To facilitate the verification process, we employ the IPSG tool, which automatically generates formal proofs for desired properties based on a formal specification and auxiliary lemmas.
Ensuring the correctness of quantum programs is crucial for quantum software quality assurance. Although various effective verification methods exist for classical programs, they cannot be applied to quantum programs due to the fundamental differences in their execution logic, such as quantum superposition and entanglement. This calls for new methods to verify the correctness of quantum programs. In this paper, we present a behavioral interface specification language (BISL) called ScaffML for the quantum programming language Scaffold. ScaffML allows the specification of pre- and post-conditions for Scaffold modules and enables the mixing of assertions with Scaffold code, thereby facilitating debugging and verification of quantum programs. This paper discusses the goals and overall approach of ScaffML and describes the basic features of the language through examples. ScaffML provides an easy-to-use specification language for quantum programmers, supporting static analysis, run-time checking, and formal verification of Scaffold programs. Finally, we present several instances to illustrate the workflow and functionalities of ScaffML.
Post-quantum cryptography (PQC) and quantum key distribution (QKD) address the quantum threat from opposite directions: PQC replaces vulnerable public-key algorithms with schemes believed to resist quantum cryptanalysis, while QKD derives keys whose secrecy rests on physical assumptions rather than computational ones. Because each approach has a distinct failure mode, a growing body of work combines them so that a session key remains secure if either component holds. We first establish the deployed baseline, hybrid classical-plus-PQC key exchange, against which QKD-augmented designs must be judged. We then propose a taxonomy of hybrid PQC-QKD designs along eight dimensions (integration layer, combiner construction, authentication scope and source, QKD topology, trusted entities, key-delivery interface, classical component, and evidence type), and use it to compare published protocols, including Muckle and its successors, MACsec and TLS integrations, and IKEv2 mechanisms standardised in RFCs 8784, 9370, and 9867. We examine key-combiner constructions in light of the KEM-combiner literature and of NIST, ETSI, and ITU-T guidance, and map the security arguments for hybrid PQC-QKD protocols onto a common grid of security model, assumptions, permitted compromise, established guarantee, and limitations. We synthesise deployment evidence from metropolitan and national QKD networks, distinguishing the few testbeds that have run PQC in the key path from pure-QKD deployments, and summarise the standards and policy landscape, including the positions of national security agencies that recommend against relying on QKD alone. We close with open problems: authentication of the QKD classical channel, shared-infrastructure threat models, device certification versus formal proofs, formal verification of hybrid handshakes, and the lack of peer-reviewed deployment economics.