  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.
