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.
Wed 16 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
16:37 - 17:43: Quantum ProgrammingResearch Papers at Sala I Chair(s): Jens PalsbergUniversity of California, Los Angeles (UCLA) | |||
16:37 - 16:59 Talk | Quantitative Robustness Analysis of Quantum Programs Research Papers Shih-Han HungUniversity of Maryland, Kesha HietalaUniversity of Maryland, Shaopeng ZhuUniversity of Maryland, Mingsheng YingUniversity of Technology Sydney, Michael HicksUniversity of Maryland, College Park, Xiaodi WuUniversity of Oregon, USA Link to publication DOI Media Attached | ||
16:59 - 17:21 Talk | Game Semantics for Quantum Programming Research Papers Link to publication DOI Media Attached | ||
17:21 - 17:43 Talk | Quantum Relational Hoare Logic Research Papers Dominique UnruhUniversity of Tartu Link to publication DOI Pre-print Media Attached File Attached |