论文标题
正式化纳卡摩式风格的股份证明
Formalizing Nakamoto-Style Proof of Stake
论文作者
论文摘要
容忍性分布式系统将单个方的信任转移到参加该协议的大多数当事方。这使基于区块链的加密货币成为可能：它们允许当事方就没有信任的第三方的总交易达成共识。为了信任分布式系统，协议的安全性和实施的正确性必须是无可争议的。 我们介绍了第一台机器检查证明，以确保共识算法的安全性和可笑性。我们使用基础证明助理Coq验证了股权证明（POS）中amoto风格的区块链（NSB）协议。 特别是，我们考虑了具有静态损坏方的同步网络中的POS NSB。我们为此设置定义了执行语义，并证明了链的增长，链质量和常见前缀，这既意味着安全性和livesice。
Fault-tolerant distributed systems move the trust in a single party to a majority of parties participating in the protocol. This makes blockchain based crypto-currencies possible: they allow parties to agree on a total order of transactions without a trusted third party. To trust a distributed system, the security of the protocol and the correctness of the implementation must be indisputable. We present the first machine checked proof that guarantees both safety and liveness for a consensus algorithm. We verify a Proof of Stake (PoS) Nakamoto-style blockchain (NSB) protocol, using the foundational proof assistant Coq. In particular, we consider a PoS NSB in a synchronous network with a static set of corrupted parties. We define execution semantics for this setting and prove chain growth, chain quality, and common prefix which together imply both safety and liveness.
