比特币是一种备受欢迎的电子加密货币,依赖其底层协议提供安全保障。然而,比特币底层协议未被权威机构要求给出专业的安全证明,因此大众难以客观认识比特币安全性。相关工作基于计算方法形式化分析了比特币安全性,但由于计算方法建模的复杂性,相关工作通过粗粒度抽象完成了比特币共识协议安全属性的手工证明和推导,规避了其他协议交互细节以及对协议组合运行的讨论。而被简略的协议部分可能会导致攻击被遗漏,因此对比特币协议更细粒度系统的分析是必要的。本文系统地抽象了比特币底层协议模块及其实体交互,设计了敌手模型和安全目标,利用符号方法实现了对比特币的细粒度形式化安全分析。本文开展的主要工作如下:1.系统地抽象了比特币各协议模块及其实体交互的行为。实际上,比特币并未对支付、共识、合作挖矿以及跨链协议及其协议实体给出明确划分和定义,本文不同于现有工作只着眼于节点实体和共识协议,将现有工作尚未细粒度抽象的比特币支付协议、矿池协议以及跨链协议纳入本文的形式化分析范围,并系统抽象了协议交互行为细节,基于比特币源码及其相关文档,抽象了五个比特币协议实体和四个协议模块及其消息交互。2.细粒度地设计了比特币敌手模型及安全目标。本文在比特币未对协议敌手模型提供准确定义的情况下,基于Dolev-Yao敌手模型以及比特币实际部署情况,赋予了敌手在比特币网络环境中可实施的攻击能力。由于比特币文档中只提到隐私性和可问责性,且缺乏精确定义,因此本文根据实体实际安全需求,形式化定义了比特币应保证的认证性、隐私性、可问责性以及金额一致性,这些安全属性用于验证比特币协议执行的单射一致性是否可被满足、交易发起方真实身份隐私性是否被保证、恶意实体是否可被找出、诚实实体是否会被错怪以及已支出资产是否可被用于伪造非法交易。3.符号化建模了可实现自动化形式化验证的比特币协议模型。本文利用符号方法,将比特币各协议模块及其实体交互形式化为一套公理体系,权衡模型复杂度及验证难度完成了可自动化验证的模型规则和引理定义,并利用形式化验证工具SmartVerif实现对模型的自动化状态推导和形式化验证实验。本文的形式化验证实验证明了比特币协议独立运行时不满足的安全属性,也证明了在考虑协议模块间交互时不满足的安全属性。本文发现了多种比特币攻击路径,包括目前已被分析的攻击以及未被形式化分析的攻击,本文为此提供了临时防护建议。