**Abstract:**
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.