对中本聪式权益证明的形式化验证
密码学与安全
2023-03-15 v2 计算机科学中的逻辑
摘要
容错分布式系统将对单一方的信任转移到了参与协议的多数方上。这使得基于区块链的加密货币成为可能：它们允许各方在无可信第三方的情况下就交易的全序达成一致。要信任一个分布式系统，协议的安全性及实现的正确性必须无可争议。我们提出了首个经机器检验的证明，其同时保证共识算法的安全性和活性。我们使用基础证明辅助工具 Coq 验证了一种中本聪式区块链（NSB）的权益证明（PoS）协议。具体而言，我们考虑了在同步网络中具有静态腐败方集合的 PoS NSB。我们为该设定定义了执行语义，并证明了链增长、链质量与公共前缀性质，这些性质共同蕴含了安全性与活性。
引用
@article{arxiv.2007.12105,
title = {Formalizing Nakamoto-Style Proof of Stake},
author = {Søren Eller Thomsen and Bas Spitters},
journal= {arXiv preprint arXiv:2007.12105},
year = {2023}
}