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
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13420/
Rupić, Kristijan ;
Rožić, Lovro ;
Derek, Ante
Mechanized Formal Model of Bitcoin’s Blockchain Validation Procedures
Abstract
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
@InProceedings{rupi_et_al:OASIcs:2020:13420,
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 = {https://drops.dagstuhl.de/opus/volltexte/2020/13420},
URN = {urn:nbn:de:0030-drops-134209},
doi = {10.4230/OASIcs.FMBC.2020.7},
annote = {Keywords: blockchain, Bitcoin, program verification, Coq}
}
