Skip to content

BitML

Implementing Bitcoin contracts directly as Bitcoin transactions is tedious and error prone.

Verification is ad-hoc for each contract

BitML (Bitcoin Modelling Language) addresses the issues:

  • Higher level of abstraction w.r.t. Bitcoin transactions.
  • Formal language with precise semantics, simplifies verification.
  • Can be complied to standard Bitcoin transactions.
  • Computational soundness: attacks in the computational model can also be observed in the symbolic model, with overwhelming probability.

Workflow

Advertisement: The contract and the required preconditions (deposits and secrets) are broadcasted.

Stipulation: participants may accept the contract if they satisfy the preconditions.

Execution: participants perform actions following the contract.

A contract advertisement is: \(\{G\}C\), where

  • \(G\) is the precondition
  • \(C\) is the contract

Preconditions

Contract preconditions in formal language:

\(G::=A:?v@x\), volatile deposit of \(v\) ₿, expected from \(A\).

\(G::=A:!v@x\), persistent deposit of \(v\), ₿expected from \(A\).

\(G::=secret\ a\): committed secret by \(A\).

\(G::=G|G\), composition

  • Persistent deposits are transferred to the contract as soon as the contract starts
  • Volatile ones may be transferred when the contract demands them, if they are not already spent.
  • Secrets needs to be committed before the contract starts, therefore they are included in the set of preconditions.

Configurations

\(\Gamma::=0\), empty

\(\Gamma::=\{G\}C\), contract advertisement

\(\Gamma::=\langle C,v\rangle_x\), an active contract containing \(v\) ₿

\(\Gamma::=\langle A,v\rangle_x\), a deposit of \(v\) ₿ redeemable by \(A\)

\(\Gamma::=A[\chi]\), authorization of \(A\) to perform \(\chi\).

\(\Gamma::=\{A:a\#N\}\), committed secret of \(A\) (\(N\in\mathbb N\cup\{\bot\}\))

\(\Gamma::=A:a\#N\), revealed secret of \(A\) (\(N\in\mathbb N\))

\(\Gamma::=\Gamma|\Gamma'\), parallel composition

Stipulation

Let \(G=A:!1₿@x|A:?1₿@y|A:secret\ a\).

\(\langle A,1₿\rangle_x|\langle A,1₿\rangle_y|\{G\}C\)

\(\to\langle A,1₿\rangle_x|\langle A,1₿\rangle_y|\{G\}C|\{A:a\#N\}|A[\#\triangleright\{G\}C]=\Gamma\)

\(\to\Gamma|A[x\triangleright\{G\}C]\)

\(\to\langle A,1₿\rangle_y|\langle C,1₿\rangle_z|\{A:a\#N\}\)

where value \(N\) is the length of the secret in bits, the actual value is immaterial in BitML.

Syntax of Contracts

\(C::=\sum_{i\in I}D_i\), contract

\(D::=\text{put }\vec x\&\text{ reveal }\vec a\ if\ p.C\), collect deposits \(\vec x\) and secrets \(\vec a\).

\(D::=\text{withdraw }A\), transfer the balance to \(A\)

\(D::=\text{split }\vec v\to \vec C\), split the balance (\(|\vec v|=|\vec C|\))

\(D::=A:D\), wait for \(A\)'s authorization

\(D::=\text{after }t:D\), wait until time \(t\)

Sums

In a sum \(\sum_{i\in I}D_i\) at most one branch is executed.

The executed branch is picked among the enabled ones.

It can happen that no branch is enabled in a certain state, it may be a transient situation or the contract is stuck.

Withdraw

withdraw A, it simply transfers the contract balance to participant \(A\) and terminates.

\(\langle\text{withdraw }A,v\rangle_x\to\langle A,v\rangle_y\)

Put

put \(\vec x.C\), it addes the deposits at \(\vec x\) to the contract balance

Reveal

reveal \(\vec a\) if \(p.C\), reveals the committed secrets and, if \(p\) holds, reduces to \(C\).

Authorizations

\(A:D\), behaves as \(D\), but requires \(A\)'s authorization. If \(A\) doesn't provide the authorization, the branch is not enabled.

Split

split \(\vec v\to\vec C\), splits the contract in several contracts that are executed in parallel. The sum of the balances of the new contracts cannot exceed the balance of the original one

Time

In BitML, time is dealt with by adding the current time \(t\) in parallel with the untimed configuration \(\Gamma|t\).

Delay transitions increase \(t\) by some non-zero value \(\delta\) and leave the configuration otherwise unchanged.

Action transitions, instead, are instant: \(t\) does not change.

A time consuming action can be encoded with a delay transition followed by an action transition

After

after \(t:D\), behaves as \(D\) if current time is greater or equal than \(t\). Cannot fire otherwise.

Some Example

Omitted

Compiling BitML

A contract advertisement \(\{G\}C\) is compiled to a finite set of Bitcoin transactions.

These transactions are signed by all participants

The first transaction is \(T_{init}\), which redeems all the deposits and can be redeemed by the transactions corresponding to the subsequent moves in the contract.

When \(T_{init}\) is appended to the blockchain, the contract is stipulated.

Key Generation

Before compilations, participants generate the key pairs and exchange the public ones

  • \(K(A)\), used by \(A\) to redeem her founds from a withdraw \(A\) contract.
  • \(K(D,A)\), for all subterms \(D\) of \(C\). These keys are required to perform the first step of \(D\).

Compilation

After key generation and exchange, participants use the BitML compiler to create the transactions.

Participants sign transactions with the appropriate private keys.

Participants exchange signatures for all transactions but \(T_{init}\).

After all signatures are collected, participants sign and exchange \(T_{init}\).

Otherwise, a malicious participant could submit \(T_{init}\) without signing the rest of the transactions.

Extensions of BitML

Recursion

An extension of BitML pursues this by extending the language with a renegotiation primitive. The new renegotiated contract redeems the old contract balance.

Verification

BitML comes with a compiler and a model checker.

The model checker allows to verify the liquidity property: a contract is liquid if it never freezes founds indefinitely.

Also possible to verify custom LTL properties.