{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T11:40:44Z","timestamp":1789904444711,"version":"4.0.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100002301","name":"Eesti Teadusagentuur","doi-asserted-by":"publisher","award":["IUT2-1"],"award-info":[{"award-number":["IUT2-1"]}],"id":[{"id":"10.13039\/501100002301","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA2386-17-1-4022"],"award-info":[{"award-number":["FA2386-17-1-4022"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>We present a logic for reasoning about pairs of interactive quantum programs \u2013 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.<\/jats:p>","DOI":"10.1145\/3290346","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":63,"title":["Quantum relational Hoare logic"],"prefix":"10.1145","volume":"3","author":[{"given":"Dominique","family":"Unruh","sequence":"first","affiliation":[{"name":"University of Tartu, Estonia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-001-0014-7"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2014.57"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_33"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_42"},{"key":"e_1_2_2_5_1","volume-title":"EasyCrypt: A Tutorial. In FOSAD 2012\/2013 Tutorial Lectures. Springer, 146\u2013166","author":"Barthe Gilles","year":"2014"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_2_2_7_1","volume-title":"Crypto 2011 (LNCS)","author":"Barthe Gilles"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009896"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1964621.1964640"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_2_2_11_1","unstructured":"David A. Basin Andreas Lochbihler and S. Reza Sefidgar. 2017. CryptHOL: Game-based Proofs in Higher-order Logic. IACR ePrint 2017\/753 .  David A. Basin Andreas Lochbihler and S. Reza Sefidgar. 2017. CryptHOL: Game-based Proofs in Higher-order Logic. IACR ePrint 2017\/753 ."},{"key":"e_1_2_2_12_1","volume-title":"Eurocrypt \u201994 (LNCS)","author":"Bellare Mihir"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11761679_25"},{"key":"e_1_2_2_14_1","first-page":"175","article-title":"Quantum cryptography: Public-key distribution and coin tossing","author":"Bennett Charles H.","year":"1984","journal-title":"Computers, Systems and Signal Processing. IEEE"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.1"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25385-0_3"},{"key":"e_1_2_2_19_1","unstructured":"CertiCrypt authors. 2013. CertiCrypt: Computer-Aided Cryptographic Proofs in Coq. http:\/\/certicrypt.gforge.inria.fr\/ . Accessed 2018-10-24.  CertiCrypt authors. 2013. CertiCrypt: Computer-Aided Cryptographic Proofs in Coq. http:\/\/certicrypt.gforge.inria.fr\/ . Accessed 2018-10-24."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00417500"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.23.880"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1009378.1009560"},{"key":"e_1_2_2_24_1","unstructured":"CryptoVerif authors. 2018. CryptoVerif: Cryptographic protocol verifier in the computational model. http:\/\/prosecco.gforge. inria.fr\/personal\/bblanche\/cryptoverif\/ . Accessed 2018-10-24.  CryptoVerif authors. 2018. CryptoVerif: Cryptographic protocol verifier in the computational model. http:\/\/prosecco.gforge. inria.fr\/personal\/bblanche\/cryptoverif\/ . Accessed 2018-10-24."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"e_1_2_2_28_1","volume-title":"Toward Automatic Verification of Quantum Cryptographic Protocols. In CONCUR 2015 (LIPIcs)","volume":"42","author":"Feng Yuan","year":"2015"},{"key":"e_1_2_2_29_1","volume-title":"Crypto \u201901 (LNCS)","author":"Fujisaki Eiichiro"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-002-0204-y"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_2_2_32_1","volume-title":"Introduction to Modern Cryptography","author":"Katz Jonathan"},{"key":"e_1_2_2_33_1","unstructured":"Takahiro Kubota Yoshihiko Kakutani Go Kato Yasuhito Kawano and Hideki Sakurada. 2012. Application of a Process Calculus to Security Proofs of Quantum Protocols. In FCS \u201912. 141\u2013147.  Takahiro Kubota Yoshihiko Kakutani Go Kato Yasuhito Kawano and Hideki Sakurada. 2012. Application of a Process Calculus to Security Proofs of Quantum Protocols. In FCS \u201912. 141\u2013147."},{"key":"e_1_2_2_34_1","volume-title":"Automated Verification of Equivalence on Quantum Cryptographic Protocols. In SCSS 2013 (EPiC Series in Computing)","volume":"15","author":"Kubota Takahiro","year":"2013"},{"key":"e_1_2_2_35_1","volume-title":"Chuang","author":"Nielsen Michael A.","year":"2010"},{"key":"e_1_2_2_36_1","volume-title":"LNCS","volume":"2283","author":"Nipkow Tobias","year":"2002"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.85.441"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-002-0133-9"},{"key":"e_1_2_2_40_1","volume-title":"Stein et al","author":"William","year":"2014"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.01.016"},{"key":"e_1_2_2_42_1","unstructured":"The PG dev team. 2018. Proof General (A generic Emacs interface for proof assistants). https:\/\/proofgeneral.github.io\/ . Accessed 2018-10-24.  The PG dev team. 2018. Proof General (A generic Emacs interface for proof assistants). https:\/\/proofgeneral.github.io\/ . Accessed 2018-10-24."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29011-4_10"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46803-6_25"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2817206"},{"key":"e_1_2_2_46_1","unstructured":"Dominique Unruh. 2018a. chsh.ec. https:\/\/raw.githubusercontent.com\/dominique- unruh\/qrhl- tool\/v0.3\/examples\/chsh.ec . Also contained in { Unruh 2018c }.  Dominique Unruh. 2018a. chsh.ec. https:\/\/raw.githubusercontent.com\/dominique- unruh\/qrhl- tool\/v0.3\/examples\/chsh.ec . Also contained in { Unruh 2018c }."},{"key":"e_1_2_2_47_1","unstructured":"Dominique Unruh. 2018b. Chsh.thy. https:\/\/raw.githubusercontent.com\/dominique- unruh\/qrhl- tool\/v0.3\/examples\/Chsh. thy . Also contained in { Unruh 2018c }.  Dominique Unruh. 2018b. Chsh.thy. https:\/\/raw.githubusercontent.com\/dominique- unruh\/qrhl- tool\/v0.3\/examples\/Chsh. thy . Also contained in { Unruh 2018c }."},{"key":"e_1_2_2_48_1","doi-asserted-by":"crossref","unstructured":"Dominique Unruh. 2018c. Verification tool for quantum relational Hoare Logic (artifact accompanying this paper). Available in the ACM Digital Library.  Dominique Unruh. 2018c. Verification tool for quantum relational Hoare Logic (artifact accompanying this paper). Available in the ACM Digital Library.","DOI":"10.1145\/3291619"},{"key":"e_1_2_2_49_1","unstructured":"Dominique Unruh. 2018a. dominique-unruh\/qrhl-tool: Prototype proof assistant for qRHL. GitHub. https:\/\/github.com\/ dominique- unruh\/qrhl- tool Also contained in { Unruh 2018c }.  Dominique Unruh. 2018a. dominique-unruh\/qrhl-tool: Prototype proof assistant for qRHL. GitHub. https:\/\/github.com\/ dominique- unruh\/qrhl- tool Also contained in { Unruh 2018c }."},{"key":"e_1_2_2_50_1","unstructured":"Dominique Unruh. 2018b. qrhl-tool binary distribution version 0.3. https:\/\/github.com\/dominique- unruh\/qrhl- tool\/ releases\/tag\/v0.3 Also contained in { Unruh 2018c }.  Dominique Unruh. 2018b. qrhl-tool binary distribution version 0.3. https:\/\/github.com\/dominique- unruh\/qrhl- tool\/ releases\/tag\/v0.3 Also contained in { Unruh 2018c }."},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1137\/060670997"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2012.37"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32009-5_44"},{"key":"e_1_2_2_56_1","unstructured":"Li Zhou Shenggang Ying Nengkun Yu and Mingsheng Ying. 2018. Quantum Coupling and Strassen Theorem. arXiv:1803.10393 {quant-ph}.  Li Zhou Shenggang Ying Nengkun Yu and Mingsheng Ying. 2018. Quantum Coupling and Strassen Theorem. arXiv:1803.10393 {quant-ph}."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290346","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290346","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290346","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290346"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290346"],"URL":"https:\/\/doi.org\/10.1145\/3290346","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}