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.Gabbrielli.2
URN: urn:nbn:de:0030-drops-132242
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13224/
Go to the corresponding OASIcs Volume Portal

Laneve, Cosimo ; Veschetti, Adele

A Formal Analysis of the Bitcoin Protocol

pdf-format:
OASIcs-Gabbrielli-2.pdf (2 MB)

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.

BibTeX - Entry

@InProceedings{laneve_et_al:OASIcs:2020:13224,
  author =	{Cosimo Laneve and Adele Veschetti},
  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 =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{Frank S. de Boer and Jacopo Mauro},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13224},
  URN =		{urn:nbn:de:0030-drops-132242},
  doi =		{10.4230/OASIcs.Gabbrielli.2},
  annote =	{Keywords: Bitcoin, Distributed consensus, Distributed ledgers, Blockchain, PRISM, forks}
}

Keywords: Bitcoin, Distributed consensus, Distributed ledgers, Blockchain, PRISM, forks
Collection: Recent Developments in the Design and Implementation of Programming Languages
Issue Date: 2020
Date of publication: 27.11.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI