一种基于拜占庭容错的PoS共识协议形式化分析方法  

A Formal Analysis Method of PoS Consensus Protocol Based on Byzantine Fault Tolerance

作　　者：陈凯杰 熊焰[1] 黄文超[1] 武建双 CHEN Kaijie;XIONG Yan;HUANG Wenchao;WU Jianshuang(Department of Computer Science and Technology,University of Science and Technology of China,Hefei 230022,China;Hefei Tianwei Information Security Technology Co.,Ltd.,Hefei 230000,China)

机构地区：[1]中国科学技术大学计算机科学与技术学院,合肥230022 [2]合肥天帷信息安全技术有限公司,合肥230000

出　　处：《信息网络安全》2021年第8期35-42,共8页Netinfo Security

基　　金：国家自然科学基金[61972369];国家重点研发计划[2018YFB2100301]。

摘　　要：区块链共识协议是一种确保区块链网络中不同节点的数据达成一致的重要机制,随着区块链应用的爆发性增长,针对区块链共识协议的攻击不断出现。文章提出一种基于拜占庭容错的PoS共识协议形式化分析方法,通过归纳建模共识节点整体状态迁移解决协议模型状态空间爆炸问题,同时结合实际安全威胁形式化建模信道模型和攻击者模型,根据协议一致性要求形式化描述两大类安全属性并进行形式化验证。实验结果表明,该类协议具有拜占庭容错能力。最后,文章分析了针对0确认交易的双花攻击所需的条件,并提出防护方法。The blockchain consensus protocol is an important mechanism to ensure that the data of different nodes reach consensus in the blockchain network.With the explosive growth of blockchain applications,attacks against blockchain consensus mechanisms continue to emerge.This paper proposes a formal analysis method of PoS consensus protocol based on Byzantine fault tolerance.To solve the problem of protocol model state space explosion,the method first inductively models the state migration process of all consensus nodes.Then,the communication channel models and attacker models are formally modeled based on the actual security threats.Finally,according to the requirements of protocol consistency,two kinds of security properties are formally modeled and verified.The experimental results show that the protocol has the claimed Byzantine fault tolerance,and the protocol has a double-spending attack against the zero-confirmation transaction.This paper further analyzes the conditions to implement the attack and puts forward suggestions for protection.

关 键 词：区块链共识协议 拜占庭容错 归纳建模 形式化分析 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]