题目：       Quantum Relational Hoare Logic with Expectations

　　报告人：    李杨家（中科院软件所）

　　时间地点： 2021.9.15  15:00pm  N420

　　摘要：        Following the spirit of probabilistic relational Hoare logic that was used extensively for computer-verified security proofs of classical cryptographic protocols, quantum relational Hoare logic, a logic for reasoning about pairs of interactive quantum programs, has been proposed in the literature for the security analysis of post-quantum cryptography and quantum protocols. In this talk, I present a variant of the quantum relational Hoare logic that allows us to use "expectations" in pre- and postconditions. That is, when reasoning about pairs of programs, our logic allows us to quantitatively reason about how much certain pre-/postconditions are satised that refer to the relationship between the programs inputs/outputs.