Quantum Relational Hoare Logic

Abstract

We present a logic for reasoning about pairs of interactive quantum programs - quantum relational Hoare logic (qRHL). This logic follows the spirit of probabilistic relational Hoare logic (Barthe et al. 2009) and allows us to formulate how the outputs of two quantum programs relate given the relationship of their inputs. Probabilistic RHL was used extensively for computer-verified security proofs of classical cryptographic protocols. Since pRHL is not suitable for analyzing quantum cryptography, we present qRHL as a replacement, suitable for the security analysis of post-quantum cryptography and quantum protocols. The design of qRHL poses some challenges unique to the quantum setting, e.g., the definition of equality on quantum registers. Finally, we implemented a tool for verifying proofs in qRHL and developed several example security proofs in it.

arXiv commentExtended abstract appeared at POPL 2019

References in corpus (6)

• Quantum cryptography: Public key distribution and coin tossing
• Simple Proof of Security of the BB84 Quantum Key Distribution Protocol
• Random Oracles in a Quantum World
• Quantum Relational Hoare Logic
• Relational reasoning via probabilistic coupling
• Coupling proofs are probabilistic product programs

Cited by in corpus (12)

• Quantum Relational Hoare Logic
• Quantum Hoare logic with classical variables
• Formal Verification of Quantum Programs: Theory, Tools and Challenges
• Relational Proofs for Quantum Programs
• Efficient Formal Verification of Quantum Error Correcting Programs
• Algebraic Reasoning of Quantum Programs via Non-idempotent Kleene Algebra
• Symbolic Reasoning about Quantum Circuits in Coq
• Verification of Nondeterministic Quantum Programs
• On Algebraic Abstractions for Concurrent Separation Logics
• Automating Equational Proofs in Dirac Notation
• A Practical Quantum Hoare Logic with Classical Variables, I
• Hybrid Path-Sums for Hybrid Quantum Programs