区块链技术因为比特币的引入被人们广泛关注。随着近几年的发展,区块链技术的应用已不再局限于比特币等数字货币,更多传统行业与区块链结合的应用被开发出来,大量数字资产通过区块链进行管理导致区块链很容易遭受黑客攻击,安全问题阻碍了区块链的发展。共识协议是区块链的核心技术,目前已知的区块链系统受到的攻击大多针对于共识协议,只有保证共识协议的安全性才能使得区块链更加可靠从而被广泛应用。形式化方法是分析网络协议安全性最有力的方法之一。模型检测是形式化方法的一种,基于状态空间搜索对协议执行过程中所有状态进行遍历,发现潜在漏洞,进而保证协议的安全性。本文主要研究区块链共识协议的安全性问题。选取典型的区块链共识协议PBFT（Practical Byzantine Fault Tolerance,实用拜占庭容错）作为研究对象,采用形式化方法分析PBFT协议的安全性,论文主要工作如下:（1）提出PBFT共识协议抽象建模方法,简化协议执行过程中的实体个数,简化消息结构,假设协议使用的密码系统是完备的。对Maggi提出的建模方法进行扩展,针对于协议执行不同阶段定义消息传递通道。抽象和简化PBFT协议交互流程,解决PBFT共识协议通信过程过于复杂难以使用形式化方法分析的问题。（2）提出一种针对PBFT共识协议安全性分析的拜占庭节点模型构建方法,分析在PBFT协议执行过程中拜占庭节点能够对共识过程造成的破坏,将拜占庭节点的行为分为发送真消息、不发送消息、重放消息和伪造消息四类。（3）抽象PBFT一致性协议、视图切换协议的安全性质,使用LTL公式进行刻画,运用模型检测工具SPIN分析验证。分析存在拜占庭节点的情况下PBFT协议的安全性。将参与协议执行的诚实节点以及拜占庭节点数量作为自变量,给出协议能够容忍的拜占庭节点数量上限。综上所述,本文所提出协议抽象建模方法以及拜占庭节点模型构建方法,对采用形式化方法分析PBFT共识协议安全性具有参考意义;提出改变参与协议执行的节点数量来探究协议容错性上限的方法,可适用于此类共识协议的容错性分析。