DROPS

Document

A Formal Analysis of the Bitcoin Protocol

Authors: Cosimo Laneve and Adele Veschetti

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

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

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)

Copy BibTex To Clipboard

@InProceedings{laneve_et_al:OASIcs.Gabbrielli.2,
  author =	{Laneve, Cosimo and Veschetti, Adele},
  title =	{{A Formal Analysis of the Bitcoin Protocol}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{2:1--2:17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.2},
  URN =		{urn:nbn:de:0030-drops-132242},
  doi =		{10.4230/OASIcs.Gabbrielli.2},
  annote =	{Keywords: Bitcoin, Distributed consensus, Distributed ledgers, Blockchain, PRISM, forks}
}

Search Results

Documents authored by Laneve, Cosimo

A Formal Analysis of the Bitcoin Protocol

Abstract

Cite as

Thanks for your feedback!

Could not send message