License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FMBC.2020.7
URN: urn:nbn:de:0030-drops-134209
Go to the corresponding OASIcs Volume Portal

Rupić, Kristijan ; Rožić, Lovro ; Derek, Ante

Mechanized Formal Model of Bitcoin’s Blockchain Validation Procedures

OASIcs-FMBC-2020-7.pdf (0.4 MB)


We present the first mechanized formal model of Bitcoin’s transaction and blockchain data structures including the formalization of the blockchain validation procedures. Our formal model, though still a simplified representation of an actual Bitcoin blockchain, includes regular and coinbase transactions, segregated witnesses, relative and absolute locktime, the Bitcoin Script language expressions together with a denotational semantics, transaction fees and block rewards. We formally specify the details of validity checks performed when adding new blocks to the blockchain. We assume perfect cryptography and use the symbolic approach for modeling hash functions and digital signatures.
To demonstrate the utility of the model, we formally state and prove several essential properties of a valid blockchain - transactions are unique, each coin can be spent at most once and the new value is only created through block rewards. The model and the proofs are largely independent of Bitcoin specific details and easily generalize to any cryptocurrency blockchain based on the Unspent Transaction Output (UTXO) paradigm.
We mechanize all the results using the Coq proof assistant.

BibTeX - Entry

  author =	{Kristijan Rupić and Lovro Rožić and Ante Derek},
  title =	{{Mechanized Formal Model of Bitcoin’s Blockchain Validation Procedures}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{7:1--7:14},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bruno Bernardo and Diego Marmsoler},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-134209},
  doi =		{10.4230/OASIcs.FMBC.2020.7},
  annote =	{Keywords: blockchain, Bitcoin, program verification, Coq}

Keywords: blockchain, Bitcoin, program verification, Coq
Collection: 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
Issue Date: 2020
Date of publication: 11.12.2020
Supplementary Material: The Coq artifacts are available as as an open-source project at

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI