Abstract

Smart contracting protocols promise to regulate the transfer of cryptocurrency amongst participants in a trustless manner. A safe smart contract implementation should ensure that each participant can always append a contract transaction to the blockchain in order move the contract towards secure completion. To this goal, we propose Bitcoin Trace-Net, a contract verification framework which generates an executable symbolic model from the underlying contract implementation. A Trace-Net model consists of a Petri Net formalism enriched with a Dolev-Yao-like actor knowledge model. The explicit symbolic actor knowledge model supports the verification of contracts featuring cryptographic sub-protocols, which may not be observable on the blockchain. Trace-Net is sufficiently expressive to accurately model blockchain semantics such as the delay between a transaction broadcast and its subsequent confirmation, as well as adversarial blockchain reorganizations of finite depths, both of which can break smart contract safety. As an implementation-level framework, Trace-Net can be instantiated at run-time to monitor and verify smart contract protocol executions.

^{Keywords: Bitcoin; smart contracts; symbolic analysis; model checking}

1. Introduction

The term "smart contracts" is commonly attributed to Nick Szabo [1], who is known for his early work on digital cash and digital contracts. Smart contracts promise contract implementations between actors to be executed in a trustless manner without reliance on any trusted intermediaries. To this goal, blockchain protocols offer both permissionless execution and immutability of transactions. These properties promise the realization of trustless smart contracts which are safely executable by any contract participant and robust against any adversarial actions by counter-parties. More formally, we are interested in verifying contracts for execution traces which lead to safe outcomes. If the state space of the contract is finite, such a safety notion expressed as a trace property is decidable. In practice, many smart contracts are implemented in general-purpose Turing-complete languages and thus cannot be definitively verified for trustless execution. Instead, substantial attention has been directed towards the analysis of vulnerability patterns [2] on more expressive contracting platforms such as Ethereum. Static analysis of smart contracts to avoid vulnerability patterns [3] can be highly effective in finding bugs. However they cannot prove the absence of any unintentional contract behavior and therefore cannot fully deliver on the original promise of trustless smart contract execution.

Contracts implemented in Bitcoin are famously Turing-incomplete and feature finite state-spaces due to its limited expressiveness of the underlying Script language. Bitcoin as a contracting platform therefore lends itself to verification with model-checking approaches. This has been thoroughly investigated by Bartoletti & Zunino with BitML [4] [5] [6] [7] [8], a higher-level contract specification language for Bitcoin which compiles to Bitcoin transactions, appendable to the Bitcoin blockchain by the contracting participants. BitML can be symbolically executed at the language level and provides safe compiler guarantees so that honest actors can always move the specified contract forward during execution: this is a big step towards secure smart contract development since safety properties can be guaranteed at design time. However, contract specification languages at a higher abstraction level come at the cost of expressiveness when compared to designing contracts at the raw Bitcoin transaction level: implementing smart contracts directly at the computational level is unwieldy; it can also enable optimizations for higher on-chain privacy or lower execution costs. For contracting protocols such as atomic swaps [9], lightning [10], or state-channels [11], where on-chain transaction privacy or cost efficiency are paramount, BitML may not be the appropriate implementation and verification tool.

Instead, Trace-Net is intended as an implementation-level verification framework. As such, we also emphasize the need to accurately model blockchain semantics such as the delay between a transaction broadcast and its confirmation, as well as possible blockchain reorganizations [12] [13] executed by the adversary, both of which can break the security of a smart contract design. Recent protocol specification errors in the Bitcoin Lightning [14] protocol, for example, also indicate that the verification of contracts developed at the Bitcoin implementation level remain an open challenge. Bitcoin contracting protocols have been verified with cryptographic frameworks [15], but manual security proofs cannot be automated for different contract designs.

Contributions

We introduce Trace-Net as an automated contract verification framework applicable at the the transaction level of UTXO-based blockchain protocols. Trace-Net generates an executable contract model from the symbolic execution of unsigned transactions implementing an interactive contract protocol: this symbolic contract model consists of an extended Petri Net formalism representing on-chain contract states and an extensible Dolev-Yao-like [16] actor knowledge model, which expresses the actor’s ability to derive knowledge from observations and publicly known cryptographic functions. Modeling actor knowledge explicitly allows Trace-Net to be extended with additional cryptographic sub-protocols which may be unobservable on-chain (such as adaptor signatures [11]) and can therefore support a wide range of contract protocol designs. Furthermore, separate modeling of on-chain and actor knowledge states enable Trace-Net to express blockchain reorganizations which may occur during contract execution: such an event will reorder transactions whilst retaining the states of each actor’s knowledge. Blockchain reorganizations can frequently occur on blockchains with less hash power and contracts may need to be verified against such events. To the best of our knowledge, Trace-Net is the first automated approach enabling the verification of safety properties in the presence of adversarial blockchain reorganizations.

The Trace-Net contract model is unfolded into a finite-state transition system, for which temporal properties are decidable: in particular we introduce a formalization of the trustless execution property, which intuitively holds true if a contract can be safely terminated by the verifying agent despite any adversarial strategies executed by the counter-party. The positive verification of the trustless execution property results in the identification of all safe strategies for the verifying actor, which can be enforced at run-time. The verification of this property can be extended to determine the safety of contract updates which may occur during contract execution. Furthermore, we introduce the formal notion of contract stability, which describes the safety of remaining in an intermediary, non-terminal contract state: this is a useful notion for the verification of off-chain contracts such as state-channels, where the termination of a live contract protocol is deferred so that it can be updated at a later point in time.

We believe Trace-Net introduces the following promising implications: firstly, given a higher level specification of the contract, Trace-Net can be instantiated to ensure implementation correctness, by verifying that trace properties of the specification are also present at the implementation level. Of course, a contract protocol can also be verified against general safety policies expressed as temporal, trace properties, such as trustless execution and contract stability. Thirdly, the ability to perform automated verification at run-time can be useful for monitoring contract protocol executions. Dedicated key management systems in secure execution environments tasked with the secure signing of transactions could enforce universal safety policies at signing-time: otherwise, safe signing approaches must rely on contract-specific transaction pattern matching [17] which cannot be generalized to other contract types and cannot formally guarantee any contract safety properties.

Organization

The rest of the paper is organized as follows. In Section 2 we summarize existing work relevant to our solution but also provide a wider overview of approaches to formal correctness in smart contract design. In Section 3 we introduce our model of Bitcoin transactions and their symbolic execution. Subsequently, the Trace-Net framework (Section 4) is introduced which consists of actor knowledge models (Section 4.1, Section 4.1.1) and an on-chain Petri Net (Section 4.2) formalism derived from the previous symbolic execution of the underlying transactions. Finally, Section 5 and Section 6 are dedicated to the automated generation and analysis of the Trace-Net model for security properties such as trustless execution, contract update safety and contract state stability.

2. Related Work

Efforts to provide correctness guarantees in smart contracts inherently face trace-offs between the expressiveness of the implementation language and the decidability of the security properties of interest. In this section, we aim to provide a brief overview of the spectrum of formal frameworks and languages intended to ensure contract correctness and safety.

Analysis of Bitcoin Script

The Bitcoin Script language is non-Turing-complete and often used as an implementation language for various contracting protocols such as atomic swaps [9], coin join [18] variants, payment channel networks [10], generalized state channels [11] and other contract designs surveyed by past literature [19]. However, even though the limited expressiveness of Bitcoin Script is often claimed to facilitate the manual investigation of its behavior, only a fragment of its language has been formalized (Klomp & Bracciali [20]), which makes symbolic execution and formal verification of Bitcoin Script challenging. Miniscript [21] [22] [23] is a practical framework that enables symbolic execution of composable Bitcoin Script fragments, and is used by Trace-Net to lift a symbolic model from raw contract transactions. We note, however, that it is ultimately difficult to reason about the correctness of Miniscript given that the underlying Bitcoin Script semantics are only informally described. Nonetheless, developing contracts at the Bitcoin Script and transaction level provides the flexibility of optimizing the on-chain footprint for privacy and reduced execution cost.

Contracts as Cryptographic Protocols

Analysis of individual Bitcoin output scripts remains insufficient to reason about the execution of interactive Bitcoin contracts implemented over multiple transactions. The cryptography community has successfully instantiated the Universal Composability [15] framework to manually prove the security of interactive contracts designs [24] [11]. Alternatively, Andrychowicz et al. have proposed to model contract participants as timed automata [25] executing an interactive protocol, such that possible contract executions can be exhaustively explored in a model checker such as UPPAAL. This latter approach, however, still requires a contract model to be manually specified. Trace-Net builds upon past work on both symbolic Bitcoin Script execution and the treatment of Bitcoin contracts as interactive, cryptographic protocols and offers the ability to automatically generate a symbolic, executable model from raw transactions.

FSM Contract Languages

BitML by Bartoletti & Zunino [4] [5] [6] [7] [8] is a high-level contracting language for Bitcoin which features safe execution guarantees provided by compiler semantics. BitML is an elegant process algebra intended for the implementation of smart contracts, but can also be executed at the symbolic language level, providing a secure tool to the contract designer to ensure design intent and contract implementation are in agreement. Furthermore, executable BitML expressions are highly amenable to the verification of general safety properties, such as liquidity [7], which ensures that funds are never locked inside a contract design. Because the symbolic execution of BitML expressions can always be unfolded into a finite state transition system, we denote BitML as a FSM contract language, over which temporal properties are decidable. The higher level BitML abstraction and its security guarantees come at the cost of reduced control of the resulting on-chain footprint during contract execution, which may affect its usefulness in applications which emphasize on-chain privacy or execution cost.

We note that general-purpose Turing-complete languages such as Solidity can also be represented in FSM-like form, making it amenable to verification. FSolidM by Mavridou & Laszka [26] [27] [28] is a high-level contract language which translates to Solidity. FSolidM is an adapted form of the Behavior, Interaction, and Priority (BIP) framework [29] and aims to introduce rigorous control state and contact execution transition semantics. This has the potential of making the verification of some safety properties decidable, in particular temporal properties over user-defined control states using symbolic execution and predicate abstraction techniques.

Typed Functional Languages

Strong typing systems can enforce the absence of many generalized vulnerability patterns. Furthermore, functional languages lend themselves towards translation into theorem proving frameworks, where assisted proofs for contract properties can be performed. Simplicity by O’Connor [30] is a typed functional contract language intended for UTXO-blockchains such as Bitcoin, with execution semantics formalized in Coq. Scilla [31] [32] draws inspiration from both functional and automata-based languages, but ultimately represents a functional language with an adaptor to Coq. Importantly, Scilla implements inter-contract communication as functions without side-effects: a contract in an account-based blockchain platform can only call an external contract at the very end of a function execution, so that no external effects are possible in the midst of a function, thereby preventing reentrancy [19] vulnerabilities and also facilitating the implementation of inter-blockchain contract messaging in sharded blockchains.

Detection of Vulnerability Patterns

Both static analysis [33] [34] [35] [36] and theorem proving approaches [37] [38] [39] [40] have been successfully deployed to detect generalized vulnerabilities previously exploited on the Ethereum blockchain. Vulnerability patterns frequently arise when there is a mismatch between the intuition of the developer and the underlying execution semantics of the blockchain. In Ethereum, common vulnerability patterns include the reentrancy [2] problem, transaction ordering, block timestamp dependency, call stack depth limitation, unchecked send and suicidal contracts [41]. Static analysis tools, however, cannot guarantee the absence of bugs, nor can they guarantee contract safety, although VerX [35] has demonstrated decidability of contract-specific temporal properties for a fragment of the EVM language.

Domain-specific Contract Languages

Finally, we note that domain-specific contracting languages have been proposed for specific contract archetypes. The financial contract language from Bahr et al. [42], for example, provides very simple expressions for traditional financial contracts formalized by Peyton Jones et al. [43]. These include foreign exchange swaps and options, credit default swaps, and portfolios holding contracts with multiple counter-parties. Marlowe [44] provides a language to compile such contract types in form of [43] to the Cardano blockchain run-time. “Trustless” contract execution of such contracts is guaranteed by the execution framework [45] targeting the EVM run-time, though formalized compiler semantics do not exist to the best of our knowledge. Findel [46] is another DSL for financial derivatives executed on Ethereum. We presume that additional domain-specific contracting languages will emerge as blockchain platforms and smart contract applications mature.

3. Symbolic Execution of Bitcoin Transactions

We begin this section with a simplified model of Bitcoin transactions and their general execution for the general reader. In the subsequent Section 3.1, we introduce the symbolic execution of transaction scripts with Miniscript semantics (Section 3.2), resulting in symbolic execution paths for each transaction output. Section 3.3 outlines accurate transaction confirmation on the blockchain, which requires finite delays between the initial transaction broadcast and its inclusion in the blockchain: we do not model transaction confirmations as final, but account for a possibility of blockchain reorganizations of finite depths by an adversarial actor.

Transaction Anatomy

A Bitcoin transaction consists of the attribute tuple $(tx.\textsf{id}, tx.\vec{\textsf{ins}}, tx.\vec{\textsf{outs}}, tx.\textsf{after})$, where $\vec{\textsf{ins}}$ and $\vec{\textsf{outs}}$ are input and output vectors respectively. Transaction outputs represent funds which are spendable. A single transaction input always refers to a single output of a previous transaction in the blockchain, thereby forwarding or spending its value to outputs of the spending transaction (Figure 1).

The $tx.\textsf{id}$ attribute is unique to each transaction and is obtained by hashing the transaction byte string in network serialization form which encodes the inputs, outputs and after attributes. The $tx.\textsf{after}$ transaction attribute encodes a transaction level time-lock and is detailed in the subsequent transaction time-locks paragraph.

Each input in a Bitcoin transaction is represented by an attribute tuple $(in.\textsf{prevout}, in.\textsf{older}, in.\textsf{witness})$. The $in.\textsf{prevout}$ attribute uniquely references the redeemed output in an output vector of a previously confirmed transaction with a $(txid,index)$ pair. The $in.\textsf{older}$ attribute encodes a minimum delay which must pass before the transaction can be included in the blockchain: this delay begins at the time when the referenced output is finalized in the blockchain. The witness encodes input arguments which satisfy the script of the output it spends.

An output is described with the attribute tuple $(out.\textsf{value}, out.\textsf{script})$. The difference between the sum of the output values of a transaction and the value sum of the output referenced by the transaction inputs is denoted as the $fee$ which is rewarded to the miner of the block. An output script is a string of operators and is only executed during the validation of a spending transaction, with the spending input witness providing the input arguments to the script execution. This is detailed in the following paragraph.

Spending of Outputs

Transactions in Bitcoin are intended to transfer the ownership of output values from one participant to another which requires a global ordering of all transactions. Although transactions are grouped in "blocks" in the blockchain, the ordering of all transactions in the blockchain is total. An output can only be redeemed or "spent" by a single input of a transaction ordered thereafter. An output from a confirmed transaction which is not yet redeemed is denoted as an unspent transaction output, or UTXO.

In order for a transaction to be valid, all its inputs must contain witnesses which satisfy conditions expressed in the output script being spent. When a newly broadcast transaction is verified, all scripts of each output it redeems are executed against the respective input witnesses to ensure correct satisfaction. A successful spend of an output requires the script to complete without run-time errors and the script stack to contain a non-zero value stored in the top stack element.

An illustrative output script ($in.prevout.script$) and input witness ($in.witness$) pair are shown below. Note that the witness is copied element-by-element (${w_0, w_1, ..., w_m}$) into an in-memory execution stack ($stack_{init}$) before the script validation run is performed.

The script is executed opcode-by-opcode beginning with its first operator $OP_0$ and $stack_{init}$ until $OP_n$ has been completed. Operator types can read, write or delete the upper region of the script stack. Alternatively, some operator types will perform control flow. Once $OP_n$ is completed, the resulting top stack element must be non-zero for the script evaluation to be successful, thereby validating the input witness under consideration.

Transaction Time-locks

In aggregate, the transaction time-locks at the input and transaction levels result in an earliest possible broadcast time for a given transaction. The earliest broadcast time is the blockheight at which all after and older time-locks in a transaction have released and the transaction can be broadcast and amended to the blockchain.

After time-locks are encoded at the transaction level, and encode an absolute time until which the transaction is time-locked. For example, transaction $A$ in Figure 1 is time-locked until blockheight 45.

Older time-locks are encoded in each transaction input, which enforces a minimum age of the output being spent. In Figure 1, for example, input 0 of transaction $C$ encodes an after time-lock of two blocks, which requires transaction $A$ to be at least two blocks old when transaction $C$ is broadcast: this time-lock releases at the blockheight $46 + 2 = 48$, since transaction $A$ was amended in block $46$.

The earliest firing time of a transaction occurs when all after and older time-locks have released. The After time-lock of transaction $C$ in Figure 1 releases at blockheight 49, and the older time-locks at 48 and 50 respectively, given the age of the previous outputs. As a result, the effective earliest broadcast time of transaction $C$ is blockheight 50.

3.1 Symbolic Script Execution

In order to establish an executable, symbolic model of contract transactions, we must be able to perform a symbolic execution of each transaction output script. The intended purpose of an output script is to encode spending conditions, which must be satisfied by the witness of a valid transaction input. A more detailed description of Bitcoin script instruction set semantics can be found in [47] or in the Bitcoin Core source code [48]. Most importantly, a Bitcoin script encodes a finite set of execution paths $\gamma = \gamma_{0} \vee ...\vee \gamma_{n}$. Each output execution path implies a unique set of constraints on the spending input witness, which can be obtained from the symbolic execution of the output script. We have previously noted that symbolic execution is only possible for a fragment of Script [20] and remains an open challenge. Nonetheless, we illustrate symbolic script execution with Miniscript in Section 3.2 which relies on an informal definition of the underlying Bitcoin script fragment semantics.

Definition 3.1 (Symbolic Witness): A symbolic witness $\Gamma$ is a unique set of constraints imposed on the individual elements of the spending input witness by an output script. Any input witness which satisfies $\Gamma$ is a valid input witness.

The following relationship between an input witness $w$ and a symbolic witness $\Gamma$ holds true if the witness satisfies the constraints imposed by the symbolic witness.

Furthermore, we can define a symbolic execution function $sat(output)$ which returns a set of symbolic witnesses $\bar\Gamma$ containing the $n$ alternative script execution paths $\gamma_{0} \vee ...\vee \gamma_{n}$ of the output script.

For simplicity, we denote $sat(in)$ to mean $sat(in.prevout)$, which returns the symbolic witnesses of the output being spent by $in$. In order to express symbolic witnesses, we adapt and simplify the constraint expressions introduced in [20]. In particular, we wish to describe an input witness stack $(w_0, w_1, ..., w_n)$ in terms of constraints imposed on each of its elements. The following set $C$ of constraint expressions consists of symbolic witness stack elements $w_{j}$, constant byte strings $b$, constant integers $i$, relational operators and functional expressions such as signature, hash and size:

The symbolic expression $sig \: w_{0} \: pk_{A}$, for example, constrains the first witness stack element ($w_{0}$) to be a valid signature of the transaction signed by the private key $inv(pk_{A})$. The expression $hash \: w_{1} = b_{32}$ constrains the second witness stack element to be the hash pre-image of a 32-byte constant $b_{32}$: here, $hash$ represents a specific hash function supported by the Bitcoin script language which produces a 32-byte digest. The time-lock constraint $older>=i$ in $C$ constrains the value of the $in.\textsf{older}$ attribute and not the witness element directly.1 The $after>=i$ time-lock constraint is imposed on the spending transactions $tx.\textsf{after}$ attribute. Example 3.2 illustrates a symbolic witness composed of symbolic expressions from $C$ for a hash time-lock contract. Our simplified set of constraint expressions can only express symbolic execution of a subset of Bitcoin $Script$, but it is nonetheless sufficiently expressive to describe symbolic execution of Miniscript, which in turn can implement many commonly deployed Bitcoin contracting protocols [9], [18], [10], [11].

We proceed to denote several definitions which can be derived from the analysis of symbolic witnesses. Firstly, if for a specific output execution path an actor can exclusively generate a witness which satisfies the respective symbolic witness, this output path is owned by the actor.

Definition 3.2 (Output Path Ownership): An output path is owned by an actor if $\Gamma \in sat(output)$ and it only features constraints which the actor can exclusively satisfy.

Such an execution path can be spent anytime by its owner. Of course, the same output may feature alternative execution paths spendable by other actors and thus have multiple owners. If the actor can only exclusively produce the signatures of a given output execution path, but does not have the required knowledge to fulfill other non-signature witness constraints, it won’t be able to move the funds. However, this actor still maintains control over where the funds can be sent for this given output execution path, as the destination outputs are committed by the actor signatures alone. An actor owns an output if it owns all output execution paths.

Definition 3.3 (Output Path Control): An output execution path is controlled by an actor, if it can exclusively satisfy all signature expressions in the respective symbolic witnesses in $\Gamma \in \bar\Gamma$: an actor controlling an output path controls the destination of the output funds when spending along that specific output execution path.

We now consider the implications of a transaction spending multiple unspent outputs which each feature multiple, alternative symbolic witnesses $(|\bar\Gamma_{i}| > 1).$ The spending transaction needs only to satisfy one symbolic witness per input , resulting in a combinatorial expansion of valid, unique witness sets for the spending transaction.

Definition 3.4 (Symbolic Witness Permutation) Given a transaction and its inputs ($in_0$, $in_1$,...), each with a possible set of symbolic witnesses $sat(in_i) = \bar\Gamma_i = \{ \Gamma_{0,i}, \Gamma_{1,i}, ... \}$, multiple permutations of valid witness sets are possible over this multiset of symbolic witnesses. A symbolic witness permutation $\pi_i$ for a transaction $tx$ is a unique combination of symbolic witnesses for each tx input. Notation: $\pi(tx)=\{\pi_0, \pi_1, ...\}$ denotes all possible symbolic witness permutations for a given transaction $tx$.

We conclude this section by illustrating the different script execution paths of a commonly used script pattern called the hash time-locked contract (HTLC).

Example 3.1 (Hash Time-locked Contract) The following Bitcoin $Script$ example has two different spending conditions $\gamma_{0} \vee \gamma_{1}$, where $\gamma_{0}$ is encumbered with a hash-lock and public key $pk_A$ and $\gamma_{1}$ is encumbered with a delay of 10 blocks and the public key $pk_B$. This script type is commonly referred to as a Hash Time-locked Contract (HTLC), denoting the two script execution paths.

<PK_A> OP_CHECKSIG
OP_NOTIF
  <PK_B> OP_CHECKSIGVERIFY
  <10> OP_CHECKSEQUENCEVERIFY
OP_ELSE
  OP_SIZE <32> OP_EQUALVERIFY
  OP_SHA256 <B_32> OP_EQUAL
OP_ENDIF

The first execution path $\gamma_{0}$ requires a transaction signature created with the private key $inv(pk_{A})$ (line 1) and the $sha256$ preimage to the digest $b_{32}$ (Lines 6, 7). Alternative execution path $\gamma_{1}$ can be spent with a transaction signature with the private $inv(pk_{B})$ (Line 3) and a time delay of 10 blocks (Line 4) after the transaction featuring this script has been amended to the blockchain. Symbolic witnesses $\Gamma_{0}$ and $\Gamma_{1}$ for $\gamma_{0}$ and $\gamma_{1}$ of this HTLC are expressed below with constraint Expressions (1) from $C$ as follows:

The symbolic witnesses provide the necessary information for an actor to determine whether it can deduce a valid witness for a Bitcoin $Script$ from its knowledge. For example, an actor with the knowledge of $inv(pk_{A})$, the sha256 preimage of $b_{32},$ and the symbolic witness $\Gamma_{0},$ will be able to produce a two element witness stack which satisfies $\Gamma_{0}$ (or the execution path $\gamma_0$).

We have now defined symbolic witnesses which satisfy specific output execution paths of a Bitcoin output script and demonstrated this information can be used to generate a valid input witness. As previously noted, there exists no full formalization of the Bitcoin script language to enable symbolic execution of the entire Bitcoin $Script$ language to the best of our knowledge. For a subset of Script, Klomp & Bracciali [20] have formalized the semantics of individual script operations, so that the constraints expressions in the symbolic witness can be inferred step-wise during the symbolic execution of each script command. Alternatively, we propose to make use of the symbolic analysis framework which Miniscript provides, which covers a useful fragment of Bitcoin $Script$.

3.2 Miniscript

This introductory section on Miniscript is not required for the comprehension of Trace-Net and can be skipped by the reader, but we include it nonetheless as Miniscript provides a useful framework for symbolic execution of the underlying Script fragments, with which a Trace-Net model can be instantiated.

Terms in the Miniscript language $M$ each express a unique $Script$ template, consisting of one or more $Script$ operations. Terms are composable according to Miniscript semantics to produce additional expressions, as shown in the first column of Table 1. The semantics of the underlying Bitcoin $script(m)$ of each Miniscript term $m$ are captured by $type(m)$ and type modifier properties. We refer to [21] for a full description of Miniscript and focus on a selected subset to illustrate its relevance to Trace-Net. The $script(m)$ column of Table 1 includes the $Script$ fragments required to parse the raw Bitcoin $Script$ from Example 3.1 into the following Miniscript expression:

Informally, the Miniscript term $andor(m_x, m_y, m_z)$ implies satisfaction expressed as $(m_{x} \wedge m_{y}) \vee m_z$. The Miniscript term $and_v(m_x, m_y)$ requires the satisfaction of both subterms ($m_{x} \wedge m_{y}$). Miniscript distinguishes between satisfying and dissatisfying symbolic witnesses for a given Miniscript term $m$: a dissatisfying symbolic witness provides an input to a $Script$ fragment which executes without a run-time error but does not satisfy its specific execution path. A dissatisfying witness of a Miniscript term is required for the composition of Miniscript parent terms, where the satisfaction or dissatisfaction of a child term may be required for the satisfaction of the parent term. Importantly, however, the satisfying witnesses of the parent Miniscript term can be expressed in terms of the (dis)satisfying witnesses of its child terms, as shown in Table 1.

We now illustrate how to construct symbolic witnesses for our HTLC Miniscript (Equation 2) with Miniscript semantics shown in Table 1. (Dis)satisfying symoblic witnesses for terminal Miniscript subexpressions such as $pk_{A,B}$, $sha256(b_{32})$ and $older(10)$ are derived first:

At the next expression level, we derive the satisfying symbolic witnesses of $v(pk_B)$ and subsequently $and_{v}(v(pk_{B}), older(10)$ by concatenation of the symbolic witnesses of the child terms according to the $(d)sat(m)$ columns of Table 1.

Finally, we can infer the symbolic witnesses $\Gamma_{0}$ and $\Gamma_{1}$ of the top-level $andor$ Minsicript expression representing our HTLC script.

We also note that Miniscript terms are typed and feature type modifier properties, which capture the stack manipulation behavior of the underlying $Script$ fragments, to ensure correct composition of terms: the Miniscript type $B$ is called a base expression, as it pushes a non-zero stack element to the stack upon satisfaction. A $V$ type, in contrast, does not add a stack element upon satisfaction, which can be nonetheless useful as a conditional expression in a parent Miniscript term. Further details about the type and properties of Miniscript are defined in [21].

Example 3.2 (Atomic Swap Contract with Miniscript): We introduce a contract protocol called an atomic swap for which we will step-wise instantiate the Trace-Net model for illustration purposes. The atomic swap protocol is intended for two actors to exchange ownership of Bitcoin outputs. It features HTLC scripts previously introduced in Example 3.1.

A possible implementation of an atomic swap is shown in Figure 2. Its execution resembles a commit-protocol between the two actors: first, Alice commits her coin to the contract. If Bob responds in like, the coin swap can take place. If Bob does not respond, Alice can withdraw her funds after the expiration of a time-out. In our example implementation, each funding contract transaction features a single output with an HTLC. Both HTLC’s feature an identical hash-lock, which functions as a proof of publication.2 In Miniscript terms, these two output scripts are expressed as follows:

For both scripts, let us denote the script execution path featuring the hashlocks as the swap paths, because they finalize the swap between participating actors. These output paths featuring $pk_A$ or $pk_B$ are controlled by actors A and B respectively, and the private keys for signing remain secret. Swap paths are coupled by the shared hash-lock with a $b_{32}$ secret pre-image generated by a the initiating actor A. Subsequent paragraphs demonstrate how the hash-lock can provide a verifiable publication proof for the swap transaction of the initiating actor. This is required to ensure either both or none of the swap paths are executed.

Contract Security

Should the initiating actor A attempt to obtain its swapped funds after both actors have committed funds, the pre-image of this hash-lock will be revealed to actor B upon its broadcast to the Bitcoin network, as a witness element of the swap transaction. Having observed the hash-lock preimage, actor B can now proceed to redeem its swap transaction, thereby completing the contract. The hash-lock therefore functions as a proof-of-publication, which performs the "atomic" coupling between the two swap transactions. Omitting the distinction between transaction broadcasts and confirmations, a successful atomic swap initiated by Alice has the following execution trace:

Should the Alice become unresponsive after $\xrightarrow{tx_{fund,A}} \xrightarrow{tx_{fund,B}}$, actor B can wait until the time-lock on its funding transaction output expires, releasing returning actor B’s committed funds. Subsequently, with an additional delay, actor A too can regain ownership of its original funds in this abort scenario.

Note however, that unsafe contract execution traces are possible with this implementation. Consider the following trace, for example:

If Bob funds the contract first, its funds can be swept by actor Alice who generated the secret pre-image and can execute the swap path of $HTLC_{B}$. Another subtle contract aspect are the delays ($\Delta T_{A}$, $\Delta T_{B}$) imposed on abort transactions $tx_{abort, A}$, $tx_{abort, B}$. For a swap initiated by Alice, who generates the secret pre-image, setting $\Delta T_{A} = \Delta T_{B}$ will enable the following contract execution trace:

This trace results in actor A obtaining ownership of both utxo’s after executing both $tx_{swap,\:A}$ and $tx_{abort,\:A}$, which is clearly not the intent of the contract design. This unsafe contract outcome is possible, since the time-locks can release simultaneously, enabling race conditions between swap and abort paths: $tx_{swap,A}$/$tx_{abort, B}$ and $tx_{swap,B}$/ $tx_{abort, A}$. In the trace above, we assume the adversary will confirm its transactions first and therefore win both races. A safe contract must therefore be safe despite the possibility of competing transactions. We can solve this by ensuring that $\Delta T_{A} > \Delta T_{B}$ for a swap contract initiated by Alice, who generates the secret hash pre-image and must confirm a funding transaction first.

Having now considered several trace examples including some which represent unintended contract executions, we proceed to formalize transaction confirmation semantics, which describe how transactions are appended to the blockchain in the Trace-Net model.

3.3 Transaction Confirmation Semantics

Transaction fees

Trace-Net neglects transaction fees, and assumes that these can be sufficiently adjusted without resigning after a transaction is broadcast according to client implementation logics to ensure a transaction is appended to the blockchain within a fixed duration.

Transaction confirmation delays

We differentiate between transactions broadcast by the verifying actor and all other, potentially adversarial external actors. The finite confirmation delays for the verifying internal and external actors can be parameterized independently during contract verification (Section 5) to accurately reflect contract deployment environments.

Adversarial Blockchain Reorganization

Given that smaller blockchains are often secured by minimal proof-of-work [12] [13], the cost of performing a 51% attack and reorganizing the blockchain can be low enough for attackers to pursue. A reorganization allows the attacker to selectively replace and inject transactions in the new chain branch and re-execute the ongoing contract to its advantage. Trace-Net models an adversarial blockchain reorganization at each contract state, to ensure a smart contract safety property will hold despite bounded reorganizations by an adversary (Section 5).

4. Trace-Net: A Symbolic Model of Contracts

Having covered the symbolic execution of Bitcoin transactions, we can now proceed to detail how Trace-Net provides a symbolic model of the entire contract execution. In addition to symbolic analysis of individual output scripts, we must provide a stateful contract model which captures both actor knowledge and blockchain state relevant to the contract. This symbolic contract model must be executable, featuring direct messages exchanges, and on-chain events. We provide an overview of the symbolic Trace-Net Model before defining state transition semantics in subsequent subsections.

Internal & External Actors

In our model of Bitcoin contract protocols, each verifying actor will assume that all other counter-parties are colluding against the verifying actor. We can thereby simplify each contracting protocol as one between two actors: the internal, verifying actor and the adversarial, external actor. This implies that direct contract protocol messaging can be modelled as single bi-directional communication channel between these two actors, with no additional relevant intruders.

Actor Knowledge

We model the actor knowledge states as $K_{int},K_{ext}$, consisting of symbolic knowledge objects such as transaction templates and secrets. Actors always expand their knowledge when it is updated with a direct message from the counter-party or an observation on the blockchain. Knowledge expansion is performed with a set of public functions $\Sigma$ available to all actors, modeling Dolev-Yao deductive abilities of an actor during contract protocol execution (Section 4.1).

Setup phase

Each contract protocol implementation begins with the generation of the contract transaction templates during the setup phase. Transaction templates have fully defined attributes, but feature empty witnesses, and can therefore not be broadcast. We denote a transaction template as $tx^{\prime}$ and a completed, valid contract transaction with valid witnesses as $tx$. Informally, the setup phase corresponds to the $stipulation$ of the contract for the participating actors. The setup involves no exchanges of signatures or generated secrets. We express the generation of the contract transaction templates as a implementation-defined function $\textsf{GenTx}$, which, on an input of public keys $PK^{*}$, hash digests $B^{*}$ and funding output sets $outs_f^{*}$, will output a set of contract transaction templates $TX^{\prime}$. These required inputs to $\textsf{GenTx}$ are defined by the contract implementation, but require at least one public key and one funding output in total.

Inputs to and output of $\textsf{GenTx}$ are known by both internal and external actors at the end of the setup phase. Actors have access to the following public functions in $\Sigma_{setup}$ during the setup phase:

The function $\textsf{Gen}$ is a from a Bitcoin supported signature scheme $\Xi = (\textsf{Gen}, \textsf{Sign}, \textsf{Vrfy})$, $\textsf{PK}$ the public key derivation function and $\textsf{Hash}$ a hash function supported by Bitcoin script. For simplicity, actors call Gen to generate both private key or hash pre-image secrets required for the public key and hash inputs of GenTx. These secrets are added to the actors knowledge during the setup phase: once this is complete, Trace-Net can be instantiated to symbolically execute the contract and generate the reachable state-space for safety verification.

Symbolic execution phase

Trace-Net models a symbolic contract state with the tuple $(K_{int}, K_{ext}, B)$, where $K$ is the state of an actor’s knowledge and $B$ the on-chain state of the contract Bitcoin transactions. In each protocol state during the execution phase, the following transaction types can be fired by the actors if the transitions are in a fireable state.

• $\textit{e}$ - Message exchange

• $\textit{tb}$ - Transaction broadcast

• $\textit{t}$ - On-chain confirmation

• $\textit{d}$ - Time delay

• $\textit{r}$ - Blockchain reorganization

We provide an initial introduction to the transition types and formally define both transition firing semantics in later sections. For actor $a,b \in \{int,ext\}$:

$(K_a,K_b,B) \xrightarrow{e^{a}} (K_a,K_b^{\prime},B)$: A message exchange transition is a direct message between internal and external actors, where the knowledge of recipient is updated with the message object. A message exchange transition only updates the knowledge state of the receiving actor (Definition 4.2, Definition 4.3).

$(K_a,K_b,B) \xrightarrow{tb^{a}} (K_a,K_b^{\prime},B)$: When an actor intends to add a valid transaction to the Bitcoin blockchain, the transaction must first be broadcast to the Bitcoin peer-to-peer network with a transaction broadcast transition, fired by an actor who can produce the transaction from knowledge. A broadcast is only modeled in Trace-Net if it results in an update of the counterparty’s knowledge (Definition 4.4, Definition 4.5).

$(K_a,K_b,B) \xrightarrow{t^{a}} (K_a,K_b,B^{\prime})$: An on-chain transaction can only be confirmed or amended to the blockchain if it has previously been broadcast or is already fully known by the counterparty. An on-chain transition only updates the on-chain contract state, and can be preceded by a time delay to model the required confirmation time (Definition 4.12, Definition 4.13).

$(K_a,K_b,B) \xrightarrow{d} (K_a,K_b,B^{\prime})$: A time delay interval is expressed in a number amended blocks and like an on-chain transition only affects the on-chain state $B$ (Definition 4.10).

$(K_{int},K_{ext},B) \xrightarrow{r^{ext}(n)} (K_{int}/K_{int}^{\prime},K_{ext},B^{\prime})$: A blockchain reorganization of depth $n$ is fireable by the external actor at any contract state. Since the external actor can freely determine the reorganization depth and transaction ordering of the new chain branch, different reorganizations up to a maximum depth are possible at a given state (Definition 4.14, Section 5).

Actor Strategies

We refer to the set of fire-able transitions of an actor as its strategies in contract state $(K_{int}, K_{ext}, B)$.

4.1 Actor Knowledge Derivation

Actor knowledge is modeled in a Dolev-Yao-fashion [16], where each actor can access a set of public function to deduce additional information during the symbolic execution of the underlying contract implementation.

Definition 4.1 (Actor Knowledge): An actor knowledge $K$ is a finite set of transaction templates, private keys, public keys, hash pre-images and signatures. $K$ can be expanded with a set of public functions $\Sigma_{exec}$ during symbolic contract execution whenever $K$ is updated with external information.

Let $k$ be a knowledge object which is derived from $K$ with a function in $\Sigma_{exec}$. We denote the knowledge expansion of $K$ with $k$ with the following notation.

The public functions $\Sigma_{exec}$ allow actors to derive sweep transaction templates from outputs and transaction signatures from private keys.

• $\textsf{SweepTx}(out)$ is a function that generates a symbolic sweep transaction template spending $out$, which features an execution path controlled (Definition 3.3) by a single actor $a \in \{int, ext\}$. This sweep transaction sends the funds to single output owned by actor $a$.

  $$\begin{split} K_{int} \vdash \{ & tx^{\prime}_{swap, int}, tx^{\prime}_{abort, int}, tx^{\prime}_{sweep, int}, \\ & tx^{\prime}_{swap, ext}, tx^{\prime}_{abort, ext}, tx^{\prime}_{sweep, ext}, \\ & sig_{pk_{int}}(tx^{\prime}_{fund, int}), \;sig_{pk_{int}}(tx^{\prime}_{swap, int}), \\ & sig_{pk_{int}}(tx^{\prime}_{abort, in}),sig_{pk_{int}}(tx^{\prime}_{sweep, int}) \} \end{split}$$

  Where $ctrl(out,actor)$ denotes that $out$ features an execution path controlled by $actor$. $K \vdash out$ if the output is a member of any transaction template in the knowledge of actor $actor$.

• $\textsf{Sign}(tx^{\prime},inv(pk))$ is a function that on input transaction template $tx^{\prime}$ and secret key $inv(pk)$ outputs a signature $sig_{pk}(tx^{\prime})$. This signature satisfies the constraint $[sig \; w \; pk]$ as $w$.

  $$\begin{split} K_{int} \vdash \{ & tx^{\prime}_{swap, int}, tx^{\prime}_{abort, int}, tx^{\prime}_{sweep, int}, \\ & tx^{\prime}_{swap, ext}, tx^{\prime}_{abort, ext}, tx^{\prime}_{sweep, ext}, \\ & sig_{pk_{int}}(tx^{\prime}_{fund, int}), \;sig_{pk_{int}}(tx^{\prime}_{swap, int}), \\ & sig_{pk_{int}}(tx^{\prime}_{abort, in}),sig_{pk_{int}}(tx^{\prime}_{sweep, int}) \} \end{split}$$

  This derivation rule is applicable to all public keys featured in the symbolic witnesses of transaction template inputs ($pk$ in $\textsf{sat}(tx^{\prime}.ins)$).

Bounded knowledge expansion with $\Sigma_{exec}$ implies a finite contract execution state-space. Inputs and outputs of public functions SweepTx and Sign are typed, such that derived knowledge cannot be used as an inputs to $\Sigma_{exec}$. SweepTx consumes controlled outputs and produces owned outputs. Likewise, signatures generated from the public Sign function cannot be used as inputs for $\Sigma_{exec}$.

Example 4.1 (Initial Knowledge Expansion): In the following example, we illustrate how the actor knowledge is expanded at the beginning of the symbolic execution phase of an atomic swap contract.

For our atomic swap example initiated by the internal actor, the initial knowledge $K^{int}$ of internal actor after the setup phase executed by the contract implementation is initialized as follows. Note that we do not explicitly list the funding outputs, as these are already referenced as $in.prevout$ attributes in the funding transactions, which the actor can extract. For simplicity, we assume that actors reuse private keys for all outputs.

Subsequently, since $tx^{\prime}_{fund, int}$ and $tx^{\prime}_{fund, ext}$ contain the funding outputs as well as swap and abort output execution paths which are all controlled by single actors, we can expand the internal actor’s knowledge with sweep transactions (SweepTx) for all these output execution paths. These sweep transactions (sweep, swap, abort) are depicted in Figure 4.

The internal actor furthermore can derive signatures which are required to satisfy the the symbolic witnesses featuring public key $pk_{int}$ with Sign. The knowledge of the internal actor has now been fully expanded in the initial state of the symbolic contract execution.

4.1.1 Cryptographic Extensions

It is possible to extend $\Sigma_{setup}$ (Equation 3) and $\Sigma_{exec}$ (Equation 4) to model additional cryptographic sub-protocols useful for the construction of contracts. We demonstrate such an extension with the adaptor signature scheme, previously formalized in [11]. An adaptor signature scheme consists of $\Xi_{adapt} = (\textsf{pSign},\:\textsf{pVrfy},\:\textsf{Adapt},\:\textsf{Ext})$ for a signature scheme $\Xi_{sig} = (\textsf{Gen},\:\textsf{Sign},\:\textsf{Vrfy})$.

• $\textsf{pSign}(tx^{\prime},\textsf{inv}(pk),pk_y)$ is a function that on input a message $tx^{\prime}$, private key $inv(pk)$ and public key $pk_y$ outputs a pre-signature $psig_{pk}(tx^{\prime},pk_y).$

• $\textsf{pVrfy}(psig_{pk}(tx^{\prime},pk_y),tx^{\prime},pk,pk_y)$ is a function that verifies a pre-signature against a message $tx^{\prime}$ and public keys $pk$ and $pk_y$.

• $\textsf{Adapt}(psig_{pk}(tx^{\prime},pk_y),inv(pk_y)$ is a function that on input a pre-signature $psig_{pk}(tx^{\prime},pk_y)$ and a private key $inv(pk_y)$ returns a signature $sig_{pk}(tx^{\prime})$.

• $\textsf{Ext}(psig_{pk}(tx^{\prime},pk_y), sig_{pk}(tx^{\prime}),pk_y$) is a function that on input a pre-signature, corresponding signature and public key $pk_y$ returns the a private key $inv(pk_y)$.

Given pre-signature $psig_{pk}(tx^{\prime},pk_y)$, an observer can extract $inv(pk_y)$ upon learning $sig_{pk}(tx^{\prime})$ with the function $\textsf{Ext}$. Conversely, given $psig_{pk}(tx^{\prime},pk_y)$ and $inv(pk_y)$, a valid signature $sig_{pk}(tx^{\prime})$ can be inferred.

Example 4.2 (Atomic Swap with Adaptor Signatures): In the following example, our atomic swap contract has the hash-lock in the swap spending paths replaced with pre-signatures from $\Xi_{adapt}$. The pre-signatures are known by both actors but not observable on-chain.

We adapt the output scripts for atomic swap transactions from Example 3.2 and replace the hash-lock in the swap spending condition with a public key of the counterparty. Expressed in Miniscript, the HTLC output scripts of $tx_{fund, in}$ and $tx_{fund,ex}$ for our atomic swap contract initiated by the internal actor are the following:

With the hash-lock removed, there are no on-chain transaction semantics which reveal a coupling between the swap paths of the two contract participants. Instead, this coupling is setup during the user-defined setup protocol with an exchange of pre-signatures between the actors.

Setup Phase: The user-defined setup phase now features an extended public function set.

Note that GenTx must also generate swap transactions for both actors, so that both actors can generate and verify pre-signatures for swap transactions $tx_{swap,int}^{\prime}, tx_{swap,ext}^{\prime}$ of the counter-party. $inv(pk_y)$ is generated by the initiating, internal actor and so $inv(pk_y)\notin K_{ext}$ at setup. Once these pre-signatures are validated, the setup protocol is complete. When compared to the previously illustrated atomic swap contract with hash-locks, the actor knowledge after contract setup are extended by pre-signatures and related public keypairs ($inv(pk_y)$, $pk_y$).

The set of public functions available to actors $\Sigma_{exec}$ during symbolic contract execution is extended with $\textsf{Adapt},\textsf{Ext} \in \Xi_{adapt}$.

We only illustrate the contract state during symbolic execution when both funding transactions are confirmed and no direct messages have been exchanged yet. The initiating internal actor wishes to execute its swap transaction: the spending conditions for the swap path of output script $m_{ext}$ require $sig_{pk_{int}}(tx^{\prime}_{swap, int})$ and $sig_{pk_{ext}}(tx^{\prime}_{swap, int})$, the latter which is derived with the Adapt function.

Once $tx_{swap,int}$ is executed, the external actor can observe $sig_{pk_int}(tx^{\prime}_{swap, int})$ (publication proof), and derive $inv(pk_y)$ with the Ext function.

The external actor can expand its knowledge with adapt, the pre-signature and publication proof to obtain $sig_{pk_{ext}}(tx^{\prime}_{swap,ext},pk_y)$. This signature enables the external actor to also execute its swap transaction, thereby completing the contract.

Note that without the shared hash-lock, the atomic swap scheme with adaptor signature does not reveal any contract coupling between swap transactions on the Bitcoin blockchain: the atomic coin swap contract is now no longer visible to the observer of the Bitcoin network.

4.1.2 Messages & Transaction Broadcasts

In addition to deducing information from existing knowledge with public functions, actors can directly exchange messages to update the knowledge of the recipient. Furthermore, a transaction broadcast by an actor which includes information previously unknown to the counter-party also results in the knowledge update of the observer.

Definition 4.2 (Fire-able Message Transition): A message transition $e^{a}(k)$ with payload $k$ is fire-able by an actor $a \in \{int,ext\}$ with knowledge $K_a$, if $k$ is known by the sender but unknown to the recipient.

Definition 4.3 (Message Transition Firing): Let $e^{a}(k)$ be a transition for actor knowledges $(K_a,K_b)$, fire-able by actor $a \in \{int,ext\}$. The firing of of $e^{a}(k)$ updates actor knowledge $(K_a,K_b)$ to $(K_a, K_{b}\cup \{k\})$

An actor knowledge can also be expanded with knowledge observed on the blockchain. Specifically, an actor will expand its knowledge when the counter-party broadcasts a transaction on the network and the transaction includes previously unknown input witness elements such as signatures or hash pre-images.

A transaction broadcast is only fireable during the symbolic execution of a contract if it leads to a knowledge update of the observing actor. In order for an actor to fire a broadcast transition, it must be deducible by the initiating actor, be consensus valid according to a blockchain model B, and provide new information to the counterparty. A complete, valid transaction can be deduced by an actor if can produce a valid witness for each of its inputs: a valid witness stack for an input must satisfy at least one of the symbolic witnesses $\{\Gamma_0,\Gamma_1,...\}=sat(in)$. The deduction rule for an actor to derive a valid transaction is shown below:

The actor must know the transaction template, and be able to generate a valid witness $w$ for each transaction template.

Definition 4.4 (Fire-able Transaction Broadcast): A transaction broadcast $tb$ for a transaction is fire-able if it is deducible by actor $a \in \{int,ext\}$, is valid in blockchain state B and contains witness stack elements unknown to actor b.

Definition 4.5 (Transaction Broadcast Firing): The firing of a transaction broadcast leads to an update of the observing actors knowledge if it contains witness elements previously unknown to the observer.

Witness elements of the broadcast transaction $tx$ are denoted as $w_{i} \in tb^{a}.ins$ in the firing rule shown above.

4.2 Trace-Net Blockchain Model

The Trace-Net blockchain model captures the on-chain state of contract transactions. To this end, Trace-Net adopts a classic Petri Net skeleton to capture the state and fire-ability of on-chain transitions based on the availability of unspent outputs, and the current height of the Bitcoin blockchain.

There are four classical Petri-Net elements [49] adopted by the Trace-Net: places, tokens, arcs, and on-chain transitions, as shown in Figure 3. Tokens can only exist in places. Each on-chain transition is connected to at least one place with directed arcs. Arcs pointing from a place to an on-chain transition reflect transaction inputs and are denoted input arcs $(p,t)$. Arcs pointing to places represent transaction outputs and are denoted output arcs $(t,p)$. A given place $p$ can only connect to a single input and single output arc at most and represents a transaction output.

When an on-chain transition fires, the input arcs of the fired transition each consume a token from their connected place. Simultaneously, each transition output arc will produce a token to its connected place during firing, modeling the consumption and production of unspent transaction outputs on the blockchain during the execution of the contract protocol. The place marking function $m(p) \in \{0,1\}$ returns the number of tokens currently in a place $p$. We extend the Petri Net formalism with time markings and earliest firing time intervals to arrive at the definition of a Trace-Net.

Definition 4.6 (Trace-Net): A Trace-Net $\mathcal{Z}$ is the tuple $(K^{int}_0, K^{ext}_0,P,T,F, I_{older},I_{after},m_0,b_{0})$ such that

1. $K^{int}_0, K^{ext}_0$ is the initial actor knowledge.

2. There exists a $p(out) \in P$ for each $out \in K^{in}_0/K^{ex}_0$.

3. F is a relation $F\subseteq(P \times T) \cup (T \times P)$.

4. For all $tx \in K^{int/ext}_0$:

   1. There exists a unique $t \in T$ for each $\pi_i$ of $\pi(tx)$.

   2. For each $tx$ and $in \in tx$, $(p(in.prevout),t)\in F$.

   3. For each $tx$ and $out \in tx$, $(t,p(out)) \in F$.

5. $I_{after}, I_{older}:(P \times T) \rightarrow \mathbb{N}^0$

   1. $I_{after}(p,t)$, $I_{older}(p,t) \models t.\pi_i$ for $t \in T$

6. $m_0$ : $P \rightarrow \{0,1\}$ is the initial marking.

7. $b_0 \in \mathbb{N}$ is the initial blockheight.

(2) A place is added to $\mathcal{Z}$ for each output featured in the contract transaction templates present in the initial actor knowledge states. This includes outputs referenced by transaction templates (funding outputs) and symbolic sweep transactions. (3) F a relation representing input and output arcs. (4) Trace-Net models a dedicated transition for each symbolic witness permutation (Definition 3.4) of a transaction: this enables the fireability of each symbolic witness permutation to be modeled separately. (5) Earliest firing intervals is a function over input arcs and must satisfy the symbolic witness permutation associated with its transition. The firing intervals are implied by the $after$ and $older$ constraints expressed in the respective symbolic witness.

Let us denote $t^{-}$ as the required token availability for $t$ over all places $P$ in Trace-Net $\mathcal{Z}$ in order for $t$ to be fireable. This is illustrated in Figure 3.