Skip to main content

Bitcoin Trace-Net: Formal Contract Verification at Signing Time

Published onOct 22, 2021
Bitcoin Trace-Net: Formal Contract Verification at Signing Time
·

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.id,tx.ins,tx.outs,tx.after)(tx.\textsf{id}, tx.\vec{\textsf{ins}}, tx.\vec{\textsf{outs}}, tx.\textsf{after}), where ins\vec{\textsf{ins}} and outs\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.idtx.\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.aftertx.\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.prevout,in.older,in.witness)(in.\textsf{prevout}, in.\textsf{older}, in.\textsf{witness}). The in.prevoutin.\textsf{prevout} attribute uniquely references the redeemed output in an output vector of a previously confirmed transaction with a (txid,index)(txid,index) pair. The in.olderin.\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.

Figure 1: Transaction C (TXIDC) spends outputs at indices 1 & 0 from transactions A & B respectively. Transaction C is time-locked until blockheight 50 since it is limited by the older time-lock of input 1: note that the older time-lock of input 0 in transaction C releases earlier at blockheight of 48.

An output is described with the attribute tuple (out.value,out.script)(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 feefee 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.scriptin.prevout.script) and input witness (in.witnessin.witness) pair are shown below. Note that the witness is copied element-by-element (w0,w1,...,wm{w_0, w_1, ..., w_m}) into an in-memory execution stack (stackinitstack_{init}) before the script validation run is performed.

The script is executed opcode-by-opcode beginning with its first operator OP0OP_0 and stackinitstack_{init} until OPnOP_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 OPnOP_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 AA 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 CC encodes an after time-lock of two blocks, which requires transaction AA to be at least two blocks old when transaction CC is broadcast: this time-lock releases at the blockheight 46+2=4846 + 2 = 48, since transaction AA was amended in block 4646.

The earliest firing time of a transaction occurs when all after and older time-locks have released. The After time-lock of transaction CC 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 CC 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 γ=γ0...γn\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 ww and a symbolic witness Γ\Gamma holds true if the witness satisfies the constraints imposed by the symbolic witness.

wΓw \models \Gamma

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

sat(output)=Γˉ={Γ0,...,Γn}sat(output) = \bar\Gamma = \{\Gamma_0,..., \Gamma_n\}

For simplicity, we denote sat(in)sat(in) to mean sat(in.prevout)sat(in.prevout), which returns the symbolic witnesses of the output being spent by inin. 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 (w0,w1,...,wn)(w_0, w_1, ..., w_n) in terms of constraints imposed on each of its elements. The following set CC of constraint expressions consists of symbolic witness stack elements wjw_{j}, constant byte strings bb, constant integers ii, relational operators and functional expressions such as signature, hash and size:

exp::=expexp    sig  wj  pk    hash  wj=b32    size  wj=i  wj=b    after>=i    older>=i\begin{split} exp \: ::= \: & exp \wedge exp \;| \; \textrm{sig} \; w_{j} \; pk \; | \; \textrm{hash} \; w_{j} = b_{32} \; | \; size \; w_{j} = i \; | \\ & w_{j} = b \; | \; after \: >= i \; | \; older \: >= i \end{split}(1)

The symbolic expression sigw0pkAsig \: w_{0} \: pk_{A}, for example, constrains the first witness stack element (w0w_{0}) to be a valid signature of the transaction signed by the private key inv(pkA)inv(pk_{A}). The expression hashw1=b32hash \: w_{1} = b_{32} constrains the second witness stack element to be the hash pre-image of a 32-byte constant b32b_{32}: here, hashhash represents a specific hash function supported by the Bitcoin script language which produces a 32-byte digest. The time-lock constraint older>=iolder>=i in CC constrains the value of the in.olderin.\textsf{older} attribute and not the witness element directly.1 The after>=iafter>=i time-lock constraint is imposed on the spending transactions tx.aftertx.\textsf{after} attribute. Example 3.2 illustrates a symbolic witness composed of symbolic expressions from CC for a hash time-lock contract. Our simplified set of constraint expressions can only express symbolic execution of a subset of Bitcoin ScriptScript, 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 Γsat(output)\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 (Γˉi>1).(|\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 (in0in_0, in1in_1,...), each with a possible set of symbolic witnesses sat(ini)=Γˉi={Γ0,i,Γ1,i,...}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 πi\pi_i for a transaction txtx is a unique combination of symbolic witnesses for each tx input. Notation: π(tx)={π0,π1,...}\pi(tx)=\{\pi_0, \pi_1, ...\} denotes all possible symbolic witness permutations for a given transaction txtx.

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 ScriptScript example has two different spending conditions γ0γ1\gamma_{0} \vee \gamma_{1}, where γ0\gamma_{0} is encumbered with a hash-lock and public key pkApk_A and γ1\gamma_{1} is encumbered with a delay of 10 blocks and the public key pkBpk_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 γ0\gamma_{0} requires a transaction signature created with the private key inv(pkA)inv(pk_{A}) (line 1) and the sha256sha256 preimage to the digest b32b_{32} (Lines 6, 7). Alternative execution path γ1\gamma_{1} can be spent with a transaction signature with the private inv(pkB)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 Γ0\Gamma_{0} and Γ1\Gamma_{1} for γ0\gamma_{0} and γ1\gamma_{1} of this HTLC are expressed below with constraint Expressions (1) from CC as follows:

The symbolic witnesses provide the necessary information for an actor to determine whether it can deduce a valid witness for a Bitcoin ScriptScript from its knowledge. For example, an actor with the knowledge of inv(pkA)inv(pk_{A}), the sha256 preimage of b32,b_{32}, and the symbolic witness Γ0,\Gamma_{0}, will be able to produce a two element witness stack which satisfies Γ0\Gamma_{0} (or the execution path γ0\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 ScriptScript 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 ScriptScript.

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 MM each express a unique ScriptScript template, consisting of one or more ScriptScript 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)script(m) of each Miniscript term mm are captured by type(m)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)script(m) column of Table 1 includes the ScriptScript fragments required to parse the raw Bitcoin ScriptScript from Example 3.1 into the following Miniscript expression:

andor(pkA,sha256(b32),andv(v(pkB),older(10)))\begin{split} andor(& \\ & pk_{A}, \\ & sha256(b_{32}), \\ & and_{v}(v(pk_{B}),older(10))\\ & ) \\ \end{split}(2)

Informally, the Miniscript term andor(mx,my,mz)andor(m_x, m_y, m_z) implies satisfaction expressed as (mxmy)mz(m_{x} \wedge m_{y}) \vee m_z. The Miniscript term andv(mx,my)and_v(m_x, m_y) requires the satisfaction of both subterms (mxmym_{x} \wedge m_{y}). Miniscript distinguishes between satisfying and dissatisfying symbolic witnesses for a given Miniscript term mm: a dissatisfying symbolic witness provides an input to a ScriptScript 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.

Table 1: An overview of selected Miniscript terms required to express the HTLC script template from Example 3.1. Columns sat(m) and dsat(m) denote satisfying and dissatisfying symbolic witnesses for the respective Miniscript term m, whereas script(m) and type(m) denote the underlying Bitcoin Script and Miniscript type respectively. Miniscript terms are composed as follows: andor(mx,my,mz)(m_x,m_y,m_z) contains child terms mx,mym_x,m_y and mzm_z . The parent andor term can be satisfied by composing both satisfying and dissatisfying symoblic witnesses of its child terms.

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 pkA,Bpk_{A,B}, sha256(b32)sha256(b_{32}) and older(10)older(10) are derived first:

sat(pkA,B)=[sig  w0  pkA,B]dsat(pkA,B)=[w0=0]sat(sha256(b32))=[sha256  w0=b32]sat(older(10))=[older>=i]\begin{split} sat(pk_{A,B}) &= [sig \; w_{0} \; pk_{A,B}] \\ dsat(pk_{A,B}) &= [w_{0} = 0] \\ sat(sha256(b_{32})) &= [sha256 \; w_{0} = b_{32}] \\ sat(older(10)) &= [older >= i] \end{split}

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

sat(v(pkB))=sat(pkB)=[sig  X0  pkA,B]sat(andv(v(pkB),older(10))=sat(older(10))+sat(v(pkB))=[sig  w0  pkB,  older>=10]\begin{split} sat(v(pk_{B})) &= sat(pk_{B}) = [sig \; X_{0} \; pk_{A,B}] \\ sat(and_{v}(v(pk_{B}), older(10)) &= sat(older(10))+sat(v(pk_{B})) \\ &= [sig \; w_{0} \; pk_{B}, \; older >= 10] \end{split}

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

sat(andor(pkA,sha256(b32),  andv(v(pkB),older(10)))=sat(sha256(b32))+sat(pkA)  sat(andv(v(pkB),older(10)))+dsat(pkA)=[sha256  w0=b32,  sig  w1  pkA]  [sig  w0  pkB,  w1=  0,  after>=10]  =Γ0    Γ1\begin{split} sat(andor(pk_{A},\:sha256(b_{32}&),\;and_{v}(v(pk_{B}),\:older(10))) \\ = sat(sha256(b_{32}&))+sat(pk_{A}) \; \vee \\ sat(and_{v}(v(pk_{B}),\:old&er(10)))+dsat(pk_{A}) \\ = [sha256 \; w_{0} = b&_{32}, \; sig \; w_{1} \; pk_{A}] \; \vee \\ [sig \; w_{0} \;pk_{B}, \; w_{1} =& \; 0, \; after >= 10] \; \\ = \Gamma_{0} \; &\vee \; \Gamma_{1} \end{split}

We also note that Miniscript terms are typed and feature type modifier properties, which capture the stack manipulation behavior of the underlying ScriptScript fragments, to ensure correct composition of terms: the Miniscript type BB is called a base expression, as it pushes a non-zero stack element to the stack upon satisfaction. A VV 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].

Figure 2: A set of contract transactions are shown which stipulate an atomic swap contract between participants A and B. Both transaction outputs feature alternative γswap and γabort execution paths, whilst the identical hash-locks and staggered time-locks enforce the exclusive execution of either swap or abort paths for both parties.

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:

HTLCA=andor(pkB,sha256(b32),andv(v(pkA),older(15)))\begin{split} HTLC_A=andor(&pk_{B}, sha256(b_{32}), \\ & and_{v}(v(pk_{A}),older(15))) \\ \end{split}

HTLCB=andor(pkA,sha256(b32),andv(v(pkB),older(10)))\begin{split} HTLC_B=andor(& pk_{A}, sha256(b_{32}), \\ & and_{v}(v(pk_{B}),older(10))) \\ \end{split}

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 pkApk_A or pkBpk_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 b32b_{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:

txfund,Atxfund,Btxswap,Atxswap,B\xrightarrow{tx_{fund,A}} \xrightarrow{tx_{fund,B}} \xrightarrow{tx_{swap,A}} \xrightarrow{tx_{swap,B}} \circ

Should the Alice become unresponsive after txfund,Atxfund,B\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.

txfund,Atxfund,Bd10txabort,Bd5txabort,A\xrightarrow{tx_{fund,A}} \xrightarrow{tx_{fund,B}} \xrightarrow{d_{10}} \xrightarrow{tx_{abort,B}} \xrightarrow{d_{5}} \xrightarrow{tx_{abort,A}} \circ

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

txfund,Btxswap,A\xrightarrow{tx_{fund,B}} \xrightarrow{tx_{swap,A}} \circ

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 HTLCBHTLC_{B}. Another subtle contract aspect are the delays (ΔTA\Delta T_{A}, ΔTB\Delta T_{B}) imposed on abort transactions txabort,Atx_{abort, A}, txabort,Btx_{abort, B}. For a swap initiated by Alice, who generates the secret pre-image, setting ΔTA=ΔTB\Delta T_{A} = \Delta T_{B} will enable the following contract execution trace:

txfund,Atxfund,Bd(ΔTA/B)txabort,Atxswap,A\xrightarrow{tx_{fund,A}} \xrightarrow{tx_{fund,B}} \xrightarrow{d(\Delta T_{A/B})} \xrightarrow{tx_{abort,A}} \xrightarrow{tx_{swap,A}} \circ

This trace results in actor A obtaining ownership of both utxo’s after executing both txswap,Atx_{swap,\:A} and txabort,Atx_{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: txswap,Atx_{swap,A}/txabort,Btx_{abort, B} and txswap,Btx_{swap,B}/ txabort,Atx_{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 ΔTA>ΔTB\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 Kint,KextK_{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 txtx^{\prime} and a completed, valid contract transaction with valid witnesses as txtx. Informally, the setup phase corresponds to the stipulationstipulation 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 GenTx\textsf{GenTx}, which, on an input of public keys PKPK^{*}, hash digests BB^{*} and funding output sets outsfouts_f^{*}, will output a set of contract transaction templates TXTX^{\prime}. These required inputs to GenTx\textsf{GenTx} are defined by the contract implementation, but require at least one public key and one funding output in total.

GenTx(PKint,PKext,Bint,Bext,outsfint,outsfext)=TX\textsf{GenTx}(PK^{int},PK^{ext}, B^{int}, B^{ext}, outs_f^{int}, outs_f^{ext}) = TX^{\prime}

Inputs to and output of GenTx\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 Σsetup\Sigma_{setup} during the setup phase:

Σsetup=(Gen,PK,Hash,GenTx)\Sigma_{setup}=(\textsf{Gen},\:\textsf{PK},\:\textsf{Hash},\:\textsf{GenTx})(3)

The function Gen\textsf{Gen} is a from a Bitcoin supported signature scheme Ξ=(Gen,Sign,Vrfy)\Xi = (\textsf{Gen}, \textsf{Sign}, \textsf{Vrfy}), PK\textsf{PK} the public key derivation function and Hash\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 (Kint,Kext,B)(K_{int}, K_{ext}, B), where KK is the state of an actor’s knowledge and BB 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.

  • e\textit{e} - Message exchange

  • tb\textit{tb} - Transaction broadcast

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

  • d\textit{d} - Time delay

  • r\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{int,ext}a,b \in \{int,ext\}:

(Ka,Kb,B)ea(Ka,Kb,B)(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).

(Ka,Kb,B)tba(Ka,Kb,B)(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).

(Ka,Kb,B)ta(Ka,Kb,B)(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).

(Ka,Kb,B)d(Ka,Kb,B)(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 BB (Definition 4.10).

(Kint,Kext,B)rext(n)(Kint/Kint,Kext,B)(K_{int},K_{ext},B) \xrightarrow{r^{ext}(n)} (K_{int}/K_{int}^{\prime},K_{ext},B^{\prime}): A blockchain reorganization of depth nn 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 (Kint,Kext,B)(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 KK is a finite set of transaction templates, private keys, public keys, hash pre-images and signatures. KK can be expanded with a set of public functions Σexec\Sigma_{exec} during symbolic contract execution whenever KK is updated with external information.

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

KkK \vdash k

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

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

    Kint{txswap,int,txabort,int,txsweep,int,txswap,ext,txabort,ext,txsweep,ext,sigpkint(txfund,int),  sigpkint(txswap,int),sigpkint(txabort,in),sigpkint(txsweep,int)}\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)ctrl(out,actor) denotes that outout features an execution path controlled by actoractor. KoutK \vdash out if the output is a member of any transaction template in the knowledge of actor actoractor.

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

    Kint{txswap,int,txabort,int,txsweep,int,txswap,ext,txabort,ext,txsweep,ext,sigpkint(txfund,int),  sigpkint(txswap,int),sigpkint(txabort,in),sigpkint(txsweep,int)}\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 (pkpk in sat(tx.ins)\textsf{sat}(tx^{\prime}.ins)).

Bounded knowledge expansion with Σexec\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 Σexec\Sigma_{exec}. SweepTx consumes controlled outputs and produces owned outputs. Likewise, signatures generated from the public Sign function cannot be used as inputs for Σexec\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 KintK^{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.prevoutin.prevout attributes in the funding transactions, which the actor can extract. For simplicity, we assume that actors reuse private keys for all outputs.

Kint={inv(pkint),b32,txfund,int,txfund,ext}\begin{split} K_{int} = \{ & inv(pk_{int}),b_{32}, tx^{\prime}_{fund, int},tx^{\prime}_{fund, ext}\} \end{split}

Subsequently, since txfund,inttx^{\prime}_{fund, int} and txfund,exttx^{\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.

Kint{txswap,int,txabort,int,txsweep,int,txswap,ext,txabort,ext,txsweep,ext,sigpkint(txfund,int),  sigpkint(txswap,int),sigpkint(txabort,in),sigpkint(txsweep,int)}\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}

The internal actor furthermore can derive signatures which are required to satisfy the the symbolic witnesses featuring public key pkintpk_{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 Σsetup\Sigma_{setup} (Equation 3) and Σexec\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 Ξadapt=(pSign,pVrfy,Adapt,Ext)\Xi_{adapt} = (\textsf{pSign},\:\textsf{pVrfy},\:\textsf{Adapt},\:\textsf{Ext}) for a signature scheme Ξsig=(Gen,Sign,Vrfy)\Xi_{sig} = (\textsf{Gen},\:\textsf{Sign},\:\textsf{Vrfy}).

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

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

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

  • Ext(psigpk(tx,pky),sigpk(tx),pky\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 pkypk_y returns the a private key inv(pky)inv(pk_y).

Given pre-signature psigpk(tx,pky)psig_{pk}(tx^{\prime},pk_y), an observer can extract inv(pky)inv(pk_y) upon learning sigpk(tx)sig_{pk}(tx^{\prime}) with the function Ext\textsf{Ext}. Conversely, given psigpk(tx,pky)psig_{pk}(tx^{\prime},pk_y) and inv(pky)inv(pk_y), a valid signature sigpk(tx)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 Ξadapt\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 txfund,intx_{fund, in} and txfund,extx_{fund,ex} for our atomic swap contract initiated by the internal actor are the following:

mint=andor(pkext,pkint,andv(v(pkint),older(15)))\begin{split} m_{int}=andor(&pk_{ext}, pk_{int}, \\ & and_{v}(v(pk_{int}),older(15))) \\ \end{split}

mext=andor(pkint,pkext,andv(v(pkext),older(10)))\begin{split} m_{ext}=andor(& pk_{int}, pk_{ext}, \\ & and_{v}(v(pk_{ext}),older(10))) \\ \end{split}

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.

Σsetup={Gen,PK,Hash,genTx,pSign,pVrfy}\Sigma_{setup}^{\prime} = \{ \textsf{Gen}, \textsf{PK}, \textsf{Hash}, \textsf{genTx}, \textsf{pSign}, \textsf{pVrfy} \}

Note that GenTx must also generate swap transactions for both actors, so that both actors can generate and verify pre-signatures for swap transactions txswap,int,txswap,exttx_{swap,int}^{\prime}, tx_{swap,ext}^{\prime} of the counter-party. inv(pky)inv(pk_y) is generated by the initiating, internal actor and so inv(pky)Kextinv(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(pky)inv(pk_y), pkypk_y).

Kint={...,inv(pky),psigpkext(txswap,int,pky),psigpkint(txswap,ext,pky)}\begin{split} K_{int} = \{ & ..., inv(pk_y), \\ & psig_{pk_{ext}}(tx^{\prime}_{swap,int},pk_y), psig_{pk_{int}}(tx^{\prime}_{swap,ext},pk_y) \} \end{split}

Kext={...,pky,psigpkint(txswap,ext,pky),psigpkext(txswap,int,pky)}\begin{split} K_{ext} = \{ & ..., pk_y, \\ & psig_{pk_{int}}(tx^{\prime}_{swap,ext},pk_y), psig_{pk_{ext}}(tx^{\prime}_{swap,int},pk_y) \} \end{split}

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

Σexec={SweepTx,Sign,Adapt,Ext}\Sigma_{exec}^{\prime} = \{ \textsf{SweepTx}, \textsf{Sign},\textsf{Adapt}, \textsf{Ext} \}

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 mextm_{ext} require sigpkint(txswap,int)sig_{pk_{int}}(tx^{\prime}_{swap, int}) and sigpkext(txswap,int)sig_{pk_{ext}}(tx^{\prime}_{swap, int}), the latter which is derived with the Adapt function.

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

The external actor can expand its knowledge with adapt, the pre-signature and publication proof to obtain sigpkext(txswap,ext,pky)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 ea(k)e^{a}(k) with payload kk is fire-able by an actor a{int,ext}a \in \{int,ext\} with knowledge KaK_a, if kk is known by the sender but unknown to the recipient.

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

\begin{prooftree}
\AxiomC{$K_{a} \vdash k$}
\AxiomC{$K_{b} \cancel{\vdash} k$}
  \BinaryInfC{$K_b \xrightarrow{e^{a}(k)} K_b\;\cup\;\{k\}$}
\end{prooftree}

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 {Γ0,Γ1,...}=sat(in)\{\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 ww for each transaction template.

Definition 4.4 (Fire-able Transaction Broadcast): A transaction broadcast tbtb for a transaction is fire-able if it is deducible by actor a{int,ext}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 txtx are denoted as witba.insw_{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)(p,t). Arcs pointing to places represent transaction outputs and are denoted output arcs (t,p)(t,p). A given place pp 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){0,1}m(p) \in \{0,1\} returns the number of tokens currently in a place pp. 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 Z\mathcal{Z} is the tuple (K0int,K0ext,P,T,F,Iolder,Iafter,m0,b0)(K^{int}_0, K^{ext}_0,P,T,F, I_{older},I_{after},m_0,b_{0}) such that

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

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

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

  4. For all txK0int/exttx \in K^{int/ext}_0:

    1. There exists a unique tTt \in T for each πi\pi_i of π(tx)\pi(tx).

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

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

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

    1. Iafter(p,t)I_{after}(p,t), Iolder(p,t)t.πiI_{older}(p,t) \models t.\pi_i for tTt \in T

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

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

(2) A place is added to Z\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 afterafter and olderolder constraints expressed in the respective symbolic witness.

Figure 3: Classical Petri Net components consist of places, arcs, transitions and tokens. The classical Petri Net firing rule denotes that a transition can only fire if its input arcs are connected to places populated with tokens.

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

t(p)={1if  (p,t)F0if  (p,t)∉Ft(p)^{-}=\begin{cases}1 & if\; (p,t)\in F\\0 & if \; (p,t)\not\in F\end{cases}

Similarly, we can denote (p,t)(p,t)^{-} as the required token availability for place pp required by an input arc, which will trivially be 1 for a connected place and 0 for a disconnected one.

Figure 4: A Trace-Net model of an atomic swap initiated by the internal actor is shown. Input arc and transition markings are overlayed on top of the Trace-Net skeleton. Transitions are annotated with the actors who can produce the corresponding valid transaction witnesses from knowledge. The state shown above represents the contract state zz imminently after the confirmation of the internal actor’s funding transaction. Note the chain-height is 20 at time of evaluation, and that abort delays are set to 15 and 10 blocks respectively.

Trace-Net Z\mathcal{Z} models the possible on-chain contract transactions and the possible states of unspent outputs throughout the symbolic execution of the contract. However, in order to model the contract state, we must also introduce a notion of time to determine the expiration of time-locks.

Definition 4.7 (Time Markings): A function h:(P×T)N0h_{*}:(P \times T) \rightarrow \mathbb{N}^0 is a time marking in Z\mathcal{Z}.

In order to express the satisfaction or dissatisfaction of time constraints imposed by spending conditions featuring (after>=i)(after >=i) or (older>i)(older >i) expressions, stateful time markings are applied to input arcs. For an on-chain transition to be fire-able, all time markings must have released the respective on-chain transition. A time marking releases its input arc when they reach or exceed their respective earliest firing times.

  1. holder(p,t)Iolder(p,t))h_{older}(p,t) \geq I_{older}(p,t))

  2. hafter(p,t)Iafter(p,t))h_{after}(p,t) \geq I_{after}(p,t))

We can now define a contract state in the Trace-Net framework. It consists of the state of actor knowledge, time markings, place markings and on-chain history of confirmed blockchain transactions. An example of a contract state is depicted in Figure 4, which represents the contract state of an atomic swap initiated by the internal actor after the contract has been unilaterally funded by the internal, verifying party.

Definition 4.8 (Trace-Net State): Let a state in Trace-Net Z be the tuple z:=(Kin,Kex,B)=(Kin,Kex,holder,hafter,m,q)z := (K_{in}, K_{ex}, B) = (K_{in}, K_{ex}, h_{older}, h_{after}, m, q) such that

  1. For all (p,t)F:(p,t)\in F:

    1. ((p,t)<m)holder(p,t)=0((p,t)^{-}< m) \rightarrow h_{older}(p,t)=0

    2. ((p,t)=m)holder(p,t)N0((p,t)^{-}= m) \rightarrow h_{older}(p,t) \in \mathbb{N}^0

    3. hafter(p,t)Nh_{after}(p,t) \rightarrow \mathbb{N}

  2. mm is the current place marking

  3. qq is the current on-chain history

(1) The input arc time marking holder(p,t)h_{older}(p,t) can only begin to increment when a symbolic unspent output becomes available. hafterh_{after} is always equal to the blockheight, as it only enforces a global expiration time unrelated to output confirmation ages.

Definition 4.9 (On-chain history): The on-chain history at a Trace-Net state is the history of the on-chain contract transactions appended to the blockchain.

On-chain histories can be expressed as a list of tuples q={(t0,h0),(t1,h1),...}q = \{(t_{0}, h_{0}), (t_{1}, h_{1}),...\} ordered according to their position in the blockchain, where hih_i represents the blockheight of the transaction corresponding to tit_i.

Definition 4.10 (Time transition d): Let d be a non-zero natural number, and z a state in Z\mathcal{Z}, then the elapsing of time d will change state z into zz^{\prime} such that

  1. Kin,Kex,m:=Kin,Kex,mK_{in}^{\prime}, K_{ex}^{\prime}, m^{\prime} := K_{in}, K_{ex},m

  2. holder(p,t):={holder(p,t)+diffm(p,t)0iffm≱(p,t)h^{\prime}_{older}(p,t) := \begin{cases}h_{older}(p,t)+d & iff \quad m \geq (p,t)^{-} \\0 & iff \quad m \not\geq (p,t)^{-} \end{cases}

  3. hafter:=hafter+dh_{after}^{\prime} := h_{after}^{\prime} + d

Note that the holder(p,t)h_{older}(p,t) delay marking does not begin to increment before the input place is populated with a token. For an older marking for input arc (p,t)(p,t) to release its on-chain transition tt, it must increment beyond an earliest firing time Iolder(p,t)I_{older}(p, t), which in turn is determined by the presence of an older time-lock in the associated output satisfaction conditions given by t.πit.\pi_i, where πi\pi_i is the witness permutation associated with the on-chain transition tt (Definition 4.6). In the absence of an older time-lock, Iolder(p,t)I_{older}(p,t) is set to 00. The hafter(p,t)h_{after}(p,t) input arc time marking simply holds the value of the chain height at the time of evaluation and is initiated to the initial blockheight b0b_0. It releases the on-chain transition at the earliest firing time which is determined by the after time-lock of the output its input arc is connected to. In absence of an after time-lock, Iafter(p,t)I_{after}(p,t) is set to 00.

Definition 4.11 (Valid On-chain Transition): An on-chain transition t is valid if

  1. mtm \geq t^{-}

  2. holder(p,t)Iolder(p,t))h_{older}(p,t) \geq I_{older}(p,t)) for all pP.(p,t)Fp \in P.(p,t) \in F

  3. hafter(p,t)Iafter(p,t)h_{after}(p,t) \geq I_{after}(p,t) for all pP.(p,t)Fp \in P.(p,t) \in F

Definition 4.12 (Fire-able On-chain Transition): A transition t in Trace-Net state Z is ready to fire by an actor if

  1. tt is a valid on-chain transaction

  2. tbtb for tx(t)tx(t) is not fireable (Definition: 4.5)

  3. actor(Kactortx(t))\exists actor (K_{actor} \vdash tx(t))

An on-chain transition tt can fire if its pre-places are populated, and all input arc time markings have released, and a single or both actors can deduce valid witnesses for all inputs from knowledge. An on-chain transition firing is always proceeded by a transaction broadcast (tbtb for tx(t)tx(t)), if the broadcast results in an update of an actor’s knowledge: thus, tbtb and tt cannot both be fireable.

Definition 4.13 (On-chain transition firing): The firing of a fire-able on-chain transition of t in Trace-Net Z\mathcal{Z} changes the state z into z=(Kin,Kex,holder,hafter,m)z^{\prime} = (K_{in}, K_{ex}, h_{older}, h_{after}, m^{\prime}) where

  1. m:=m+Δtm : = m + \Delta\:t

We denote Δt\Delta\:t as change in the place markings of the Trace-Net as a result of the on-chain transition firing.

Definition 4.14 (Chain roll-back transition firing): A roll-back of a blockchain by nn blocks by the adversarial external actor at state zz is always fireable. It reverts the transactions in the on-chain chronology which were confirmed within nn blocks of the current height bb and changes the contract state zz to z=(Kin,Kex,holder,hafter,m,q)z^{\prime} = (K_{in}, K_{ex}, h_{older}^{\prime}, h_{after}^{\prime}, m^{\prime}, q^{\prime}) where

  1. qq^{\prime} has reverted all transactions in qq which were confirmed in the rolled-back blocks.

  2. mrevΔtm^{\prime} - \sum^{rev}\Delta t, where revrev is the set of reverted transactions and Δt\Delta t the changes in place marking they effected.

  3. hafter:={hafternif  haftern>00if  haftern0h_{after}^{\prime}:=\begin{cases}h_{after} - n & if\; h_{after} - n > 0 \\0 & if \; h_{after} - n \leq 0\end{cases}

  4. holder(p,t):={holder(p,t)nif  holder(p,t)n>00if  haftern0h_{older}(p,t)^{\prime}:=\begin{cases}h_{older}(p,t) - n & if\; h_{older}(p,t) - n > 0 \\0 & if \; h_{after} - n \leq 0\end{cases}

Note that the knowledge of the actors is not rolled back during a roll-back transition firing, as the previously observed and derived knowledge of an actor cannot be deleted by the adversarial external actor. Once a roll-back is completed, it is possible to model alternative chain branches created by the 51% attacker, who can generate any valid contract transaction order in the new branch (Section 5).

Trace-Net Generation

Algorithm 1 summarizes the generation of a Trace-Net from a set of Bitcoin contract transaction templates in Kint,extK_{int,ext} after the completion of the implemented contract setup phase.

To generate the Trace-Net Z\mathcal{Z} in state z0z_0, all transactions in the contract are iterated through. Places are generated for each in- and output in the contract (Lines 7-16). Subsequently, a transaction is represented by one or more on-chain transition instances, each representing a unique symbolic witness permutation: the product returns a cartesian product over all sets of alternative symbolic witnesses Γˉi\bar{\Gamma}_i for each ith input (Lines 19, 20) and returns a set of symbolic witness permutations π(tx)={π0,π1,...}\pi(tx) = \{ \pi_0, \pi_1, ...\}. A separate on-chain transition is instantiated for each with the corresponding input arcs adopting earliest firing time values from the respective symbolic witness constraints (Lines 27, 28).

5. Automated Trace-Net Analysis

Figure 5: A partial reachability graph for our atomic-swap contract example is shown above which has been generated with transaction confirmation delays and reorganization depths set to zero for simplicity. The contract is being evaluated for its initial state z0z_0, before any funding transaction has been executed. Each contract execution trace shown is denoted with the outcome of its execution.

Let Z\mathcal{Z} be our Trace-Net and z0={K0in,K0ex,holder,0=0,hafter,0=b0,m0,q0=}z_{0} = \{ K^{in}_0, K^{ex}_0, h_{older,0}=0, h_{after,0}=b_0, m_0, q_0 = \emptyset \} its initial state. We are interested in generating the transition system or reachability graph RGRG which expresses the total state space reachable by all possible contract executions. At each state zz, the fireability of messages, transaction broadcast, transaction confirmation and blockchain roll-backs is evaluated, which in turn implies the strategies of each actor in state zz. We parameterize the generation of RGRG with two additional parameters: confirmation delays and maximum blockchain reorganization depth.

Confirmation delays

The confirmation delay between on-chain transaction broadcast and confirmation in a block is denoted cintc_{int} and cextc_{ext} respectively, where cint,cextZc_{int}, c_{ext} \in \mathbb{Z}. Non-zero confirmation delays imply that an on-chain transaction fired by actor will always be preceded by a delay transition of duration cint/extc_{int/ext}.

Blockchain reorganizations

We explicitly model the ability of the adversary to reorganize the blockchain up to a depth of rmaxZr_{max} \in \mathbb{Z} when generating RGRG. At each Trace-Net state, alternate blockchain reorganizations of all depths up to rmaxr_{max} are generated. An adversarial reorganization can be described as a rr-depth roll-back (Definition 4.14) transition from state zz to state zbrz_{br}, followed by the generation of all possible contract states reachable within r+1r+1 blocks starting from zbrz_{br} fireable by the external actor (Algorithm 2, Lines 26-33). Although not explored in Algorithm 2, the chain heights from resulting reorganizations can include heights which are larger than 1. On-chain contract transitions fired by the external actor in the reorganized branch do not need to be prepended with a confirmation delay, as the external actor can directly append any valid transaction to any block in the reorganized chain, without having to broadcast to the public network. A blockchain reorganization from zz to the reorganized state zz' is a single externally fireable transition in the reachability graph: zreorgzz \xrightarrow{reorg} z^{\prime}.

The resulting reachability graph RG(Z,zinit,cint,ext,rmax)=(W,E)RG(\mathcal{Z}, z_{init}, c_{int,ext},r_{max}) = (W, E) is a directed graph with the set of vertices WW, and edges EE. It is necessarily finite, given the bounded knowledge expansion after each state transition and the finite number of contract transactions. Figure 5 illustrates the partial reachability graph of an atomic swap contract initiated by the external actor. Algorithm 2 generates the contract state space reachable from an initial state z0z_{0} by recursively computing all child states directly reachable via transitions fireable in each state. The time delay transition is only fired if its firing results in an expiration of time-locks, thereby releasing a contract transaction. The time-transition delay is chosen to be minimal, in order to reflect the transaction execution order enforced by contract time-locks.

Feasible termination trace

A feasible termination trace σ\sigma will traverse the reachability graph RG(Z,z0,cint,ext,rmax)RG(\mathcal{Z}, z_0, c_{int,ext}, r_{max}) from z0z_{0} until a terminal state znz_{n} is reached, where no further transitions can be fired.

σ=z0θ0z1...zn1θn1zn\sigma = z_{0} \overset{\theta_{0}}{\rightarrow} z_{1} ... z_{n-1}\overset{\theta_{n-1}}{\rightarrow}z_{n}

The finite reachability graph allows an exhaustive analysis of all feasible contract traces. The types of transitions and firing actors can be analyzed to infer temporal contract safety properties of interest.

6. Contract Safety Properties

We can now formalize the notion of trustless contract execution, which implies that the verifying actor can always safely terminate the contract execution despite any adversarial strategies pursued by the external actor.

6.1 Trustless Execution Property

(i) Safe Terminal States

The safety of terminal states in a reachability graph RG(Z,zinit,..)RG(\mathcal{Z}, z_{init},..) are determined by a user-supplied safety policy function policy(Kint,ext,m)\textsf{policy}(K_{int,ext}, m), and therefore depends on the actor knowledge state and output markings at the terminal state in question. Actor knowledge states can imply information leaked to the counter-party, and place markings infer the balance owned by the internal actor. For our atomic swap example, we could suggest a policy function which ensures that in a safe terminal state, the internal actor must obtain a balance equal to the amount used to fund the contract, thereby ensuring that only terminal states of the abort and success paths are considered safe.

(ii) (Un)cooperative Termination Trace

An execution trace σint\sigma^{int} in RGRG beginning at a state zinitz_{init} which leads to a safe terminal state within finite transitions fired by a single actor is an uncooperative termination trace. The presence of internally fireable, uncooperative traces from contract state zz implies that the verifying actor can reach a safe terminal state if the external actor ceases to participate in the contract protocol. A cooperative termination trace is a contract execution trace which includes transitions fired by both actors.

(iii) Safe Non-terminal States

  1. A safe non-terminal state zsz_{s} in RGRG features at least one uncooperative termination trace σint\sigma^{int} fireable by the verifying actor.

  2. If the external actor can fire any on-chain transition textt^{ext} in zz along σint\sigma^{int}, then the resulting state zz^{\prime} computed from ztextzz \overset{t^{ext}}{\rightarrow} z^{\prime} must also be a safe state.

(iv) Safe Termination Trace

If all intermediary states along a (un)cooperative termination trace σint/ext\sigma^{int/ext} are safe for the verifying internal actor, then the trace is considered safe, as the verifying actor is guaranteed to have an execution path to safe termination, despite any adversarial strategies pursued by the actor.

Definition 6.1 (Trustless Execution Property): The contract execution from a state zinitz_{init} exhibits the trustless execution property if there exists at least one safe cooperative trace beginning at zinitz_{init}.

6.2 Analysis of Contract Updates

A contract update can occur whilst a contract is not yet terminated. This implies the execution of an additional setup phase and new transaction templates being added the current actor knowledge Kint,Kext,RGupdateKint,Kext,RGK_{int}, K_{ext}, RG \xrightarrow{update} K_{int}^{\prime}, K_{ext}^{\prime}, RG^{\prime}, from which an updated Trace-Net and reachability graph RGRG^{\prime} are generated. If RGRG^{\prime} features additional, safely reachable terminal states the contract update is safe, as it increases the contract-state space with additional safe termination traces.

6.3 Contract State Stability

A contract state zz is stable if

RG(Z,z,cint,ext,rmax)=RG(Z,z,cint,ext,rmax)RG(\mathcal{Z}, z, c_{int,ext}, r_{max}) = RG(\mathcal{Z}, z^{\prime}, c_{int,ext}, r_{max})(5)

where zzz \overset{\infty}{\rightarrow} z^{\prime} and \infty is a delay of infinite duration. This implies that the execution of the contract can be deferred indefinitely. Both the analysis of contract updates and verification of the state stability property can be useful in the analysis of off-chain protocols, which defer transaction broadcasts so that contract updates can be performed off-chain.

7. Conclusion

We have introduced a novel method to automate the verification of multi-party Bitcoin contract protocols at the raw contract transactions level. The main advantages of contract verification at the implementation level is the ability to verify a contract at run-time and to accurately model the underlying blockchain execution environment, which may include confirmation delays and possible chain reorganizations. Furthermore, Trace-Net can be useful as an effective monitoring framework for contract protocol implementations.

The main components of our framework consist of a stateful actor knowledge model and an extended Petri Net model which captures the semantics of on-chain contract output availability and time-locks. Together, these two components determine which strategies are available to contracting participants in all contract protocol states. Furthermore, we have demonstrated the extension of Trace-Net actor knowledge model with adaptor signatures in Section 4.1.1, thereby extending Trace-Net verification to contracts which can be executed privately.

The instantiation of Trace-Net was illustrated with atomic swaps and we emphasize that Trace-Net semantics are sufficiently expressive for more complex protocols such as payment channel networks [10] or generalized state-channels [11]. Trace-Net lends itself to further investigations, including methods to efficiently represent the unfolded state-space in which the verification is performed, as the state-space explosion problem remains untreated. Proposals [50] [8] have been made to extend Bitcoin script, providing Turing-machine expressiveness, which would be a valuable future area of research for Trace-Net. Furthermore, domain-specific contract specification languages can be investigated which compile to Trace-Net models as an intermediate representation, whilst providing inherent contract safety and liveness guarantees. We intend to develop research tooling to explore the verification of Trace-Net models with time-proven model-checking frameworks.

Acknowledgments

Thanks to the reviewers of the early versions of this paper. A special acknowledgement to Josh Harvey for early discussions on formal Petri Net specifications of automata-based programs which inspired the idea of Trace-Net for Bitcoin contracts. Bitcoin contracting protocol experts Antoine Riard, Dmitry Petukhov, Nadav Cohen, and Thibaut le Guilly all provided valuable perspectives to refine Trace-Net semantics. Finally, the author wishes to express his sincere gratitude to Professor Alberto Lluch Lafuente and Professor Andrea Vandin for graciously sharing their expertise in formal methods and model-checking methodology, without which this work would not have been possible.

Comments
0
comment
No comments here
Why not start the discussion?