We analyze the protocol of the bitcoin blockchain by using the PRISM probabilistic model checker. In particular, we (i) extend PRISM with the ledger data type, (ii) model the behavior of the key participants in the protocol—the miners—and (iii) describe the whole protocol as a parallel composition of processes. The probabilistic analysis of the model highlights how forks happen and how they depend on specific parameters of the protocol, such as the difficulty of the cryptopuzzle and the network communication delays. Our results confirm that considering transactions in blocks at depth larger than 5 as confirmed is reasonable because the majority of miners have consistent blockchains up-to that depth with probability of almost 1. We also study the behavior of networks with churn miners, which may leave the network and rejoin afterwards, and with different topologies.

Stochastic modeling and analysis of the bitcoin protocol in the presence of block communication delays

De Nicola R.;Galletta L.;Mercanti I.
;
2021

Abstract

We analyze the protocol of the bitcoin blockchain by using the PRISM probabilistic model checker. In particular, we (i) extend PRISM with the ledger data type, (ii) model the behavior of the key participants in the protocol—the miners—and (iii) describe the whole protocol as a parallel composition of processes. The probabilistic analysis of the model highlights how forks happen and how they depend on specific parameters of the protocol, such as the difficulty of the cryptopuzzle and the network communication delays. Our results confirm that considering transactions in blocks at depth larger than 5 as confirmed is reasonable because the majority of miners have consistent blockchains up-to that depth with probability of almost 1. We also study the behavior of networks with churn miners, which may leave the network and rejoin afterwards, and with different topologies.
bitcoin
blockchain fork
stochastic modeling & analysis
File in questo prodotto:
File Dimensione Formato  
Blockchain_PRISM_PEPA.pdf

accesso aperto

Tipologia: Documento in Pre-print
Licenza: Nessuna licenza
Dimensione 763.81 kB
Formato Adobe PDF
763.81 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/20.500.11771/20139
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
social impact