Stochastic Modelling and Analysis of the Bitcoin Protocol in Presence of Block Communication Delays

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 behaviour 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 permanent is reasonable because the majority of miners have consistent blockchains up-to that depth with probability of almost 1. We also study the behaviour of networks with churn miners, which may leave the network and rejoin afterwards, and with different topologies.