Advertisement

SoK: Unraveling Bitcoin Smart Contracts

  • Nicola Atzei
  • Massimo Bartoletti
  • Tiziana Cimoli
  • Stefano Lande
  • Roberto Zunino
Open Access
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10804)

Abstract

Albeit the primary usage of Bitcoin is to exchange currency, its blockchain and consensus mechanism can also be exploited to securely execute some forms of smart contracts. These are agreements among mutually distrusting parties, which can be automatically enforced without resorting to a trusted intermediary. Over the last few years a variety of smart contracts for Bitcoin have been proposed, both by the academic community and by that of developers. However, the heterogeneity in their treatment, the informal (often incomplete or imprecise) descriptions, and the use of poorly documented Bitcoin features, pose obstacles to the research. In this paper we present a comprehensive survey of smart contracts on Bitcoin, in a uniform framework. Our treatment is based on a new formal specification language for smart contracts, which also helps us to highlight some subtleties in existing informal descriptions, making a step towards automatic verification. We discuss some obstacles to the diffusion of smart contracts on Bitcoin, and we identify the most promising open research challenges.

1 Introduction

The term “smart contract” was conceived in [43] to describe agreements between two or more parties, that can be automatically enforced without a trusted intermediary. Fallen into oblivion for several years, the idea of smart contract has been resurrected with the recent surge of distributed ledger technologies, led by Ethereum (http://www.ethereum.org/) and Hyperledger (https://www.hyperledger.org/). In such incarnations, smart contracts are rendered as computer programs. Users can request the execution of contracts by sending suitable transactions to the nodes of a peer-to-peer network. These nodes collectively maintain the history of all transactions in a public, append-only data structure, called blockchain. The sequence of transactions on the blockchain determines the state of each contract, and, accordingly, the assets of each user.

A crucial feature of smart contracts is that their correct execution does not rely on a trusted authority: rather, the nodes which process transactions are assumed to be mutually untrusted. Potential conflicts in the execution of contracts are resolved through a consensus protocol, whose nature depends on the specific platform (e.g., it is based on “proof-of-work” in Ethereum). Ideally, contracts execute correctly whenever the adversary does not control the majority of some resource (e.g., computational power for “proof-of-work” consensus).

The absence of a trusted intermediary, combined with the possibility of transferring money given by blockchain-based cryptocurrencies, creates a fertile ground for the development of smart contracts. For instance, a smart contract may promise to pay a reward to anyone who provides some value that satisfies a given public predicate. This generalises cryptographic puzzles, like breaking a cipher, inverting a hash function, etc.

Since smart contracts handle the ownership of valuable assets, attackers may be tempted to exploit vulnerabilities in their implementation to steal or tamper with these assets. Although analysis tools [17, 30, 34] may improve the security of contracts, so far they have not been able to completely prevent attacks. For instance, a series of vulnerabilities in Ethereum contracts [10] have been exploited, causing money losses in the order of hundreds of millions of dollars [3, 4, 5].

Using domain-specific languages (possibly, not Turing-complete) could help to overcome these security issues, by reducing the distance between contract specification and implementation. For instance, despite the discouraging limitations of its scripting language, Bitcoin has been shown to support a variety of smart contracts. Lotteries [6, 14, 16, 36], gambling games [32], contingent payments [13, 24, 35], and other kinds of fair multi-party computations [8, 31] are some examples of the capabilities of Bitcoin as a smart contracts platform.

Unlike Ethereum, where contracts can be expressed as computer programs with a well-defined semantics, Bitcoin contracts are usually realised as cryptographic protocols, where participants send/receive messages, verify signatures, and put/search transactions on the blockchain. The informal (often incomplete or imprecise) narration of these protocols, together with the use of poorly documented features of Bitcoin (e.g., segregated witnesses, scripts, signature modifiers, temporal constraints), and the overall heterogeneity in their treatment, pose serious obstacles to the research on smart contracts in Bitcoin.

Contributions. This paper is, at the best of our knowledge, the first systematic survey of smart contracts on Bitcoin. In order to obtain a uniform and precise treatment, we exploit a new formal model of contracts. Our model is based on a process calculus with primitives to construct Bitcoin transactions, to put them on the blockchain, and to search the blockchain for transactions matching given patterns. Our calculus allows us to give smart contracts a precise operational semantics, which describes the interactions of the (possibly dishonest) participants involved in the execution of a contract.

We exploit our model to systematically formalise a large portion of the contracts proposed so far both by researchers and Bitcoin developers. In many cases, we find that specifying a contract with the intended security properties is significantly more complex than expected after reading the informal descriptions of the contract. Usually, such informal descriptions focus on the case where all participants are honest, neglecting the cases where one needs to compensate for some unexpected behaviour of the dishonest environment.

Overall, our work aims at building a bridge between research communities: from that of cryptography, where smart contracts have been investigated first, to those of programming languages and formal methods, where smart contracts could be expressed using proper linguistic models, supporting advanced analysis and verification techniques. We outline some promising research perspectives on smart contracts, both in Bitcoin and in other cryptocurrencies, where the synergy between the two communities could have a strong impact in future research.

2 Background on Bitcoin Transactions

In this section we give a minimalistic introduction to Bitcoin [21, 38], focussing on the crucial notion of transaction. To this purpose, we rely on the model of Bitcoin transactions in [11]. Here, instead of repeating the formal machinery of [11], we introduce the needed concepts through a series of examples. We will however follow the same notation of [11], and point to the formal definitions therein, to allow the reader to make precise the intuitions provided in this paper.

Bitcoin is a decentralised infrastructure to securely transfer currency (the bitcoins, Open image in new window ) between users. Transfers of bitcoins are represented as transactions, and the history of all transactions is stored in a public, append-only, distributed data structure called blockchain. Each user can create an arbitrary number of pseudonyms through which sending and receiving bitcoins. The balance of a user is not explicitly stored within the blockchain, but it is determined by the amount of unspent bitcoins directed to the pseudonyms under her control, through one or more transactions. The logic used for linking inputs to outputs is specified by programmable functions, called scripts.

Hereafter we will abstract from a few technical details of Bitcoin, e.g. the fact that transactions are grouped into blocks, and that each transaction must pay a fee to the “miner” who appends it to the blockchain. We refer to [11] for a discussion on the differences between the formal model and the actual Bitcoin.

2.1 Transactions

In their simplest form, Bitcoin transactions allow to transfer bitcoins from one participant to another one. The only exception are the so-called coinbase transactions, which can generate fresh bitcoins. Following [11], we assume that there exists a single coinbase transaction, the first one in the blockchain. We represent this transaction, say Open image in new window , as follows:

The transaction Open image in new window has three fields. The fields Open image in new window and Open image in new window are set to \(\bot \), meaning that Open image in new window does not point backwards to any other transaction (since Open image in new window is the first one on the blockchain). The field Open image in new window contains a pair. The first element of the pair, \(\lambda x_{}.\, x_{}< 51\), is a script, that given as input a value \(x_{}\), checks if \(x_{}< 51\) (this is just for didactical purposes: we will introduce more useful scripts in a while). The second element of the pair, Open image in new window , is the amount of currency that can be transferred to other transactions.

Now, assume that participant Open image in new window wants to redeem Open image in new window from Open image in new window , and transfer that amount under her control. To do this, Open image in new window has to append to the blockchain a new transaction, e.g.:

The field Open image in new window points to the transaction Open image in new window in the blockchain. To be able to redeem from there Open image in new window , Open image in new window must provide a witness which makes the script within Open image in new window evaluate to true. In this case the witness is 42, hence the redeem succeeds, and Open image in new window is considered spent. The script within Open image in new window is the most commonly used one in Bitcoin: it verifies the signature \(x_{}\) with Open image in new window ’s public key. The message against which the signature is verified is the transaction1 which attempts to redeem Open image in new window .

Now, to transfer Open image in new window to another participant Open image in new window , Open image in new window can append to the blockchain the following transaction:

where the witness Open image in new window is Open image in new window ’s signature on Open image in new window (but for the Open image in new window field itself).

The ones shown above represent just the simplest cases of transactions. More in general, a Bitcoin transaction can collect bitcoins from many inputs, and split them between one or more outputs; further, it can use more complex scripts, and specify time constraints on when it can be appended to the blockchain.

Following [11], hereafter we represent transactions as tuples of the form Open image in new window , where:

In transaction fields, we represent a list \(\ell _1 \cdots \ell _n\) as \(1 \mapsto \ell _1, \ldots , n \mapsto \ell _n\), or just as \(\ell _1\) when \(n=1\). We denote with Open image in new window the canonical transaction, i.e. the transaction with a single output of the form Open image in new window , and with all the other fields empty (denoted with \(\bot \)).

Example 1

Consider the transactions in Fig. 1. In Open image in new window there are two outputs: the first one transfers Open image in new window to any transaction Open image in new window which provides as witness a signature of Open image in new window with key \(k_{}\); the second output can transfer Open image in new window to a transaction whose witness satisfies the script \(e_1\). The transaction Open image in new window tries to redeem Open image in new window from the output at index 1 of Open image in new window , by providing the witness \(\sigma _1\). Since Open image in new window , then Open image in new window can be appended only after at least \(t_{}\) time units have passed since the transaction in Open image in new window (i.e., Open image in new window ) appeared on the blockchain. In Open image in new window , the input 1 refers to the output 2 of Open image in new window , and the input 2 refers to the output 1 of Open image in new window . The witness \(\sigma _2\) and \(\sigma _2'\) are used to evaluate Open image in new window , replacing the occurrences of \(x_{}\) and \(x_{}'\) in \(e_1\). Similarly, \(\sigma _3\) is used to evaluate Open image in new window , replacing the occurrences of \(x_{}\) in \(e_2\). The transaction Open image in new window can be put on the blockchain only after time \(t'_{}\).    \(\square \)

Fig. 1.

Three Bitcoin transactions.

2.2 Scripts

In Bitcoin, scripts are small programs written in a non-Turing equivalent language. Whoever provides a witness that makes the script evaluate to “true”, can redeem the bitcoins retained in the associated (unspent) output. In the abstract model, scripts are terms of the form \(\lambda \varvec{z} . e\), where \(\varvec{z}\) is a sequence of variables occurring in \(e\), and \(e\) is an expression with the following syntax:Besides variables \(x_{}\), constants \(k_{}\), and basic arithmetic/logical operators, the other expression are peculiar: \(| e |\) denotes the size, in bytes, of the evaluation of \(e\); \(\mathsf{H}(e)\) evaluates to the hash of \(e\); \(\mathsf{versig}_{\varvec{k_{}}}({\varvec{e}})\) evaluates to true iff the sequence of signatures \(\varvec{e}\) (say, of length m) is verified by using m out of the n keys in \(\varvec{k_{}}\). For instance, the script \(\lambda x_{}. \mathsf{versig}_{k_{}}({x_{}})\) is satisfied if x is a signature on the redeeming transaction, verified with the key \(k_{}\). The expressions Open image in new window and Open image in new window define absolute and relative time constraints: they evaluate as \(e\) if the constraints are satisfied, otherwise they evaluate to false.
In Fig. 2 we recap from [11] the semantics of script expressions. The function Open image in new window takes three parameters: Open image in new window is the redeeming transaction, i is the index of the redeeming witness, and \(\rho \) is a map from variables to values. We use \(\bot \) to represent the “failure” of the evaluation, Open image in new window for a public hash function, and \( size ({n})\) for the size (in bytes) of an integer n. The function Open image in new window verifies a sequence of signatures \(\varvec{\sigma }\) against a sequence of keys \(\varvec{k_{}}\) (see Sect. 2.3) All the semantic operators used in Fig. 2 are strict, i.e. they evaluate to \(\bot \) if some of their operands is \(\bot \). We use syntactic sugar for expressions, e.g. \( false \) denotes \(1~\textsf {=}~0\), \( true \) denotes \(1~\textsf {=}~1\), while \(e~\textsf {and}~e'\) denotes \(\mathsf {if}~{e}~\mathsf {then}~{e'}~\mathsf {else}~{ false }\).
Fig. 2.

Semantics of script expressions.

Example 2

Recall the transactions in Fig. 1. Let \(e_1\) (the script expression within Open image in new window ) be defined as Open image in new window , for \(h_{}^{}\) and \(t'_{}\) constants such that Open image in new window . Further, let \(\sigma _2\) and \(\sigma _2'\) (the witnesses within Open image in new window ) be respectively Open image in new window and \(s_{}^{}\), where Open image in new window is the signature of Open image in new window (excluding its witnesses) with key \(k_{}\), and \(s_{}^{}\) is a preimage of \(h_{}^{}\), i.e. Open image in new window . Let Open image in new window . To redeem Open image in new window with the witness Open image in new window , the script expression is evaluated as follows:   \(\square \)

2.3 Transaction Signatures

The signatures verified with Open image in new window never apply to the whole transaction: the content of Open image in new window field is never signed, while the other fields can be excluded from the signature according to some predefined patterns. To sign parts of a transaction, we first erase the fields which we want to neglect in the signature. Technically, we set these fields to the “null” value \(\bot \) using a transaction substitution.

A transaction substitution Open image in new window replaces the content of field Open image in new window with d. If the field is indexed (i.e., all fields but Open image in new window ), we denote with Open image in new window the substitution of the i-th item in field Open image in new window , and with Open image in new window the substitution of all the items of field Open image in new window but the i-th. For instance, to set all the elements of the Open image in new window field of Open image in new window to \(\bot \), we write Open image in new window , and to additionally set the second input to \(\bot \) we write Open image in new window .

In Bitcoin, there exists a fixed set of transaction substitutions. We represent them as signature modifiers, i.e. transaction substitutions which set to \(\bot \) the fields which will not be signed. Signatures never apply to the whole transaction: modifiers always discard the content of the Open image in new window , while they can keep all the inputs or only one, and all the outputs, or only one, or none. Modifiers also take a parameter i, which is instantiated to the index of the witness where the signature will be included. Below we only present two signature modifiers, since the others are not commonly used in Bitcoin smart contracts.

The modifier Open image in new window only sets the first witness to i, and the other witnesses to \(\bot \) (so, all inputs and all outputs are signed). This ensures that a signature computed for being included in the witness at index i can not be used in any witness with index \(j \ne i\):The modifier Open image in new window removes the witnesses, and all the inputs but the one at index i (so, a single input and all outputs are signed). Differently from Open image in new window , this modifier discards the index i, so the signature can be included in any witness:Signatures carry information about which parts of the transaction are signed: formally, they are pairs \(\sigma = (w,\mu _{})\), where \(\mu \) is the modifier, and w is the signature on the transaction Open image in new window modified with \(\mu _{}\). We denote such signature as Open image in new window , where \(k_{}\) is a key, and i is the index used by \(\mu _{}\), if any. Verification of a signature \(\sigma \) for index i is denoted by Open image in new window . Formally:where Open image in new window and \( ver \) are, respectively, the signing function and the verification function of a digital signature scheme.

Multi-signature verification Open image in new window extends verification to the case where \(\varvec{\sigma }\) is a sequence of signatures and \(\varvec{k_{}}\) is a sequence of keys. Intuitively, if \(|\varvec{\sigma }|=m\) and \(|\varvec{k_{}}|=n\), it implements a m-of-n multi-signature scheme, evaluating to true if all the m signatures match (some of) the keys in \(\varvec{k_{}}\). The actual definition also takes into account the order of signatures, as formalised in Definition 6 of [11].

2.4 Blockchain and Consistency

Abstracting away from the fact that the actual Bitcoin blockchain is formed by blocks of transactions, here we represent a blockchain Open image in new window as a sequence of pairs Open image in new window , where \(t_{i}\) is the time when Open image in new window has been appended, and the values \(t_{i}\) are increasing. We say that the j-th output of the transaction Open image in new window in the blockchain is spent (or, for brevity, that Open image in new window is spent) if there exists some transaction Open image in new window in the blockchain (with \(i' > i\)) and some \(j'\) such that Open image in new window .

We now describe when a pair Open image in new window can be appended to Open image in new window . Following [11], we say that Open image in new window is a consistent update of Open image in new window at time \(t_{}\), in symbols Open image in new window , when the following conditions hold:
  1. 1.
    for each input i of Open image in new window , if Open image in new window then:
    1. (a)

      Open image in new window corresponds to one of the transactions in Open image in new window ;

       
    2. (b)
       
    3. (c)

      the witness Open image in new window makes the script in Open image in new window evaluate to true;

       
     
  2. 2.

    the time constraints Open image in new window and Open image in new window in Open image in new window are satisfied at time \(t_{}\ge t_{n}\);

     
  3. 3.

    the sum of the amounts of the inputs of Open image in new window is greater or equal2 to the sum of the amount of its outputs.

     

We assume that each transaction Open image in new window in the blockchain is a consistent update of the sequence of past transactions Open image in new window . The consistency of the blockchain is actually ensured by the Bitcoin consensus protocol.

Example 3

Recall the transactions in Fig. 1. Assume a blockchain Open image in new window whose last pair is Open image in new window and \(t_{1} \ge t'_{}\), while Open image in new window and Open image in new window are not in Open image in new window .

We verify that Open image in new window is a consistent update of Open image in new window , assuming \(t_{2} = t_{1} + t_{}\) and that \(\sigma _1\) is the signature of Open image in new window with (the private part of) key \(k_{}\). The only input of Open image in new window is Open image in new window . Conditions 1a and 1b are satisfied, since Open image in new window is unspent in Open image in new window . Condition 1c holds because \(\mathsf{versig}_{k_{}}({\sigma _1})\) evaluates to true. Condition 2 holds: indeed the relative timelock in Open image in new window is satisfied because \(t_{2} - t_{1} \ge t_{}\). Condition 3 holds because the amount of the input of Open image in new window , i.e. Open image in new window , is equal to the amount of its output. Note instead that Open image in new window would not be a consistent update of Open image in new window , since it violates condition 1a on the second input.

Now, let Open image in new window . We verify that Open image in new window is a consistent update of Open image in new window , assuming \(t_{3} \ge t_{2}\), \(e_1\) as in Example 2, and \(e_2 = \mathsf{versig}_{k'_{}}({x_{}})\). Further, let Open image in new window , let \(\sigma _2' = s_{}^{}\), and Open image in new window . Conditions 1a and 1b hold, because Open image in new window and Open image in new window are in Open image in new window , and the referred outputs are unspent. Condition 1c holds because the output scripts Open image in new window and Open image in new window against \(\sigma _2,\sigma _2'\) and \(\sigma _3\) evaluate to true. Condition 2 is satisfied at \(t_{3} \ge t_{2} \ge t_{1} \ge t'_{}\). Finally, condition 3 holds because the amount Open image in new window in Open image in new window is equal to the sum of the amounts in Open image in new window and Open image in new window .    \(\square \)

3 Modelling Bitcoin Contracts

In this section we introduce a formal model of the behavior of the participants in a contract, building upon the model of Bitcoin transactions in [11].

We start by formalising a simple language of expressions, which represent both the messages sent over the network, and the values used in internal computations made by the participants. Hereafter, we assume a set \(\mathsf Var\) of variables, and we define the set \(\mathsf Val\) of values comprising constants \(k_{}\in \mathbb {Z}\), signatures \(\sigma \), scripts \(\lambda \varvec{z} . e\), transactions Open image in new window , and currency values \(v_{}\).

Definition 1

(Contract expressions). We define contract expressions through the following syntax:

where \(\varvec{E_{}}\) denotes a finite sequence of expressions (i.e., \(\varvec{E_{}} = E_{1} \cdots E_{n}\)). We define the function \({\llbracket {\cdot }\rrbracket _{}}\) from (variable-free) contract expressions to values in Fig. 3. As a notational shorthand, we omit the index i in Open image in new window (resp. Open image in new window ) when the signed (resp. verified) transactions have a single input.

Fig. 3.

Semantics of contract expressions.

Intuitively, when \(T_{}\) evaluates to a transaction Open image in new window , the expression Open image in new window represents the transaction obtained from Open image in new window by substituting the field Open image in new window with the sequence of values obtained by evaluating \(\varvec{E_{}}\). For instance, Open image in new window denotes the transaction obtained from Open image in new window by replacing the witness at index 1 with the signature \(\sigma \). Further, Open image in new window evaluates to the signature of the transaction represented by \(T_{}\), and Open image in new window represents the m-of-n multi-signature verification of the transaction represented by \(T_{}\). Both for the signing and verification, the parameter i represents the index where the signature will be used. We assume a simple type system (not specified here) that rules out ill-formed expressions, like e.g. Open image in new window .

We formalise the behaviour of a participant as an endpoint protocol, i.e. a process where the participant can perform the following actions: (i) send/receive messages to/from other participants; (ii) put a transaction on the ledger; (iii) wait until some transactions appear on the blockchain; (iv) do some internal computation. Note that the last kind of operation allows a participant to craft a transaction before putting it on the blockchain, e.g. setting the Open image in new window field to her signature, and later on adding the signature received from another participant.

Definition 2

(Endpoint protocols). Assume a set of participants (named Open image in new window , Open image in new window , Open image in new window , ...). We define prefixes Open image in new window , and protocols Open image in new window as follows:We assume that each name Open image in new window has a unique defining equation Open image in new window where the free variables in Open image in new window are included in Open image in new window . We use the following syntactic sugar:

The behaviour of protocols is defined in terms of a LTS between systems, i.e. the parallel composition of the protocols of all participants, and the blockchain.

Definition 3

(Semantics of protocols). A system Open image in new window is a term of the form Open image in new window , where (i) all the Open image in new window are distinct; (ii) there exists a single component Open image in new window , representing the current state of the blockchain Open image in new window , and the current time t; (iii) systems are up-to commutativity and associativity of Open image in new window . We define the relation \(\xrightarrow {}\) between systems in Fig. 4, where Open image in new window is the set of all the transactions in Open image in new window that are equal to Open image in new window , except for the witnesses. When writing Open image in new window we intend that the conditions above are respected.

Fig. 4.

Semantics of endpoint protocols.

Intuitively, a guarded choice Open image in new window can behave as one of the branches Open image in new window . A parallel composition Open image in new window executes concurrently Open image in new window and Open image in new window . All the rules (except the last two) specify how a protocol Open image in new window evolves within a system. Rule [Com] models a message exchange between Open image in new window and Open image in new window : participant Open image in new window sends messages \(\varvec{E_{}}\), which are received by Open image in new window on variables Open image in new window . Communication is synchronous, i.e. Open image in new window is blocked until Open image in new window is ready to receive. Rule [Check] allows the branch Open image in new window of a sum to proceed if the condition represented by \(E_{}\) is true. Rule [Put] allows Open image in new window to append a transaction to the blockchain, provided that the update is consistent. Rule [Ask] allows the branch Open image in new window of a sum to proceed only when the blockchain contains some transactions Open image in new window obtained by instantiating some \(\bot \) fields in \(\varvec{T_{}}\) (see Sect. 2). This form of pattern matching is crucial because the value of some fields (e.g., Open image in new window ), may not be known at the time the protocol is written. When the Open image in new window prefix unblocks, the variables Open image in new window in Open image in new window are bound to Open image in new window , so making it possible to inspect their actual fields. Rule [Def] allows a named process Open image in new window to evolve as Open image in new window , assuming a defining equation Open image in new window . The variables \(\varvec{x_{}}\) in Open image in new window are substituted with the results of the evaluation of \(\varvec{E_{}}\). Such defining equations can be used to specify recursive behaviours. Finally, rule [Delay] allows time to pass3.
Fig. 5.

Transactions of the naïve escrow contract.

Example 4

(Naïve escrow). A buyer Open image in new window wants to buy an item from the seller Open image in new window , but they do not trust each other. So, they would like to use a contract to ensure that Open image in new window will get paid if and only if Open image in new window gets her item. In a naïve attempt to realise this, they use the transactions in Fig. 5, where we assume that Open image in new window used in Open image in new window , is a transaction output redeemable by Open image in new window through her key Open image in new window . The transaction Open image in new window makes Open image in new window deposit Open image in new window , which can be redeemed by a transaction carrying the signatures of both  Open image in new window and  Open image in new window . The transactions Open image in new window and Open image in new window redeem Open image in new window , transferring the money to Open image in new window or Open image in new window , respectively.

The protocols of  Open image in new window and Open image in new window are, respectively, Open image in new window and Open image in new window :First, Open image in new window adds her signature to Open image in new window , and puts it on the blockchain. Then, she internally chooses whether to unblock the deposit for Open image in new window or to request a refund. In the first case, Open image in new window sends Open image in new window to Open image in new window . In the second case, she waits to receive the signature Open image in new window from Open image in new window (saving it in the variable \(x_{}\)); afterwards, she puts Open image in new window on the blockchain (after setting Open image in new window ) to redeem the deposit. The seller Open image in new window waits to see Open image in new window on the blockchain. Then, he chooses either to receive the signature Open image in new window from  Open image in new window (and then redeem the payment by putting Open image in new window on the blockchain), or to refund Open image in new window , by sending his signature Open image in new window .
This contract is not secure if either Open image in new window or Open image in new window are dishonest. On the one hand, a dishonest Open image in new window can prevent Open image in new window from redeeming the deposit, even if she had already received the item (to do that, it suffices not to send her signature, taking the rightmost branch in Open image in new window ). On the other hand, a dishonest Open image in new window can just avoid to send the item and the signature (taking the leftmost branch in Open image in new window ): in this way, the deposit gets frozen. For instance, let Open image in new window , where Open image in new window contains Open image in new window unredeemed. The scenario where Open image in new window has never received the item, while Open image in new window dishonestly attempts to receive the payment, is modelled as follows:
At this point the computation is stuck, because both Open image in new window and Open image in new window are waiting a message from the other participant. We will show in Sect. 4.3 how to design a secure escrow contract, with the intermediation of a trusted arbiter.

4 A Survey of Smart Contracts on Bitcoin

We now present a comprehensive survey of smart contracts on Bitcoin, comprising those published in the academic literature, and those found online. To this aim we exploit the model of computation introduced in Sect. 3. Remarkably, all the following contracts can be implemented by only using so-called standard transactions4, e.g. via the compilation technique in [11]. This is crucial, because non-standard transactions are currently discarded by the Bitcoin network.

4.1 Oracle

In many concrete scenarios one would like to make the execution of a contract depend on some real-world events, e.g. results of football matches for a betting contract, or feeds of flight delays for an insurance contract. However, the evaluation of Bitcoin scripts can not depend on the environment, so in these scenarios one has to resort to a trusted third-party, or oracle [2, 19], who notifies real-world events by providing signatures on certain transactions.
Fig. 6.

Transactions of a contract relying on an oracle.

For example, assume that Open image in new window wants to transfer Open image in new window to Open image in new window only if a certain event, notified by an oracle Open image in new window , happens. To do that, Open image in new window puts on the blockchain the transaction Open image in new window in Fig. 6, which can be redeemed by a transactions carrying the signatures of both  Open image in new window and  Open image in new window . Further, Open image in new window instructs the oracle to provide his signature to Open image in new window upon the occurrence of the expected event.

We model the behaviour of Open image in new window as the following protocol:Here, Open image in new window waits to receive the signature Open image in new window from Open image in new window , then he puts Open image in new window on the blockchain (after setting its Open image in new window ) to redeem Open image in new window . In practice, oracles like the one needed in this contract are available as services in the Bitcoin ecosystem5.

Notice that, in case the event certified by the oracle never happens, the Open image in new window within Open image in new window are frozen forever. To avoid this situation, one can add a time constraint to the output script of Open image in new window , e.g. as in the transaction Open image in new window in Fig. 10.

4.2 Crowdfunding

Assume that the curator Open image in new window of a crowdfunding campaign wants to fund a venture Open image in new window by collecting Open image in new window from a set Open image in new window of investors. The investors want to be guaranteed that either the required amount Open image in new window is reached, or they will be able to redeem their funds. To this purpose, Open image in new window can employ the following contract. She starts with a canonical transaction Open image in new window (with empty Open image in new window field) which has a single output of Open image in new window to be redeemed by Open image in new window . Intuitively, each Open image in new window can invest money in the campaign by “filling in” the Open image in new window field of the Open image in new window with a transaction output under their control. To do this, Open image in new window sends to Open image in new window a transaction output Open image in new window , together with the signature \(\sigma _i\) required to redeem it. We denote with Open image in new window the value of such output. Notice that, since the signature \(\sigma _i\) has been made on Open image in new window , the only valid output is the one of Open image in new window to be redeemed by Open image in new window . Upon the reception of the message from Open image in new window , Open image in new window updates Open image in new window : the provided output is appended to the Open image in new window field, and the signature is added to the corresponding Open image in new window field. If all the outputs Open image in new window are distinct (and not redeemed) and the signatures are valid, when Open image in new window the filled transaction Open image in new window can be put on the blockchain. If Open image in new window collects Open image in new window , the difference \(v'_{}- v_{}\) goes to the miners as transaction fee.

The endpoint protocol of the curator is defined as Open image in new window , where:while the protocol of each investor Open image in new window is the following:Note that the transactions sent by investors are not known a priori, so they cannot just create the final transaction and sign it. Instead, to allow Open image in new window to complete the transaction Open image in new window without invalidating the signatures, they compute them using the modifier Open image in new window . In this way, only a single input is signed, and when verifying the corresponding signature, the others are neglected.

4.3 Escrow

In Example 4 we have discussed a naïve escrow contract, which is secure only if both the buyer Open image in new window and the seller Open image in new window are honest (so making the contract pointless). Rather, one would like to guarantee that, even if either Open image in new window or Open image in new window (or both) are dishonest, exactly one them will be able to redeem the money: in case they disagree, a trusted participant Open image in new window , who plays the role of arbiter, will decide who gets the money (possibly splitting the initial deposit in two parts) [1, 19].
Fig. 7.

Transactions of the escrow contract.

The output script of the transaction Open image in new window in Fig. 7 is a 2-of-3 multi-signature schema. This means that Open image in new window can be redeemed either with the signatures Open image in new window and Open image in new window (in case they agree), or with the signature of Open image in new window (with key Open image in new window ) and the signature of Open image in new window or that of Open image in new window (in case they disagree). The transaction Open image in new window in Fig. 7 allows the arbiter to issue a partial refund of Open image in new window to Open image in new window , and of Open image in new window to Open image in new window . Instead, to issue a full refund to either Open image in new window or Open image in new window , the arbiter signs, respectively, the transactions Open image in new window or Open image in new window (not shown in the figure). The protocols of Open image in new window and Open image in new window are similar to those in Example 4, except for the part where they ask Open image in new window for an arbitration:In the summation within Open image in new window , participant Open image in new window internally chooses whether to send her signature to Open image in new window (so allowing Open image in new window to redeem Open image in new window via Open image in new window ), or to proceed with Open image in new window . There, Open image in new window waits to receive either Open image in new window ’s signature (which allows Open image in new window to redeem Open image in new window by putting Open image in new window on the blockchain), or a response from the arbiter, in the process Open image in new window . The three cases in the summation of Open image in new window in Open image in new window correspond, respectively, to the case where Open image in new window gets a full refund (\(z_{}=1\)), a partial refund (\(0< z_{}< 1\)), or no refund at all (\(z_{}=0\)).
The protocol for Open image in new window is dual to that of Open image in new window :If an arbitration is requested, Open image in new window internally decides (through the \(\tau \) actions) who between Open image in new window and Open image in new window can redeem the deposit in Open image in new window , by sending its signature to one of the two participants, or decide for a partial refund of \(z_{}\) and \(1 - z_{}\) bitcoins, respectively, to Open image in new window and Open image in new window , by sending its signature on Open image in new window to both participants:Note that, in the unlikely case where both Open image in new window and Open image in new window choose to send their signature to the other participant, the Open image in new window deposit becomes “frozen”. In a more concrete version of this contract, a participant could keep listening for the signature, and attempt to redeem the deposit when (unexpectedly) receiving it.
Fig. 8.

Transactions of the intermediated payment contract.

4.4 Intermediated Payment

Assume that Open image in new window wants to send an indirect payment of Open image in new window to Open image in new window , routing it through an intermediary  Open image in new window who retains a fee of Open image in new window bitcoins. Since Open image in new window does not trust Open image in new window , she wants to use a contract to guarantee that: (i) if Open image in new window is honest, then Open image in new window are transferred to Open image in new window ; (ii) if Open image in new window is not honest, then Open image in new window does not lose money. The contract uses the transactions in Fig. 8: Open image in new window transfers Open image in new window from Open image in new window to Open image in new window , and Open image in new window splits the amount to Open image in new window ( Open image in new window ) and to Open image in new window ( Open image in new window ). We assume that Open image in new window is a transaction output redeemable by Open image in new window . The behaviour of Open image in new window is as follows:Here, Open image in new window receives from Open image in new window his signature on Open image in new window , which makes it possible to pay Open image in new window later on. The \(\tau \) branch and the \(\mathsf {else}\) branch ensure that Open image in new window will correctly terminate also if Open image in new window is dishonest (i.e., Open image in new window does not send anything, or he sends an invalid signature). If Open image in new window receives a valid signature, she puts Open image in new window on the blockchain, adding her signature to the Open image in new window field. Then, she also appends Open image in new window , adding to the Open image in new window field her signature and Open image in new window ’s one. Since Open image in new window takes care of publishing both transactions, the behaviour of Open image in new window consists just in sending his signature on Open image in new window . Therefore, Open image in new window ’s protocol can just be modelled as Open image in new window .

This contract relies on SegWit. In Bitcoin without SegWit, the identifier of Open image in new window is affected by the instantiation of the Open image in new window field. So, when Open image in new window is put on the blockchain, the input in Open image in new window (which was computed before) does not point to it.

4.5 Timed Commitment

Assume that Open image in new window wants to choose a secret \(s_{}^{}\), and reveal it after some time—while guaranteeing that the revealed value corresponds to the chosen secret (or paying a penalty otherwise). This can be obtained through a timed commitment [20], a protocol with applications e.g. in gambling games [25, 28, 42], where the secret contains the player move, and the delay in the revelation of the secret is intended to prevent other players from altering the outcome of the game. Here we formalise the version of the timed commitment protocol presented in [8].
Fig. 9.

Transactions of the timed commitment.

Intuitively, Open image in new window starts by exposing the hash of the secret, i.e. Open image in new window , and at the same time depositing some amount Open image in new window in a transaction. The participant Open image in new window has the guarantee that after t time units, he will either know the secret \(s_{}^{}\), or he will be able to redeem Open image in new window .

The transactions of the protocol are shown in Fig. 9, where we assume that Open image in new window is a transaction output redeemable by Open image in new window . The behaviour of Open image in new window is modelled as the following protocol:Participant Open image in new window starts by putting the transaction Open image in new window on the blockchain. Note that within this transaction Open image in new window is committing the hash of the chosen secret: indeed, \(h_{}^{}\) is encoded within the output script Open image in new window . Then, Open image in new window sends to Open image in new window her signature on Open image in new window . Note that this transaction can be redeemed by  Open image in new window only when \(t_{}\) time units have passed since Open image in new window has been published on the blockchain, because of the relative timelock declared in  Open image in new window . After sending her signature on  Open image in new window , Open image in new window internally chooses whether to reveal the secret, or do nothing (via the \(\tau \) actions). In the first case, Open image in new window must put the transaction Open image in new window on the blockchain. Since it redeems Open image in new window , she needs to write in Open image in new window both the secret \(s_{}^{}\) and her signature, so making the former public.
A possible behaviour of the receiver Open image in new window is the following:In this protocol, Open image in new window first receives from Open image in new window (and saves in \(x_{}\)) her signature on the transaction Open image in new window . Then, Open image in new window checks if the signature is valid: if not, he aborts the protocol. Even if the signature is valid, Open image in new window cannot put Open image in new window on the blockchain and redeem the deposit immediately, since the transaction has a timelock \(t_{}\). Note that Open image in new window cannot change the timelock: indeed, doing so would invalidate Open image in new window ’s signature on  Open image in new window . If, after \(t_{}\) time units, Open image in new window has not published Open image in new window yet, Open image in new window can proceed to put Open image in new window on the blockchain, writing Open image in new window ’s and his own signatures in the witness. Otherwise, Open image in new window retrieves Open image in new window from the blockchain, from which he can obtain the secret, and use it in Open image in new window .
A variant of this contract, which implements the timeout in Open image in new window , and does not require the signature exchange, is used in Sect. 4.7.
Fig. 10.

Transactions of the micropayment channel contract.

4.6 Micropayment Channels

Assume that Open image in new window wants to make a series of micropayments to Open image in new window , e.g. a small fraction of Open image in new window every few minutes. Doing so with one transaction per payment would result in conspicuous fees6, so Open image in new window and Open image in new window use a micropayment channel contract [29]. Open image in new window starts by depositing Open image in new window ; then, she signs a transaction that pays Open image in new window to Open image in new window and Open image in new window back to herself, and she sends that transaction to Open image in new window . Participant Open image in new window can choose to publish that transaction immediately and redeem its payment, or to wait in case Open image in new window sends another transaction with increased value. Open image in new window can stop sending signatures at any time. If Open image in new window redeems, then Open image in new window can get back the remaining amount. If Open image in new window does not cooperate, Open image in new window can redeem all the amount after a timeout.

The protocol of Open image in new window is the following (the transactions are in Fig. 10). Open image in new window publishes the transaction Open image in new window , depositing Open image in new window that can be spent with her signature and that of Open image in new window , or with her signature alone, after time \(t_{}\). Open image in new window can redeem the deposit by publishing the transaction Open image in new window . To pay for the service, Open image in new window sends to Open image in new window the amount v she is paying, and her signature on Open image in new window . Then, she can decide to increase v and recur, or to terminate.The participant Open image in new window waits for Open image in new window to appear on the blockchain, then receives the first value \(v_{}\) and Open image in new window ’s signature \(\sigma \). Then, Open image in new window checks if \(\sigma \) is valid, otherwise he aborts the protocol. At this point, Open image in new window waits for another pair \((v',\sigma ')\), or, after a timeout, he redeems Open image in new window using Open image in new window .Note that Open image in new window should redeem Open image in new window before the timeout expires, which is not modelled in  Open image in new window . This could be obtained by enriching the calculus with time-constraining operators (see Footnote 3).

4.7 Fair Lotteries

A multiparty lottery is a protocol where N players put their bets in a pot, and a winner—uniformly chosen among the players—redeems the whole pot. Various contracts for multiparty lotteries on Bitcoin have been proposed in [8, 9, 12, 14, 16, 36]. These contracts enjoy a fairness property, which roughly guarantees that: (i) each honest player will have (on average) a non-negative payoff, even in the presence of adversaries; (ii) when all the players are honest, the protocol behaves as an ideal lottery: one player wins the whole pot (with probability Open image in new window ), while all the others lose their bets (with probability Open image in new window ).

Here we illustrate the lottery in [8], for \(N=2\). Consider two players Open image in new window and Open image in new window who want to bet Open image in new window each. Their protocol is composed of two phases. The first phase is a timed commitment (as in Sect. 4.5): each player chooses a secret ( Open image in new window and Open image in new window ) and commits its hash ( Open image in new window and Open image in new window ). In doing that, both players put a deposit of Open image in new window on the ledger, which is used to compensate the other player in case one chooses not to reveal the secret later on. In the second phase, the two bets are put on the ledger. After that, the players reveal their secrets, and redeem their deposits. Then, the secrets are used to compute the winner of the lottery in a fair manner. Finally, the winner redeems the bets.
Fig. 11.

Transactions of the fair lottery with deposit.

The transactions needed for this lottery are displayed in Fig. 11 (we only show Open image in new window ’s transactions, as those of Open image in new window are similar). The transactions for the commitment phase ( Open image in new window ) are similar to those in Sect. 4.5: they only differ in the script of Open image in new window , which now also checks that the length of the secret is either 128 or 129. This check forces the players to choose their secret so that it has one of these lengths, and reveal it (using Open image in new window ) before the Open image in new window deadline, since otherwise they will lose their deposits (enabling Open image in new window ).

The bets are put using Open image in new window , whose output script computes the winner using the secrets, which can then be revealed. For this, the secret lengths are compared: if equal, Open image in new window wins, otherwise Open image in new window wins. In this way, the lottery is equivalent to a coin toss. Note that, if a malicious player chooses a secret having another length than 128 or 129, the Open image in new window transaction will become stuck, but its opponent will be compensated using the deposit.

The endpoint protocol Open image in new window of player Open image in new window follows (the one for Open image in new window is similar):Player Open image in new window starts by putting Open image in new window on the blockchain, then she waits for Open image in new window doing the same. If Open image in new window does not cooperate, Open image in new window can safely abort the protocol taking its Open image in new window branch, so redeeming her deposit with Open image in new window (as usual, here with \(\tau \) we are modelling a timeout). If Open image in new window commits his secret, Open image in new window executes Open image in new window , extracting the hash Open image in new window of Open image in new window ’s secret, and checking whether it is distinct from Open image in new window . If the hashes are found to be equal, Open image in new window aborts the protocol using Open image in new window . Otherwise, Open image in new window runs Open image in new window . The Open image in new window component attempts to redeem Open image in new window ’s deposit, as soon as the Open image in new window deadline of Open image in new window expires, forcing Open image in new window to timely reveal his secret. Instead, Open image in new window proceeds with the lottery, asking Open image in new window for his signature of Open image in new window . If Open image in new window does not sign, Open image in new window aborts using Open image in new window . Then, Open image in new window runs Open image in new window , finally putting the bets ( Open image in new window ) on the ledger. If this is not possible (e.g., because one of the Open image in new window is already spent), Open image in new window aborts using Open image in new window . After Open image in new window is on the ledger, Open image in new window reveals her secret and redeems her deposit with Open image in new window . In parallel, with Open image in new window she waits for the secret of Open image in new window to be revealed, and then attempts to redeem the pot ( Open image in new window ).

The fairness of this lottery has been established in [8]. This protocol can be generalised to \(N>2\) players [8, 9] but in this case the deposit grows quadratically with N. The works [14, 36] have proposed fair multiparty lotteries that require, respectively, zero and constant (\(\ge 0\)) deposit. More precisely, [36] devises two variants of the protocol: the first one only relies on SegWit, but requires each player to statically sign \(O(2^N)\) transactions; the second variant reduces the number of signatures to \(O(N^2)\), at the cost of introducing a custom opcode. Also the protocol in [14] assumes an extension of Bitcoin, i.e. the malleability of in fields, to obtain an ideal fair lottery with O(N) signatures per player (see Sect. 5).

4.8 Contingent Payments

Assume a participant Open image in new window who wants to pay Open image in new window to receive a value s which makes a public predicate p true, where p(s) can be verified efficiently. A seller Open image in new window who knows such s is willing to reveal it to Open image in new window , but only under the guarantee that he will be paid Open image in new window . Similarly, the buyer wants to pay only if guaranteed to obtain s.

A naïve attempt to implement this contract in Bitcoin is the following: Open image in new window creates a transaction Open image in new window such that Open image in new window evaluates to true if and only if \(p(x_{})\) holds and \(\varsigma _{}\) is a signature of Open image in new window . Hence, Open image in new window can redeem Open image in new window from Open image in new window by revealing s. In practice, though, this approach is arguably useful, since it requires coding p in the Bitcoin scripting language, whose expressiveness is quite limited.

More general contingent payment contracts can be obtained by exploiting zero-knowledge proofs [13, 24, 35]. In this setting, the seller generates a fresh key k, and sends to the buyer the encryption \(e_s = E_k(s)\), together with the hash Open image in new window , and a zero-knowledge proof guaranteeing that such messages have the intended form. After verifying this proof, Open image in new window is sure that Open image in new window knows a preimage \(k'\) of \(h_k\) (by collision resistance, \(k'=k\)) such that \(D_{k'}(e_s)\) satisfies the predicate p, and so she can buy the preimage k of \(h_k\) with the naïve protocol, so obtaining the solution s by decrypting \(e_s\) with k.
Fig. 12.

Transactions of the contingent payment.

The transactions implementing this contract are displayed in Fig. 12. The Open image in new window clause in Open image in new window allows Open image in new window to redeem Open image in new window if no solution is provided by the deadline \(t_{}\). The behaviour of the buyer Open image in new window can be modelled as follows:Upon receiving \(e_s\), \(h_k\) and the proof \(z_{}\)7 the buyer verifies \(z_{}\). If the verification succeeds, Open image in new window puts Open image in new window on the blockchain. Then, she waits for Open image in new window , from which she can retrieve the key k, and so use the solution \(D_{\textit{get}_{k}(x_{})}(e_s)\) in Open image in new window . In this way, Open image in new window can redeem Open image in new window . If Open image in new window does not put Open image in new window , after \(t_{}\) time units Open image in new window can get her deposit back through Open image in new window . The protocol of Open image in new window is simple, so it is omitted.

5 Research Challenges and Perspectives

Extensions to Bitcoin. The formal model of smart contracts we have proposed is based on the current mechanisms of Bitcoin; indeed, this makes it possible to translate endpoint protocols into actual implementations interacting with the Bitcoin blockchain. However, constraining smart contracts to perfectly adhere to Bitcoin greatly reduces their expressiveness. Indeed, the Bitcoin scripting language features a very limited set of operations8, and over the years many useful (and apparently harmless) opcodes have been disabled without a clear understanding of their alleged insecurity9. This is the case e.g., of bitwise logic operators, shift operators, integer multiplication, division and modulus.

For this reason some developers proposed to re-enable some disabled opcodes10, and some works in the literature proposed extensions to the Bitcoin scripting language so to enhance the expressiveness of smart contracts.

A possible extension is covenants [37], a mechanism that allows an output script to constrain the structure of the redeeming transaction. This is obtained through a new opcode, called CHECKOUTPUTVERIFY, which checks if a given Open image in new window of the redeeming transaction matches a specific pattern. Covenants are also studied in [41], where they are implemented using the opcode CAT (currently disabled) and a new opcode CHECKSIGFROMSTACK which verifies a signature against an arbitrary bitstring on the stack. In both works, covenants can also be recursive, e.g. a covenant can check if the redeeming transaction contains itself. Using recursive covenants allows to implement a state machine through a sequence of transactions that store its state.

Secure cash distribution with penalties [8, 16, 32] is a cryptographic primitive which allows a set of participants to make a deposit, and then provide inputs to a function whose evaluation determines how the deposits are distributed among the participants. This primitive guarantees that dishonest participants (who, e.g., abort the protocol after learning the value of the function) will pay a penalty to the honest participants. This primitive does not seem to be directly implementable in Bitcoin, but it becomes so by extending the scripting language with the opcode CHECKSIGFROMSTACK discussed above. Secure cash distribution with penalties can be instantiated to a variety of smart contracts, e.g. lotteries [8] poker [32], and contingent payments. The latter smart contract can also be obtained through the opcode CHECKKEYPAIRVERIFY in [24], which checks if the two top elements of the stack are a valid key pair.

Another new opcode, called MULTIINPUT [36] consumes from the stack a signature \(\sigma \) and a sequence of Open image in new window values Open image in new window , with the following two effects: (i) it verifies the signature \(\sigma \) against the redeeming transaction Open image in new window , neglecting Open image in new window ; (ii) it requires Open image in new window to be equal to some of the Open image in new window . Exploiting this opcode, [36] devise a fair N-party lottery which requires zero deposit, and \(O(N^2)\) off-chain signed transaction. The first one of these effects can be alternatively obtained by extending, instead of the scripting language, the signature modifiers. More specifically, [14] introduces a new signature modifier, which can set to \(\bot \) all the inputs of a transaction (i.e., no input is signed). In this way they obtain a fair multi-party lottery with similar properties to the one in [36].

Another way improve the expressiveness of smart contracts is to replace the Bitcoin scripting language, e.g. with the one in [40]. This would also allow to establish bounds on the computational resources needed to run scripts.

Unfortunately, none of the proposed extensions has been yet included in the main branch of the Bitcoin Core client, and nothing suggests that they will be considered in the near future. Indeed, the development of Bitcoin is extremely conservative, as any change to its protocol requires an overwhelming consensus of the miners. So far, new opcodes can only be empirically assessed through the Elements alpha project11, a testnet for experimenting new Bitcoin features. A significant research challenge would be that of formally proving that new opcodes do not introduce vulnerabilities, exploitable e.g. by Denial-of-Service attacks. For instance, unconstrained uses of the opcode CAT may cause an exponential space blow-up in the verification of transactions.

Formal Methods for Bitcoin Smart Contracts. As witnessed in Sect. 4, designing secure smart contracts on Bitcoin is an error-prone task, similarly to designing secure cryptographic protocols. The reason lies in the fact that, to devise a secure contract, a designer has to anticipate any possible (mis-)behaviour of the other participants. The side effect is that endpoint protocols may be quite convoluted, as they must include compensations at all the points where something can go wrong. Therefore, tools to automate the analysis and verification of smart contracts may be of great help.

Recent works [7] propose to verify Bitcoin smart contracts by modelling the behaviour of participants as timed automata, and then using UPPAAL [15] to check properties against an attacker. This approach correctly captures the time constraints within the contracts. The downside is that encoding this UPPAAL model into an actual implementation with Bitcoin transactions is a complex task. Indeed, a designer without a deep knowledge of Bitcoin technicalities is likely to produce an UPPAAL model that can not be encoded in Bitcoin. A relevant research challenge is to study specification languages for Bitcoin contracts (like e.g. the one in Sect. 3), and techniques to automatically encode them in a model that can be verified by a model checker.

Remarkably, the verification of security properties of smart contracts requires to deal with non-trivial aspects, like temporal constraints and probabilities. This is the case, e.g., for the verification of fairness of lotteries (like e.g. the one discussed in Sect. 4.7); a further problem is that fairness must hold against any adversarial strategy. It is not clear whether in this case it is sufficient to consider a “most powerful” adversary, like e.g. in the symbolic Dolev-Yao model. In case a contract is not secure against arbitrary (PTIME) adversaries, one would like to verify that, at least, it is secure against rational ones [27], which is a relevant research issue. Additional issues arise when considering more concrete models of the Bitcoin blockchain, respect to the one in Sect. 2. This would require to model forks, i.e. the possibility that a recent transaction is removed from the blockchain. This could happen with rational (but dishonest) miners [33].

DSLs for Smart Contracts. As witnessed in Sect. 4, modelling Bitcoin smart contracts is complex and error-prone. A possible way to address this complexity is to devise high-level domain-specific languages (DSLs) for contracts, to be compiled in low-level protocols (e.g., the ones in Sect. 3). Indeed, the recent proliferation of non-Turing complete DSLs for smart contracts [18, 22, 26] suggests that this is an emerging research direction.

A first proposal of an high-level language implemented on top of Bitcoin is Typecoin [23]. This language allows to model the updates of a state machine as affine logic propositions. Users can “run” this machine by putting transactions on the Bitcoin blockchain. The security of the blockchain guarantees that only the legit updates of the machine can be triggered by users. A downside of this approach is that liveness is guaranteed only by assuming cooperation among the participants, i.e., a dishonest participant can make the others unable to complete an execution. Note instead that the smart contracts in Sect. 4 allow honest participants to terminate, regardless of the behaviours of the environment. In some cases, e.g. in the lottery in Sect. 4.7, abandoning the contract may even result in penalties (i.e., loss of the deposit paid upfront to stipulate the contract).

Footnotes

  1. 1.

    Actually, the signature is not computed on the whole redeeming transaction, but only on a part of it, as shown in Sect. 2.3.

  2. 2.

    The difference between the amount of inputs and that of outputs is the fee paid to the miner who publishes the transaction.

  3. 3.

    To keep our presentation simple, we have not included time-constraining operators in endpoint protocols. In case one needs a finer-grained control of time, well-known techniques [39] exist to extend a process algebra like ours with these operators.

  4. 4.
  5. 5.
  6. 6.
  7. 7.

    For simplicity, here we model the zero-knowledge proof as a single message. More concretely, it should be modelled as a sub-protocol.

  8. 8.
  9. 9.
  10. 10.
  11. 11.

Notes

Acknowledgments

This work is partially supported by Aut. Reg. of Sardinia project P.I.A. 2013 “NOMAD”. Stefano Lande gratefully acknowledges Sardinia Regional Government for the financial support of his PhD scholarship (P.O.R. Sardegna F.S.E. Operational Programme of the Autonomous Region of Sardinia, European Social Fund 2014–2020).

References

  1. 1.
    Bitcoin developer guide - escrow and arbitration. https://goo.gl/8XL5Fn
  2. 2.
    Bitcoin wiki - contracts - using external state. https://en.bitcoin.it/wiki/Contract#Example_4:_Using_external_state
  3. 3.
    Understanding the DAO attack, June 2016. http://www.coindesk.com/understanding-dao-hack-journalists/
  4. 4.
    Parity Wallet security alert, July 2017. https://paritytech.io/blog/security-alert.html
  5. 5.
    A Postmortem on the Parity Multi-Sig library self-destruct, November 2017. https://goo.gl/Kw3gXi
  6. 6.
    Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, Ł.: Fair two-party computations via Bitcoin deposits. In: Böhme, R., Brenner, M., Moore, T., Smith, M. (eds.) FC 2014. LNCS, vol. 8438, pp. 105–121. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44774-1_8CrossRefGoogle Scholar
  7. 7.
    Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, Ł.: Modeling Bitcoin contracts by timed automata. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 7–22. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-10512-3_2CrossRefzbMATHGoogle Scholar
  8. 8.
    Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, L.: Secure multiparty computations on Bitcoin. In: IEEE Symposium on Security and Privacy, pp. 443–458 (2014)Google Scholar
  9. 9.
    Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, L.: Secure multiparty computations on Bitcoin. Commun. ACM 59(4), 76–84 (2016)CrossRefGoogle Scholar
  10. 10.
    Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164–186. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54455-6_8CrossRefGoogle Scholar
  11. 11.
    Atzei, N., Bartoletti, M., Lande, S., Zunino, R.: A formal model of Bitcoin transactions. In: Financial Cryptography and Data Security. LNCS, Springer (2018)Google Scholar
  12. 12.
    Back, A., Bentov, I.: Note on fair coin toss via Bitcoin (2013). http://www.cs.technion.ac.il/~idddo/cointossBitcoin.pdf
  13. 13.
    Banasik, W., Dziembowski, S., Malinowski, D.: Efficient zero-knowledge contingent payments in cryptocurrencies without scripts. In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016, Part II. LNCS, vol. 9879, pp. 261–280. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-45741-3_14CrossRefGoogle Scholar
  14. 14.
    Bartoletti, M., Zunino, R.: Constant-deposit multiparty lotteries on Bitcoin. In: Brenner, M., Rohloff, K., Bonneau, J., Miller, A., Ryan, P.Y.A., Teague, V., Bracciali, A., Sala, M., Pintore, F., Jakobsson, M. (eds.) FC 2017. LNCS, vol. 10323, pp. 231–247. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-70278-0_15CrossRefGoogle Scholar
  15. 15.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-30080-9_7CrossRefGoogle Scholar
  16. 16.
    Bentov, I., Kumaresan, R.: How to use Bitcoin to design fair protocols. In: Garay, J.A., Gennaro, R. (eds.) CRYPTO 2014, Part II. LNCS, vol. 8617, pp. 421–439. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44381-1_24CrossRefGoogle Scholar
  17. 17.
    Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., Rastogi, A., Sibut-Pinote, T., Swamy, N., Zanella-Beguelin, S.: Formal verification of smart contracts. In: PLAS (2016)Google Scholar
  18. 18.
    Biryukov, A., Khovratovich, D., Tikhomirov, S.: Findel: secure derivative contracts for ethereum. In: Brenner, M., Rohloff, K., Bonneau, J., Miller, A., Ryan, P.Y.A., Teague, V., Bracciali, A., Sala, M., Pintore, F., Jakobsson, M. (eds.) FC 2017. LNCS, vol. 10323, pp. 453–467. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-70278-0_28CrossRefGoogle Scholar
  19. 19.
    BitFury group: Smart contracts on Bitcoin blockchain (2015). http://bitfury.com/content/5-white-papers-research/contracts-1.1.1.pdf
  20. 20.
    Boneh, D., Naor, M.: Timed commitments. In: Bellare, M. (ed.) CRYPTO 2000. LNCS, vol. 1880, pp. 236–254. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-44598-6_15CrossRefGoogle Scholar
  21. 21.
    Bonneau, J., Miller, A., Clark, J., Narayanan, A., Kroll, J.A., Felten, E.W.: SoK: research perspectives and challenges for Bitcoin and cryptocurrencies. In: IEEE S & P, pp. 104–121 (2015)Google Scholar
  22. 22.
    Brown, R.G., Carlyle, J., Grigg, I., Hearn, M.: Corda: an introduction (2016). http://r3cev.com/s/corda-introductory-whitepaper-final.pdf
  23. 23.
    Crary, K., Sullivan, M.J.: Peer-to-peer affine commitment using Bitcoin. In: ACM Conference on Programming Language Design and Implementation, pp. 479–488 (2015)CrossRefGoogle Scholar
  24. 24.
    Delgado-Segura, S. et al.: A fair protocol for data trading based on Bitcoin transactions. In: Future Generation Computer Systems (2017, in press). http://dx.doi.org/10.1016/j.future.2017.08.021
  25. 25.
    Delmolino, K., Arnett, M., Kosba, A., Miller, A., Shi, E.: Step by step towards creating a safe smart contract: lessons and insights from a cryptocurrency lab. In: Clark, J., Meiklejohn, S., Ryan, P.Y.A., Wallach, D., Brenner, M., Rohloff, K. (eds.) FC 2016. LNCS, vol. 9604, pp. 79–94. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-53357-4_6CrossRefGoogle Scholar
  26. 26.
    Frantz, C.K., Nowostawski, M.: From institutions to code: towards automated generation of smart contracts. In: eCAS Workshop (2016)Google Scholar
  27. 27.
    Garay, J.A., Katz, J., Maurer, U., Tackmann, B., Zikas, V.: Rational protocol design: cryptography against incentive-driven adversaries. In: FOCS, pp. 648–657 (2013)Google Scholar
  28. 28.
    Goldschlag, D.M., Stubblebine, S.G., Syverson, P.F.: Temporarily hidden bit commitment and lottery applications. Int. J. Inf. Secur. 9(1), 33–50 (2010)CrossRefGoogle Scholar
  29. 29.
    Hearn, M.: Rapidly-adjusted (micro) payments to a pre-determined party (2013). https://bitcointalk.org
  30. 30.
    Hirai, Y.: Defining the ethereum virtual machine for interactive theorem provers. In: Brenner, M., Rohloff, K., Bonneau, J., Miller, A., Ryan, P.Y.A., Teague, V., Bracciali, A., Sala, M., Pintore, F., Jakobsson, M. (eds.) FC 2017. LNCS, vol. 10323, pp. 520–535. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-70278-0_33CrossRefGoogle Scholar
  31. 31.
    Kumaresan, R., Bentov, I.: How to use Bitcoin to incentivize correct computations. In: ACM CCS, pp. 30–41 (2014)Google Scholar
  32. 32.
    Kumaresan, R., Moran, T., Bentov, I.: How to use Bitcoin to play decentralized poker. In: ACM CCS, pp. 195–206 (2015)Google Scholar
  33. 33.
    Liao, K., Katz, J.: Incentivizing blockchain forks via whale transactions. In: Brenner, M., Rohloff, K., Bonneau, J., Miller, A., Ryan, P.Y.A., Teague, V., Bracciali, A., Sala, M., Pintore, F., Jakobsson, M. (eds.) FC 2017. LNCS, vol. 10323, pp. 264–279. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-70278-0_17CrossRefGoogle Scholar
  34. 34.
    Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: ACM CCS (2016). http://eprint.iacr.org/2016/633
  35. 35.
    Maxwell, G.: The first successful zero-knowledge contingent payment (2016). https://bitcoincore.org/en/2016/02/26/zero-knowledge-contingent-payments-announcement/
  36. 36.
    Miller, A., Bentov, I.: Zero-collateral lotteries in Bitcoin and Ethereum. In: EuroS&P Workshops, pp. 4–13 (2017)Google Scholar
  37. 37.
    Möser, M., Eyal, I., Gün Sirer, E.: Bitcoin covenants. In: Clark, J., Meiklejohn, S., Ryan, P.Y.A., Wallach, D., Brenner, M., Rohloff, K. (eds.) FC 2016. LNCS, vol. 9604, pp. 126–141. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-53357-4_9CrossRefGoogle Scholar
  38. 38.
    Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). https://bitcoin.org/bitcoin.pdf
  39. 39.
    Nicollin, X., Sifakis, J.: An overview and synthesis on timed process algebras. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 376–398. Springer, Heidelberg (1992).  https://doi.org/10.1007/3-540-55179-4_36CrossRefGoogle Scholar
  40. 40.
    O’Connor, R.: Simplicity: a new language for blockchains. In: PLAS (2017). http://arxiv.org/abs/1711.03028
  41. 41.
    O’Connor, R., Piekarska, M.: Enhancing Bitcoin transactions with covenants. In: Brenner, M., Rohloff, K., Bonneau, J., Miller, A., Ryan, P.Y.A., Teague, V., Bracciali, A., Sala, M., Pintore, F., Jakobsson, M. (eds.) FC 2017. LNCS, vol. 10323, pp. 191–198. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-70278-0_12CrossRefGoogle Scholar
  42. 42.
    Syverson, P.F.: Weakly secret bit commitment: applications to lotteries and fair exchange. In: IEEE CSFW, pp. 2–13 (1998)Google Scholar
  43. 43.
    Szabo, N.: Formalizing and securing relationships on public networks. First Monday 2(9) (1997). http://firstmonday.org/htbin/cgiwrap/bin/ojs/index.php/fm/article/view/548

Copyright information

© The Author(s) 2018

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  1. 1.Università degli Studi di CagliariCagliariItaly
  2. 2.Università degli Studi di TrentoTrentoItaly

Personalised recommendations