Document Open Access Logo

Mechanized Formal Model of Bitcoin’s Blockchain Validation Procedures

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

PDF
Thumbnail PDF

File

OASIcs.FMBC.2020.7.pdf
  • Filesize: 447 kB
  • 14 pages

Document Identifiers

Author Details

Kristijan Rupić
  • Faculty of Electrical Engineering and Computing, University of Zagreb, Croatia
Lovro Rožić
  • Faculty of Electrical Engineering and Computing, University of Zagreb, Croatia
Ante Derek
  • Faculty of Electrical Engineering and Computing, University of Zagreb, Croatia

Funding

  • Derek, Ante: This research has been partially supported by the European Regional Development Fund under the grant {KK.01.1.1.01.0009} (DATACROSS).

Cite AsGet BibTex

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)
https://doi.org/10.4230/OASIcs.FMBC.2020.7

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • blockchain
  • Bitcoin
  • program verification
  • Coq

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Bitcoin documentation. https://en.bitcoin.it/wiki/Protocol_documentation, 2010.
  2. Bitcoin improvement proposal 30: Duplicate transactions. https://github.com/bitcoin/bips/blob/master/bip-0030.mediawiki, 2012.
  3. Bitcoin improvement proposal 34: Block v2, height in coinbase. https://github.com/bitcoin/bips/blob/master/bip-0034.mediawiki, 2012.
  4. Bitcoin improvement proposal 141: Segregated witness (consensus layer). https://github.com/bitcoin/bips/blob/master/bip-0141.mediawiki, 2015.
  5. Double spending in bitcoin clients. https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2018-17144, 2018.
  6. Bitcoin improvement proposal 341: Segwit version 1 spending rules. https://github.com/bitcoin/bips/blob/master/bip-0341.mediawiki, 2020.
  7. Andrew W. Appel. Verification of a cryptographic primitive: Sha-256. ACM Trans. Program. Lang. Syst., 37(2), April 2015. URL: https://doi.org/10.1145/2701415.
  8. Nicola Atzei, Massimo Bartoletti, Tiziana Cimoli, Stefano Lande, and Roberto Zunino. Sok: Unraveling bitcoin smart contracts. In Principles of Security and Trust, pages 217-242, Cham, 2018. Springer International Publishing. Google Scholar
  9. Nicola Atzei, Massimo Bartoletti, Stefano Lande, and Roberto Zunino. A formal model of bitcoin transactions. IACR Cryptology ePrint Archive, 2017:1124, 2017. Google Scholar
  10. Vitalik Buterin. A next-generation smart contract and decentralized application platform. https://github.com/ethereum/wiki/wiki/White-Paper, 2014. White-paper.
  11. Christian Cachin, Angelo De Caro, Pedro Moreno-Sanchez, Björn Tackmann, and Marko Vukolic. The transaction graph for modeling blockchain semantics. IACR Cryptology ePrint Archive, 2017:1070, 2017. Google Scholar
  12. R. Canetti, A. Stoughton, and M. Varia. Easyuc: Using easycrypt to mechanize proofs of universally composable security. In 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), pages 167-16716, June 2019. Google Scholar
  13. Manuel Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Michael Peyton Jones, and Philip Wadler. The extended utxo model. In Workshop on Trusted Smart Contracts, 2020. Google Scholar
  14. Kaylash Chaudhary, Ansgar Fehnker, Jan Cornelis van de Pol, and Mariëlle Ida Antoinette Stoelinga. Modeling and verification of the bitcoin protocol. In Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015), Electronic Proceedings in Theoretical Computer Science, pages 46-60, Australia, November 2015. Open Publishing Association. Google Scholar
  15. D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198-208, March 1983. Google Scholar
  16. Juan Garay, Aggelos Kiayias, and Nikos Leonardos. The bitcoin backbone protocol: Analysis and applications. In Advances in Cryptology - EUROCRYPT 2015, pages 281-310, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. Google Scholar
  17. Rick Klomp and Andrea Bracciali. On symbolic verification of bitcoin’s SCRIPT language. In Data Privacy Management, Cryptocurrencies and Blockchain Technology, pages 38-56, Cham, 2018. Springer International Publishing. Google Scholar
  18. Satoshi Nakamoto. Bitcoin: a peer-to-peer electronic cash system. https://bitcoin.org/bitcoin.pdf, 2008.
  19. Karl Palmskog, Milos Gligoric, Lucas Pena, Brandon Moore, and Grigore Rosu. Verification of casper in the coq proof assistant. https://github.com/runtimeverification/casper-proofs, 2018. Technical report.
  20. Karl Palmskog, Milos Gligoric, Lucas Pena, Brandon Moore, and Grigore Rosu. Verifying finality for blockchain systems. In CoqPL'19, 2019. Google Scholar
  21. Adam Petcher and Greg Morrisett. The foundational cryptography framework. In Principles of Security and Trust, pages 53-72, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. Google Scholar
  22. George Pirlea and Ilya Sergey. Mechanising blockchain concensus. In 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM New York, 2018. Google Scholar
  23. Ilya Sergey and Kiran Gopinathan. Towards mechanising probabilistic properties of a blockchain. In CoqPL'19, 2019. Google Scholar
  24. The Coq Development Team. The coq proof assistant, version 8.10.0, October 2019. URL: https://doi.org/10.5281/zenodo.3476303.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact