论文标题
模型检查比特币和其他工作证明共识协议
Model Checking Bitcoin and other Proof-of-Work Consensus Protocols
论文作者
论文摘要
比特币骨干协议[GKL15]是比特币证明共识协议的抽象。我们使用模型检查工具（UPPAALSMC）通过改变协议参数并使用利用[GKL15]中引入的自私采矿策略的对手来检查实验证明共识的具体安全性。我们提供了建模工作证明协议的见解，并展示了操作参数之间的权衡。将此方法应用于协议设计选项，我们表明[ES18]的统一罢工规则降低了链质量属性的故障率，但增加了普通前缀属性的失败率。这种折衷说明了设计决策如何影响协议属性，在一系列具体的工作条件下，从先前的渐近分析中看不出。
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.
