A formal analysis of blockchain consensus

In this thesis, we analyse these protocols using PRISM+, our extension of the probabilistic model checker PRISM with blockchain types and operations upon them. This allows us to model the behaviour of key participants in the protocols and describe the protocols as a parallel composition of PRISM+ processes. Through our analysis of the Bitcoin model, we are able to understand how forks (where different nodes have different versions of the blockchain) occur and how they depend on specific parameters of the protocol, such as the difficulty of the cryptopuzzle and network communication delays. Our results corroborate the statement that considering confirmed the transactions in blocks at depth larger than 5 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 the Bitcoin network with churn miners (nodes that leave and rejoin the network) and with different topologies (linear topology, ring topology, tree topology and fully connected topology). PRISM+ is therefore used to analyse the resilience of Hybrid Casper when changing various basic parameters of the protocol, such as block creation rates and penalty determination strategies. We also study the robustness of Hybrid Casper against two known attacks: the Eclipse attack (where an attacker controls a significant portion of the network's nodes and can prevent other nodes from receiving new transactions) and the majority attack (where an attacker controls a majority of the network's nodes and can manipulate the blockchain to their advantage).