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.
@article{arxiv.2007.08644,
title = {Model Checking Bitcoin and other Proof-of-Work Consensus Protocols},
author = {Max DiGiacomo-Castillo and Yiyun Liang and Advay Pal and John C. Mitchell},
journal= {arXiv preprint arXiv:2007.08644},
year = {2020}
}