Modelling Bitcoin in Agda

TL;DR

This paper formalizes two models of Bitcoin's blockchain in Agda, capturing transaction structures, cryptographic operations, and blockchain properties, enabling rigorous reasoning about correctness within a proof assistant.

Contribution

It introduces two novel formal models of Bitcoin's blockchain in Agda, utilizing advanced features like induction-recursion for precise representation.

Findings

Models include standard transactions, coinbase transactions, and Merkle trees.

Abstract cryptographic operations are incorporated, with correctness outlined.

Models facilitate formal verification of blockchain properties in Agda.

Abstract

We present two models of the block chain of Bitcoin in the interactive theorem prover Agda. The first one is based on a simple model of bank accounts, while having transactions with multiple inputs and outputs. The second model models transactions, which refer directly to unspent transaction outputs, rather than user accounts. The resulting blockchain gives rise to a transaction tree. That model is formalised using an extended form of induction-recursion, one of the unique features of Agda. The set of transaction trees and transactions is defined inductively, while simultaneously recursively defining the list of unspent transaction outputs. Both structures model standard transactions, coinbase transactions, transaction fees, the exact message to be signed by those spending money in a transaction, block rewards, blocks, and the blockchain, and the second structure models as well maturation time for coinbase transactions and Merkle trees. Hashing and cryptographic operations and their correctness are dealt with abstractly by postulating corresponding operations. An indication is given how the correctness of this model could be specified and proven in Agda.