h1

h2

h3

h4

h5
h6

CerQuS

Certified Quantum Security

CoordinatorUniversity of Tartu
Grant period2019-06-01 - 2024-05-31
Funding bodyEuropean Union
Call numberERC-2018-COG
Grant number819317
IdentifierG:(EU-Grant)819317

Note: Digital communication permeates all areas of today's daily life. Cryptographic protocols are used to secure that communication. Quantum communication and the advent of quantum computers both threaten existing cryptographic solutions, and create new opportunities for secure protocols. The security of cryptographic systems is normally ensured by mathematical proofs. Due to human error, however, these proofs often contain errors, limiting the usefulness of said proofs. This is especially true in the case of quantum protocols since human intuition is well-adapted to the classical world, but not to quantum mechanics. To resolve this problem, methods for verifying cryptographic security proofs using computers (i.e., for "certifying" the security) have been developed. Yet, all existing verification approaches handle classical cryptography only - for quantum protocols, no approaches exist. This project will lay the foundations for the verification of quantum cryptography. We will design logics and software tools for developing and verifying security proofs on the computer, both for classical protocols secure against quantum computer (post-quantum security) and for protocols that use quantum communication. Our main approach is the design of a logic (quantum relational Hoare logic, qRHL) for reasoning about the relationship between pairs of quantum programs, together with an ecosystem of manual and automated reasoning tools, culminating in fully certified security proofs for real-world quantum protocols. As a final result, the project will improve the security of protocols in the quantum age, by removing one possible source of human error. In addition, the project directly impacts the research community, by providing new foundations in program verification, and by providing cryptographers with new tools for the verification of their protocols.
     

Recent Publications

All known publications ...
Download: BibTeX | EndNote XML,  Text | RIS | 

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Journal Article  ;  ;
Reasoning about Parameterized Recursive Quantum Programs with Ancilla Data and Probabilistic Control
ACM transactions on computational logic 27(4), 1-63 () [10.1145/3815573]  GO BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;
Complex Bounded Operators in Isabelle/HOL
17th International Conference on Interactive Theorem Proving : ITP 2026, July 26–29, 2026, Lisbon, Portugal / Edited by Ekaterina Komendantskaya ; Tobias Nipkow
17. International Conference on Interactive Theorem Proving, ITP 2026, LisbonLisbon, Portugal, 26 Jul 2026 - 29 Jul 20262026-07-262026-07-29 Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics (LIPIcs) 382, 3:1-3:19 ()  GO BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Journal Article
Compressed Oracles
Archive of formal proofs 2025, 176 pages ()  GO  Download fulltext Files  Download fulltextFulltext BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Journal Article
Kraus Maps
Archive of formal proofs 2025, 1-62 ()  GO  Download fulltext Files  Download fulltextFulltext BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Journal Article  ;
The Oneway to Hiding Theorem
Archive of formal proofs 2025, 145 pages ()  GO  Download fulltext Files  Download fulltextFulltext BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;
Formalizing the One-Way to Hiding Theorem
Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs
14. ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025, Denver, CO USADenver, CO USA, USA, [Erscheinungsort nicht ermittelbar] : Association for Computing Machinery, ACM Conferences () [10.1145/3703595.3705887]  GO BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;  ;  ;
Leakage-Free Probabilistic Jasmin Programs
CPP ’25 : proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs / edited by: Kathrin Stark, Amin Timany, Sandrine Blazy, and Nicolas Tabareau
14. ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025, Denver, CODenver, CO, USA, 20 Jan 2025 - 21 Jan 20252025-01-202025-01-21 New York, NY, USA : Association for Computing Machinery, Inc. 3-16 () [10.1145/3703595.3705871]  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;  ;
Bayesian Inference in Quantum Programs
52nd International Colloquium on Automata, Languages, and Programming : ICALP 2025, July 8–11, 2025, Aarhus, Denmark / edited by Keren Censor-Hillel, Fabrizio Grandoni, Joël Ouaknine, Gabriele Puppis
52. International Colloquium on Automata, Languages, and Programming, ICALP 2025, AarhusAarhus, Denmark, 8 Jul 2025 - 11 Jul 20252025-07-082025-07-11 Wadern : Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, LIPIcs - Leibniz international proceedings in informatics 334, 157:1-157:18 () [10.4230/LIPIcs.ICALP.2025.157]  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Journal Article
Without Loss of Generality
Archive of formal proofs August 30, 2024 ()  GO   Download fulltextFulltext BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Journal Article
The Tensor Product on Hilbert Spaces
Archive of formal proofs September 10, 2024 ()  GO   Download fulltextFulltext BibTeX | EndNote: XML, Text | RIS

All known publications ...
Download: BibTeX | EndNote XML,  Text | RIS | 

 Record created 2020-01-11, last modified 2023-02-11
Similar records



Rate this document:

Rate this document:
1
2
3
4
5
 
(Not yet reviewed)