形式化Nakamoto风格的权益证明
Formalizing Nakamoto-Style Proof of Stake
摘要：
容错分布式系统将对单个参与方的信任转移到参与协议的大多数参与方。这使得基于区块链的加密货币成为可能：它们允许各方在没有可信第三方的情况下就交易的总顺序达成一致。要信任分布式系统，协议的安全性和实现的正确性必须是无可争议的。我们提出了第一个机器检查证明，保证安全性和活性的共识算法。我们使用基础证明助手Coq验证了一个权益证明（PoS）Nakamoto风格的区块链（NSB）协议。特别是，我们认为一个PoS NSB在一个同步网络与一组静态的损坏方。我们定义执行语义，这种设置和证明链增长，链质量，共同前缀，这意味着安全和活性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
