Document Open Access Logo

A Formal Analysis of the Bitcoin Protocol

Authors Cosimo Laneve , Adele Veschetti

PDF

File

Thumbnail PDF
PDF
OASIcs.Gabbrielli.2.pdf
  • Filesize: 1.55 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Formalisms
Keywords
  • Bitcoin
  • Distributed consensus
  • Distributed ledgers
  • Blockchain
  • PRISM
  • forks

Metrics

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

Abstract

We study Nakamoto’s Bitcoin protocol that implements a distributed ledger on peer-to-peer asynchronous networks. In particular, we define a principled formal model of key participants - the miners - as stochastic processes and describe the whole system as a parallel composition of miners. We therefore compute the probability that ledgers turn into a state with more severe inconsistencies, e.g. with longer forks, under the assumptions that messages are not lost and nodes are not hostile. We also study how the presence of hostile nodes mining blocks in wrong positions impacts on the consistency of the ledgers. Our theoretical results agree with the simulations performed on a probabilistic model checker that we extended with dynamic datatypes in order to have a faithful description of miners' behaviour.

Cite As Get BibTex

Cosimo Laneve and Adele Veschetti. A Formal Analysis of the Bitcoin Protocol. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/OASIcs.Gabbrielli.2

Author Details

Cosimo Laneve
  • Dept. of Computer Science and Engineering, University of Bologna - INRIA Focus, Italy
Adele Veschetti
  • Dept. of Computer Science and Engineering, University of Bologna - INRIA Focus, Italy

References

  1. Bruno Biais, Christophe Bisiere, Matthieu Bouvard, and Catherine Casamatta. The blockchain folk theorem, 2018. Google Scholar
  2. S. Bistarelli, R. De Nicola, L. Galletta, C. Laneve, I. Mercanti, and A. Veschetti. Stochastic modelling and analysis of bitcoin. Manuscript submitted for publication, 2020. Google Scholar
  3. Joseph Bonneau, Andrew Miller, Jeremy Clark, Arvind Narayanan, Joshua A. Kroll, and Edward W. Felten. Sok: Research perspectives and challenges for bitcoin and cryptocurrencies. In Proc. of SP 2015, pages 104-121. IEEE Computer Society, 2015. Google Scholar
  4. R. Bowden, H. Paul Keeler, Anthony E. Krzesinski, and Peter G. Taylor. Block arrivals in the bitcoin blockchain. CoRR, abs/1801.07447, 2018. Google Scholar
  5. Miles Carlsten, Harry Kalodner, S. Matthew Weinberg, and Arvind Narayanan. On the instability of bitcoin without the block reward. In Proc. Computer and Communications Security, CCS '16, pages 154-167. ACM, 2016. Google Scholar
  6. Christian Decker and Roger Wattenhofer. Information propagation in the bitcoin network. In Proc. 13th IEEE P2P, pages 1-10. IEEE, 2013. Google Scholar
  7. Parinya Ekparinya, Vincent Gramoli, and Guillaume Jourjon. Double-spending risk quantification in private, consortium and public ethereum blockchains. CoRR, abs/1805.05004, 2018. URL: http://arxiv.org/abs/1805.05004.
  8. Ittay Eyal and Emin Gün Sirer. Majority is not enough: Bitcoin mining is vulnerable. Commun. ACM, 61(7):95-102, June 2018. URL: https://doi.org/10.1145/3212998.
  9. Michael J. Fischer, Nancy A. Lynch, and Mike Paterson. Impossibility of distributed consensus with one faulty process. J. ACM, 32(2):374-382, 1985. Google Scholar
  10. A. Fox and E. A. Brewer. Harvest, yield, and scalable tolerant systems. In Proceedings of the Seventh Workshop on Hot Topics in Operating Systems, pages 174-178, 1999. Google Scholar
  11. Juan A. Garay, Aggelos Kiayias, and Nikos Leonardos. The bitcoin backbone protocol: Analysis and applications. In Proc. of EUROCRYPT 2015, volume 9057 of Lecture Notes in Computer Science, pages 281-310. Springer, 2015. Google Scholar
  12. Johannes Göbel, Holger Paul Keeler, Anthony E. Krzesinski, and Peter G. Taylor. Bitcoin blockchain dynamics: The selfish-mine strategy in the presence of propagation delay. Perform. Eval., 104:23-41, 2016. Google Scholar
  13. Vincent Gramoli. From blockchain consensus back to byzantine consensus. Future Gener. Comput. Syst., 107:760-769, 2020. Google Scholar
  14. Stuart Haber and W. Scott Stornetta. How to time-stamp a digital document. Journal of Cryptology, 3(2):99-111, January 1991. URL: https://doi.org/10.1007/BF00196791.
  15. Charles Antony Richard Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666-677, 1978. Google Scholar
  16. Ghassan Karame, Elli Androulaki, and Srdjan Capkun. Double-spending fast payments in bitcoin. In Proc. of CCS'12, pages 906-917. ACM, 2012. Google Scholar
  17. M. Kwiatkowska, G. Norman, and D. Parker. Stochastic model checking. In M. Bernardo and J. Hillston, editors, Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), volume 4486 of LNCS (Tutorial Volume), pages 220-270. Springer, 2007. Google Scholar
  18. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Probabilistic symbolic model checking with PRISM: A hybrid approach. In Proc. TACAS 2002, volume 2280 of Lecture Notes in Computer Science, pages 52-66. Springer, 2002. Google Scholar
  19. Andrew Miller and Joseph J LaViola Jr. Anonymous byzantine consensus from moderately-hard puzzles: A model for bitcoin. Available on line: http://nakamotoinstitute. org/research/anonymous-byzantine-consensus, 2014. Google Scholar
  20. Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic cash system, 2008. URL: http://www.bitcoin.org/bitcoin.pdf.
  21. A. Pinar Ozisik and Brian Neil Levine. An explanation of nakamoto’s analysis of double-spend attacks. CoRR, abs/1701.03977, 2017. URL: http://arxiv.org/abs/1701.03977.
  22. Rafael Pass, Lior Seeman, and Abhi Shelat. Analysis of the blockchain protocol in asynchronous networks. In Proc. of EUROCRYPT 2017, volume 10210 of Lecture Notes in Computer Science, pages 643-673. Springer, 2017. Google Scholar
  23. George Pîrlea and Ilya Sergey. Mechanising blockchain consensus. In Proc. 7th Certified Programs and Proofs, CPP, pages 78-90. ACM, 2018. Google Scholar
  24. Muhammad Saad, Victor Cook, Lan Nguyen, My T. Thai, and Aziz Mohaisen. Partitioning attacks on bitcoin: Colliding space, time, and logic. In 39th IEEE Conference on Distributed Computing Systems, ICDCS 2019, pages 1175-1187. IEEE, 2019. Google Scholar
  25. Yonatan Sompolinsky and Aviv Zohar. Secure high-rate transaction processing in bitcoin. In Proc. of Financial Cryptography and Data Security 2015, volume 8975 of Lecture Notes in Computer Science, pages 507-527. Springer, 2015. Google Scholar
  26. Alexei Zamyatin, Nicholas Stifter, Philipp Schindler, Edgar R. Weippl, and William J. Knottenbelt. Flux: Revisiting near blocks for proof-of-work blockchains. IACR Cryptology ePrint Archive, 2018:415, 2018. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact