面向Coq中Algorand共识协议的已验证模型

Algorand区块链是一个基于纯权益证明而非工作量证明的安全去中心化公共账本。其核心是一种新颖的共识协议，每轮仅认证一个区块：即协议保证区块链不发生分叉。本文中，我们报告了在Coq证明助手中建模并形式化验证Algorand共识协议的工作。与以往的共识协议验证工作类似，我们将协议建模为状态转移系统并就可达全局状态进行推理。然而，与以往工作不同，我们的模型显式纳入了时序问题（例如超时与网络延迟）和对抗行为，反映了公共区块链面临的更真实环境。迄今为止，我们已证明了协议的异步安全性：即使 adversary 完全控制网络中消息传递，同一轮中也不能认证两个不同的区块。我们相信我们的模型具有足够的通用性，协议的其他相关属性（如活性）可在同一模型上得证。