Skip to content

Focus on Bitcoin and some other platforms.

Contents

A ledger of transactions

Replication among a dynamic set of nodes.

Decentralization

Smart Contracts

Programs or protocols that run on blockchains.

Possible to custom decentralized functionalities.

Platforms like Ethereum natively support smart contracts, but Bitcoin doesn't.

Why Formal Methods for Blockchain and Smart Contracts?

Errors cause huge economical losses.

Many platforms don't allow to modify contracts after deployment.

Formal verification of contracts prior of deployment is desirable.

Consensus

Consensus algorithm:

  • Classical consensus
  • Nakamoto consensus
  • ...

Cryptographic Hash Functions

\(h:\{0,1\}^*\to\{0,1\}^n\) such that

  • given \(h(x)\), finding \(x\) is computationally hard. (pre-image resistance)
  • finding \(x\neq y\) s.t. \(h(x)=h(y)\) is computationally hard (collision resistance)
  • given \(x\), finding \(y\) s.t. \(h(x)=h(y)\) is computationally hard (second pre-image resistance)
  • \(h\) can be computed efficiently

On Collisions

\(\{0,1\}^*\) is bigger than \(\{0,1\}^n\), therefore collisions must exist.

How to find collisions: By brute force: try \(2^n+1\) distinct inputs. Finding such is computationally hard. If inputs are uniformly at random, \(2^{n/2}\) attempts lead to a collision with \(1/2\) probability. (Still exponential)

Realistic Hash Functions

Complex combination of simple operations

SHA256 (Bitcoin)

KECCAC256 (Ethereum), precursor of SHA3

Applications

Message digests, digital signatures...

In blockchain:

  1. Proof of work
  2. To link the previous block
  3. To link a block header to the list of transactions of the block.

Digital Signatures

Formally, a digital signature consists of 3 probabilistic polynomial algorithms (gen, sign, vrfy)

  • gen returns a pair of keys (pk, sk), resp called public key and private key.
  • sign takes in input a message \(m\) and a private key sk and returns a signature \(\sigma\)
  • vrfy is deterministic, it takes in input a public key pk, a message \(m\) and a signature \(\sigma\), and check if the signature is equal to the value of message \(m\) crypted on pk.

A digital signature is used as follows

  1. A participant S runs gen and gets key pair.
  2. public key is broadcasted to the network, while sk is kept secret

Security of Signatures

The probability of successful attack (run in polynomial time) is low

Or to find a collision takes exponential time.

Desidarable Properties

Authentication: Receiver can verify sender's identity

Integrity: Modifying a signed message invalidates its signature

Non-repudiation: If an entity signs a message, she can't deny having signed it.

ECDSA

Elliptic Curve Digital Signature Algorithm

Both Bitcion and Ethereum use it for signing transactions.

Cryptocurrencies and Blockchians

A Naive Cryptocurrency

Each unit of currency is associated with a bit string (coin ID)

Currency is created by a special participant \(T\), which signs the newly generated coin \(<ID,SIGN_T(ID)>\), owned by \(T\).

The owner \(A\) of a coin \(c\) can spend it by generating \(<c,B,SIGN_A(c,B)>\) where \(B\) is the payee. After this transaction, \(B\) is the owner of the coin \(<c,B,SIGN_A(c,B)>\).

Problem: Double spending attack

Ruling out: Introducing a Trusted Authority (TA)

But TA can be problematic:

  • It might become unreliable

Ruling out TA

Use p2p network of nodes

In order to avoid double spending, we need to record all payments

Transactions

Bitcoin transactions: units of currency can be split and multiple transactions can be spent at once

Ethereum has an account based model of transactions.

Transaction is in the block proves there is no double spending

Blockchains and Decentralization

How are new transactions added, and who adds them?

How do we ensure that all nodes have the same copy of the blockchain?

  • Users broadcast their transactions to the network
  • Nodes collect new transactions
  • A randomly selected node groups the received transaction inside a block, appends it to the local copy of the blockchain and broadcasts the new block to the networks. If the block is valid the other nodes will append it to their local copies of the blockchain.
  • The probability of being selected is not uniform: by computing power? on amount of currency owns?
  • The selected node usually gets rewarded by some cryptocurrency.

Smart Contracts

Blockchians beyond Cryptocurrency

Blockchains were introduced in 2008 for implementing the Bitcoin cryptocurrency.

However, transactions doesn't need to be mere payments

In 2015, Ethereum blockchain was launched: it allows users to create custom programs (smart contracts) that run on the blockchain

On Smart Contracts

Proposed in 1994 by Nick Szabo.

A smart contract is a computerized transaction protocol that executes the terms of a contract.

Blockchains allow implementing smart contracts in a relative simple manner

Smart contracts exploit the following properties of programming languages

  • unambiguous semantics
  • executable

Implications of Contracts as Code

Contract clauses cannot be modified after stipulation

Code should be non-updatable

Problematic in case of buggy software

Decentralized Applications

dApps

Exchanges

DeFi (Decentralized Finance)

Market places

Gambling

Games