qrhl-tool – Interactive theorem prover for qRHL

Qrhl-tool is an interactive theorem prover for qRHL (quantum relational Hoare logic), specifically for quantum and post-quantum security proofs.

See the literature and documentation listed below for in-depth explanations.

Screenshot of qrhl-tool

Installation

See here for installation instructions.

Documentation and help

The user manual, included in the binary installation as manual.pdf
Example files, included in the binary installation in examples/
The quickstart guide contributed by Tejas Shah
Gitter chat

Papers

Quantum Relational Hoare Logic, POPL 2019 – introduces the logic underlying the tool (recommended background!)
Local Variables and Quantum Relational Hoare Logic – describes extensions of qRHL to handle local variables, used in qrhl-tool
Post-Quantum Verification of Fujisaki-Okamoto, Asiacrypt 2020 – describes the formalization of a Fujisaki-Okamoto variant in qrhl-tool.

Under the hood

The qrhl-tool uses a number of open-source libraries and tools, the most notable dependencies are:

The Isabelle theorem prover: for all non-qRHL specific reasoning.
scala-isabelle: a library for controlling Isabelle within Scala.
Complex_Bounded_Operators: An Isabelle formalization of complex bounded operators, building the foundation for the modeling of quantum mechanics in qrhl-tool.
Many more library dependencies, see the build script.

Acknowledgments

Development was supported by the Air Force Office of Scientific Research (AOARD Grant FA2386-17-1-4022), by the ERC consolidator grant CerQuS (819317), and by the PRG946 grant from the Estonian Research Council.