一句话：提出量子关系霍尔逻辑 qRHL，用于推理成对交互式量子程序并支持量子密码安全证明。
论文针对概率关系霍尔逻辑（pRHL）无法分析量子密码的问题，提出量子关系霍尔逻辑（qRHL）。该逻辑用于在给定输入关系的前提下，描述两个交互式量子程序输出之间的关系，其设计需处理量子寄存器相等性等量子特有挑战。作者实现了 qRHL 证明验证工具，并编写了若干量子协议与后量子密码安全性证明示例，为量子密码的形式化安全分析提供了基础。
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.