一句话：提出带幽灵变量的量子 Hoare 逻辑扩展，增强前后条件表达能力，并验证量子一次性密码本安全性。
量子 Hoare 逻辑用于推理量子程序，但其前后条件难以表达变量的分布、是否具有经典内容等性质。本文引入“幽灵变量”（ghost variables）扩展量子 Hoare 逻辑：幽灵变量不出现在被验证程序中，可处于任意量子态（存在量化），并可和程序变量纠缠，从而显著增强前后条件的表达能力。作者以量子一次性密码本（quantum one-time pad）为案例，展示该逻辑可用于证明其安全性。
Quantum Hoare logic allows us to reason about quantum programs. We present an extension of quantum Hoare logic that introduces “ghost variables” to extend the expressive power of pre-/postconditions. Ghost variables are variables that do not actually occur in the program and are allowed to have arbitrary quantum states (in a sense, they are existentially quantified), and be entangled with program variables. Ghost variables allow us to express properties such as the distribution of a program variable or the fact that a variable has classical content. And as a case study, we show how quantum Hoare logic with ghost variables can be used to prove the security of the quantum one-time pad.
DOI 原文 ·
@inproceedings{paperbot4998,
title = {Quantum Hoare Logic with Ghost Variables},
author = {Dominique Unruh},
booktitle = {LICS},
year = {2019},
doi = {10.1109/lics.2019.8785779}
}