Paper sets out information-flow security proofs for quantum programs

Noninterference and simulation-based definitions are proved equivalent, with verification via quantum Hoare logic and self-conjugation.

The paper develops semantic foundations and verification methods for secure information flow in quantum programs, where superposition, entanglement, and mixed classical-quantum state make leakage harder to reason about. It defines a noninterference notion that generalizes the classical one and a simulation-based notion that models an attacker, then proves the two equivalent. Standard self-composition fails because of an obstruction analogous to the no-cloning theorem, so the authors introduce self-conjugation using the deferred measurement principle and properties of unitary operations, inside a quantum Hoare logic proof framework. Examples are drawn from the quantum one-time pad, quantum error correction, and anonymous entanglement generation.