Quantum Relational Hoare Logic

TL;DR

This paper introduces quantum relational Hoare logic (qRHL), a formal system for reasoning about the relationships between pairs of quantum programs, enabling security analysis of quantum cryptography and protocols.

Contribution

It presents the first quantum extension of probabilistic relational Hoare logic, including its design, implementation, and application to security proofs.

Findings

Developed qRHL for quantum program verification

Implemented a tool for qRHL proof verification

Demonstrated security proofs using qRHL

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.