Search Results

Documents authored by Rožić, Lovro


Document
Mechanized Formal Model of Bitcoin’s Blockchain Validation Procedures

Authors: Kristijan Rupić, Lovro Rožić, and Ante Derek

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)


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.

Cite as

Kristijan Rupić, Lovro Rožić, and Ante Derek. Mechanized Formal Model of Bitcoin’s Blockchain Validation Procedures. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{rupic_et_al:OASIcs.FMBC.2020.7,
  author =	{Rupi\'{c}, Kristijan and Ro\v{z}i\'{c}, Lovro and Derek, Ante},
  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 =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.7},
  URN =		{urn:nbn:de:0030-drops-134209},
  doi =		{10.4230/OASIcs.FMBC.2020.7},
  annote =	{Keywords: blockchain, Bitcoin, program verification, Coq}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail