2026-08-25T14:43:39Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26976 2026-07-16T09:49:33Z ddc:004 open_access

Developing a Quantum Crypto Theorem Prover from Scratch (Invited Talk) Unruh, Dominique Formalized mathematics functional analysis bounded operators We describe our experience developing qrhl-tool, a theorem prover for verifying quantum cryptographic protocols, both in the post-quantum and the full quantum setting. The tool is built around quantum relational Hoare logic (qRHL), a relational program logic for reasoning about pairs of quantum programs in the style of game-based cryptographic proofs. We discuss the design choices underlying the tool: in particular, a hybrid architecture that delegates ambient-logic reasoning to Isabelle/HOL while qrhl-tool itself handles qRHL judgments and the program language; an advanced memoization mechanism (hashed computations) that enables efficient incremental proof checking; and a deliberate path towards a foundational implementation. We walk through a small worked example (the hardness of inverting f∘f given a one-way permutation f) to illustrate how these pieces fit together in practice. Along the way we highlight what we got right, what we got wrong, and which limitations (procedure parameters, local variables, runtime reasoning) we would approach differently if starting over today. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dominique Unruh 2026 Is Part Of LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2026.2 urn:nbn:de:0030-drops-269763 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.2 eng https://creativecommons.org/licenses/by/4.0/legalcode