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 / Bistarelli S.; De Nicola R.; Galletta L.; Laneve C.; Mercanti I.; Veschetti A.. - In: CONCURRENCY AND COMPUTATION. - ISSN 1532-0626. - ELETTRONICO. - Early View:(2021), pp. e6749.1-e6749.20. [10.1002/cpe.6749]

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

Laneve C.;Veschetti A.
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.
2021
Stochastic modeling and analysis of the bitcoin protocol in the presence of block communication delays / Bistarelli S.; De Nicola R.; Galletta L.; Laneve C.; Mercanti I.; Veschetti A.. - In: CONCURRENCY AND COMPUTATION. - ISSN 1532-0626. - ELETTRONICO. - Early View:(2021), pp. e6749.1-e6749.20. [10.1002/cpe.6749]
Bistarelli S.; De Nicola R.; Galletta L.; Laneve C.; Mercanti I.; Veschetti A.
File in questo prodotto:
File Dimensione Formato  
Blockchain_PRISM_PEPA.pdf

accesso aperto

Tipo: Postprint
Licenza: Licenza per accesso libero gratuito
Dimensione 1.62 MB
Formato Adobe PDF
1.62 MB 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: https://hdl.handle.net/11585/854096
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 2
social impact