No-Cloning Meets No-Leaking: A Formal Framework for Proving Quantum Programs Don't Spill Secrets

First equivalence proof linking noninterference and simulation-based security for quantum programs, plus a verification method that sidesteps the no-cloning barrier via a novel self-conjugation trick.

Imagine you're a building inspector who checks for fire safety by walking through two identical copies of a building — one with a fire, one without — and confirming that the exits behave the same way. That's self-composition, the standard trick for verifying information-flow security in classical programs. Now imagine the building is made of quantum material that physically cannot be copied. You can't build the second copy. That's the obstruction this paper solves. The committed claim: for the first time, there exist two formally equivalent definitions of information-flow security for quantum programs — noninterference-based (the program's public outputs don't depend on secret inputs) and simulation-based (an explicit attacker model can't distinguish secret-dependent executions) — and a practical proof framework to verify them. The equivalence itself is the load-bearing result. Classical security theory long ago established this kind of duality, but quantum mechanics breaks the standard proof route. The core technical contribution is self-conjugation, a replacement for the classical self-composition technique. Where classical verification duplicates a program and runs both copies, self-conjugation exploits the deferred measurement principle and unitarity to effectively run a program against its own conjugate transpose — no cloning required. This is not a hack or approximation; it's a principled semantic move that turns the no-cloning obstruction into a feature. The proof framework is built atop quantum Hoare logic, extending existing quantum program verification infrastructure rather than inventing from scratch. The paper validates the framework on three canonical quantum protocols: the quantum one-time pad (encryption), quantum error correction (fault tolerance), and anonymous entanglement generation (multiparty privacy). These are not toy examples — they're standard benchmarks in quantum cryptographic literature, and the proofs demonstrate that the framework handles the full range of quantum weirdness: superposition, entanglement, measurement, and classical-quantum interaction. On the integrity front, this is a theory paper graded by mathematical proof, not simulation or experiment. The definitions are stated precisely, the equivalence theorem is proved, and the proof rules are shown to be sound relative to quantum Hoare logic. There's no empirical benchmark to game here — the validation is whether the proofs are correct. The paper is 61 pages with 13 figures, which signals thoroughness rather than padding; quantum information-flow semantics genuinely requires this level of detail. The ladder question is interesting. The closest prior work is in quantum type systems and quantum process algebras for security (e.g., Feng et al., Gay & Nagarajan), but none have established the noninterference–simulation equivalence for a full quantum while-language with classical-quantum interaction. Classical noninterference theory (Goguen & Meseguer, 1982) and simulation-based security (Canetti's UC framework) are the intellectual ancestors, but neither extends to quantum mechanics without the self-conjugation move. The obvious successor experiment is mechanization — encoding these proofs in a theorem prover like Coq or Lean, which the authors do not attempt. The honest read: this is a 61-page pen-and-paper proof, and mechanization is a full follow-on project (likely paper #2). Scaling to verify real quantum compiler output or integrating with emerging quantum programming languages (Silq, Qiskit) is the practical next step that would move this from theory to tooling.