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;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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11391/1535919
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 0
social impact