An outpoint is an identifier of the form

interpreted as $(\textsf{txid},\textsf{index})$. An output is a tuple

where $\mathsf{Value}\subset\mathbb{N}$ is a satoshi-denominated value domain and $\mathsf{Script}$ is a consensus-interpreted locking program (e.g., a ScriptPubKey or witness program).

The UTXO set is a finite partial function

We write $U[op]$ for lookup when defined, and $\operatorname{dom}(U)\subseteq\mathsf{OutPoint}$ for its domain.

A transaction is a tuple

where $I=(in_{0},\dots,in_{n-1})$ is a list of inputs, $O=(o_{0},\dots,o_{m-1})$ is a list of outputs $o_{j}\in\mathsf{Output}$, and meta contains consensus-relevant fields (locktime, sequences, etc.). Each input is of the form $in_{i}=(op_{i},w_{i})$ with $op_{i}\in\mathsf{OutPoint}$ and $w_{i}\in\mathsf{Witness}$.

Let $\mathsf{Sighash}(tx,i,\textsf{ctx})\in\{0,1\}^{256}$ be the deterministic sighash function for input $i$ of $tx$ under a consensus context ctx (Taproot defines such a function for SegWit v1 spending) [21, 22]. We will write $m_{i}:=\mathsf{Sighash}(tx,i,\textsf{ctx})$.

The sighash function satisfies commitment if:

1. 1.

   Injectivity (modulo input index): For fixed consensus context ctx and fixed input index $i$,

   	$$\mathsf{Sighash}(tx,i,\textsf{ctx})=\mathsf{Sighash}(tx^{\prime},i,\textsf{ctx})\;\Longrightarrow\;tx\equiv_{\mathrm{cs}}tx^{\prime},$$

   where $tx\equiv_{\mathrm{cs}}tx^{\prime}$ denotes consensus-semantic equivalence: $tx$ and $tx^{\prime}$ are identical in all consensus-critical fields (version, inputs with outpoints, outputs with values and scripts, locktime, and all fields committed to by the sighash). Transactions that differ only in consensus-irrelevant encoding details (e.g., witness serialization padding, future annex content not committed to by the sighash) are considered equivalent under $\equiv_{\mathrm{cs}}$. In particular, if $tx\equiv_{\mathrm{cs}}tx^{\prime}$ then $\mathsf{ValidTx}(U,tx)=\mathsf{ValidTx}(U,tx^{\prime})$ and $\delta_{\mathsf{Tx}}(U,tx)=\delta_{\mathsf{Tx}}(U,tx^{\prime})$ for all $U$.

2. 2.

   Cross-input separation: For $i\neq j$ in the same transaction,

   	$$\mathsf{Sighash}(tx,i,\textsf{ctx})\neq\mathsf{Sighash}(tx,j,\textsf{ctx}).$$

3. 3.

   Field coverage: $\mathsf{Sighash}(tx,i,\textsf{ctx})$ commits to all consensus-critical fields of $tx$ (version, inputs with their outpoints, outputs with their values and scripts, locktime) and to the spent output’s script and value.

Two transactions $tx,tx^{\prime}$ are consensus-semantically equivalent, written $tx\equiv_{\mathrm{cs}}tx^{\prime}$, if they agree on all fields that affect consensus validation and state transition:

1. 1.

   version, locktime, and sequence numbers;

2. 2.

   the list of input outpoints $(op_{0},\dots,op_{n-1})$;

3. 3.

   the list of outputs $(o_{0},\dots,o_{m-1})$ including values and scripts;

4. 4.

   all fields committed to by the sighash function.

The equivalence class $[tx]_{\mathrm{cs}}$ is the quotient of the transaction space by $\equiv_{\mathrm{cs}}$. Transactions in the same class may differ in consensus-irrelevant encoding details (e.g., witness serialization padding, non-committed annex content, or byte-level encoding choices that do not affect $\mathsf{ValidTx}$ or $\delta_{\mathsf{Tx}}$). By construction: $tx\equiv_{\mathrm{cs}}tx^{\prime}$ implies $\mathsf{ValidTx}(U,tx)=\mathsf{ValidTx}(U,tx^{\prime})$, $\delta_{\mathsf{Tx}}(U,tx)=\delta_{\mathsf{Tx}}(U,tx^{\prime})$, and $h(tx)=h(tx^{\prime})$ for all $U$.

We formalize the quotient via a canonical normalization function:

$\mathsf{Norm}$ strips all consensus-irrelevant fields and produces a unique representative of each equivalence class. Concretely, $\mathsf{Norm}(tx)$ retains exactly the fields enumerated in items 1–4 above and sets all other fields to a fixed canonical value (e.g., empty witness, zero-length annex). The sighash commitment property (Definition 5, item 1) can then be restated as:

This eliminates any ambiguity about what “equivalent” means: two transactions are equivalent if and only if they have the same canonical representative.

Transaction validation is a predicate

defined as

where $\textsf{WitnessOK}(U,tx)$ expands to:

with $(\cdot,\pi_{i})=U[op_{i}]$ and $m_{i}=\mathsf{Sighash}(tx,i,\textsf{ctx})$.

The transaction transition function

is defined (for all inputs) by removing spent outpoints and adding newly created outpoints:

where $h(tx)\in\{0,1\}^{256}$ is the canonical transaction id and $j$ ranges over the output indices.

The transaction id function $h:\mathsf{Tx}\to\{0,1\}^{256}$ satisfies collision resistance if for all QPT adversaries $\mathcal{A}_{q}$:

The system requirement is not generic collision search in a vacuum but collision against the active identifier set: for any reachable state $U$ and any new transaction $tx$, the newly created outpoints $(h(tx),j)$ must not collide with any $op\in\operatorname{dom}(U)$. This is a weaker requirement than arbitrary collision resistance: the adversary must find a collision against a specific, evolving set of existing identifiers rather than against an arbitrary second preimage.

A block is $B\in\mathsf{Blk}:=(\textsf{hdr},(tx_{0},\dots,tx_{k-1}))$. Block validation is a predicate $\mathsf{ValidBlk}:\mathsf{UTXO}\times\mathsf{Blk}\to\{0,1\}$ requiring PoW validity and sequential transaction validity (coinbase rules elided here for brevity). The block transition function $\delta_{\mathsf{Blk}}:\mathsf{UTXO}\times\mathsf{Blk}\to\mathsf{UTXO}$ applies $\delta_{\mathsf{Tx}}$ sequentially:

A safety property is a predicate $P$ such that for every execution trace $\tau$ of the consensus state machine, if $\tau$ violates $P$ then there exists a finite prefix of $\tau$ that already violates $P$. Operationally: an explicit “bad event” occurs.

A liveness property is a predicate $Q$ such that for every finite execution prefix, there exists an extension where $Q$ holds. Operationally: assuming adequate network and mining conditions, honest transactions eventually confirm.

Block validation enforces:

where $C_{\max}$ is a consensus-enforced constant (analogous to the 4 MWU weight limit in current Bitcoin).

$G_{0}$ is identical to $\mathsf{AuthBreak}^{\mathcal{A}_{q}}(\lambda)$ (Definition 16). The challenger samples $(\mathsf{sk},\mathsf{pk})\leftarrow\mathsf{Kg}(1^{\lambda})$, sets $P:=H(\mathsf{pk})$, gives $P$ and signing oracle access to $\mathcal{A}_{q}$. $\mathcal{A}_{q}$ outputs $(m^{\star},w^{\star})$ and wins if $\mathsf{SpendPred}_{\mathrm{PQ}}(P,m^{\star},w^{\star})=1$ with $m^{\star}$ unqueried.

$G_{1}$ is identical to $G_{0}$ except: after $\mathcal{A}_{q}$ outputs $(m^{\star},w^{\star})$ with $\textsf{Parse}(w^{\star})=(\mathsf{pk}^{\star},\sigma^{\star})$, if $H(\mathsf{pk}^{\star})=P$ but $\mathsf{pk}^{\star}\neq\mathsf{pk}$, the game sets $\mathsf{bad}:=\mathsf{true}$ and the adversary still wins. Otherwise the game proceeds identically.

$G_{2}$ is identical to $G_{1}$ except: if $\mathsf{bad}=\mathsf{true}$ (i.e., $\mathsf{pk}^{\star}\neq\mathsf{pk}$ but $H(\mathsf{pk}^{\star})=P$), the adversary loses (the game outputs $\mathrm{0}$).

The game $\mathsf{CrossInput}^{\mathcal{A}_{q}}(\lambda)$ is:

1. 1.

   Challenger samples $(\mathsf{sk},\mathsf{pk})\leftarrow\mathsf{Kg}(1^{\lambda})$, sets $P:=H(\mathsf{pk})$.

2. 2.

   Challenger creates a transaction $tx$ with two inputs $i\neq j$, both spending outputs locked to $P$, and provides $\mathcal{A}_{q}$ with a valid witness $w_{i}$ for input $i$.

3. 3.

   $\mathcal{A}_{q}$ wins if it produces a valid witness $w_{j}$ for input $j$ without querying the signing oracle on $m_{j}:=\mathsf{Sighash}(tx,j,\textsf{ctx})$.

The game $\mathsf{CrossTx}^{\mathcal{A}_{q}}(\lambda)$ is:

1. 1.

   Challenger samples $(\mathsf{sk},\mathsf{pk})\leftarrow\mathsf{Kg}(1^{\lambda})$, sets $P:=H(\mathsf{pk})$.

2. 2.

   Challenger creates transaction $tx$ spending an output locked to $P$ at input $i$, and provides $\mathcal{A}_{q}$ with the valid witness $w$.

3. 3.

   $\mathcal{A}_{q}$ constructs a different transaction $tx^{\prime}\neq tx$ with an input $i^{\prime}$ spending an output locked to $P$.

4. 4.

   $\mathcal{A}_{q}$ wins if $w$ is a valid witness for input $i^{\prime}$ of $tx^{\prime}$ without querying the signing oracle on $m^{\prime}:=\mathsf{Sighash}(tx^{\prime},i^{\prime},\textsf{ctx})$.

An execution trace is a sequence

where $U_{0}$ is the genesis UTXO set and each transition satisfies $\mathsf{ValidBlk}(U_{t-1},B_{t})=1$ and $U_{t}=\delta_{\mathsf{Blk}}(U_{t-1},B_{t})$. We write $\tau[0..t]$ for the prefix up to state $U_{t}$.