Toward Protocol-Level Quantum Safety in Bitcoin A Formal, Adversarial, and Invariant-Driven Treatment

Abstract

``Quantum-safe Bitcoin'' is not a property of a subset of well-behaved transactions. It is a global safety property of the consensus state machine: for every reachable consensus state and for every quantum-capable adversary, no consensus-valid execution may contain an unauthorized state transition. This paper specifies an execution model for Bitcoin at the level required for hostile review: explicit \(\mathsf{UTXO}\) state, total validation predicates, deterministic transition functions for transactions and blocks, and a network/scheduler model sufficient to reason about mempool races and reorganizations. We define security goals in game-based form against quantum polynomial-time (QPT) adversaries, separate safety from liveness, and state concrete invariants (authorization integrity, state consistency, and determinism), proving that all invariants are preserved across valid transitions. We give a consensus-level construction for post-quantum authorization (via commit-and-reveal witness programs) and prove, via a complete game-hopping reduction, that unauthorized spends imply a break of the underlying post-quantum signature or hash binding assumptions - with a tight, non-rewinding reduction. We further define and exclude cross-input and cross-transaction witness replay attacks via sighash commitment axioms, formalize network execution as traces and prove that adversarial network control does not bypass PQ authorization, and address the quantum random oracle model. Finally, we formalize the migration dilemma - protocol-level quantum safety cannot be achieved without either freezing unmigrated legacy outputs or accepting open theft under Shor - and provide a formal migration trace model with monotonicity guarantees. All results are supported by formal artifacts: a TLA+ model exhaustively checked by TLC (zero invariant violations across 492 states; concrete counterexample for the migration dilemma) and Coq-mechanized proofs of spend predicate totality, determinism, and parse canonicality.