Model Checking Bitcoin and other Proof-of-Work Consensus Protocols
This work addresses security tradeoffs in blockchain protocol design for developers and researchers, though it is incremental as it builds on existing models and methods.
The researchers tackled the concrete security of Bitcoin and other proof-of-work consensus protocols by using model-checking to analyze protocol parameters and selfish mining attacks, showing that a uniform tie-breaking rule reduces chain quality failures but increases common prefix failures, revealing tradeoffs not apparent in prior asymptotic analyses.
The Bitcoin Backbone Protocol [GKL15] is an abstraction of the bitcoin proof-of-work consensus protocol. We use a model-checking tool (UPPAALSMC) to examine the concrete security of proof-ofwork consensus by varying protocol parameters and using an adversary that leverages the selfish mining strategy introduced in [GKL15]. We provide insights into modeling proof-of-work protocols and demonstrate tradeoffs between operating parameters. Applying this methodology to protocol design options, we show that the uniform tie-breaking rule from [ES18] decreases the failure rate of the chain quality property, but increases the failure rate of the common prefix property. This tradeoff illustrates how design decisions affect protocol properties, within a range of concrete operating conditions, in a manner that is not evident from prior asymptotic analysis.