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.
@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} }
Feedback for Dagstuhl Publishing