**Abstract:**
We present a logic for reasoning about pairs of
imperative 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.