Model Checking Bitcoin and other Proof-of-Work Consensus Protocols

The Bitcoin Backbone Protocol [4] is an abstraction of the bitcoin proof-of-work consensus protocol. We use a model-checking tool (UPPAAL-SMC) to examine the security of proof-of-work consensus by varying protocol parameters, using an adversary that leverages the selfish mining strategy introduced in [4]. We provide insights into modeling proof-of-work protocols and demonstrate trade-offs between operating parameters. Applying this methodology to protocol design, we show that the uniform tie-breaking rule from [11], an attempt to mitigate selfish mining, improves chain quality but decreases the common prefix probability. This trade-off illustrates how design decisions affect desirable protocol properties, within a range of concrete operating conditions, in a manner that is not evident from prior asymptotic analysis.