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

TL;DR

This paper uses model checking to analyze the concrete security of proof-of-work protocols like Bitcoin, revealing tradeoffs in protocol design choices affecting properties such as chain quality and common prefix.

Contribution

It introduces a model-checking approach to evaluate proof-of-work protocols under various parameters and adversarial strategies, providing insights beyond asymptotic analysis.

Findings

Uniform tie-breaking reduces chain quality failure

Tie-breaking increases common prefix failure

Tradeoffs depend on protocol parameters and adversarial strategies

Abstract

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.