面向比特币底层协议的细粒度形式化分析方法研究
发布时间：2021-01-23 09:49
比特币是一种备受欢迎的电子加密货币,依赖其底层协议提供安全保障。然而,比特币底层协议未被权威机构要求给出专业的安全证明,因此大众难以客观认识比特币安全性。相关工作基于计算方法形式化分析了比特币安全性,但由于计算方法建模的复杂性,相关工作通过粗粒度抽象完成了比特币共识协议安全属性的手工证明和推导,规避了其他协议交互细节以及对协议组合运行的讨论。而被简略的协议部分可能会导致攻击被遗漏,因此对比特币协议更细粒度系统的分析是必要的。本文系统地抽象了比特币底层协议模块及其实体交互,设计了敌手模型和安全目标,利用符号方法实现了对比特币的细粒度形式化安全分析。本文开展的主要工作如下:1.系统地抽象了比特币各协议模块及其实体交互的行为。实际上,比特币并未对支付、共识、合作挖矿以及跨链协议及其协议实体给出明确划分和定义,本文不同于现有工作只着眼于节点实体和共识协议,将现有工作尚未细粒度抽象的比特币支付协议、矿池协议以及跨链协议纳入本文的形式化分析范围,并系统抽象了协议交互行为细节,基于比特币源码及其相关文档,抽象了五个比特币协议实体和四个协议模块及其消息交互。2.细粒度地设计了比特币敌手模型及安全目标。...
【文章来源】：中国科学技术大学安徽省 211工程院校 985工程院校
【文章页数】：82 页
【学位级别】：硕士
【部分图文】：
图１．１现有工作形式化建模简化策略图示??全分析研究人员需要对各协议实体交互逻辑进行强抽象，并基于协议实际的安??
?！?！！?ｒ?＾???Ｉ?????????比特币?安全威胁?一＾?攻击者?一一＾?自动化?—??实际运行环境Ｉ？棋型定义?驗证工具???！??ｌ！?Ｕ￣存在的???！?????！！?安全漏柄??Ｉ?１１?＾?Ｉ??安全研宂人员?￣？安全目标?一＊???＞！?????ｉ：??｛?Ｉ?ｊ??规則抽象与细化的权衡??攻击者能力与证明难度的权衡?｜Ｉ??！?安全厲性集合的充整性?１１??Ｉ?Ｊ?Ｌ?Ｊ??图１．２比特币协议安全性分析整体框架??工，抽象定义了比特币各协议模块的交互细节及其实体功能，本文抽象的协议模??块包括：支付模块、共识模块、合作挖矿模块和跨链交易模块，本文抽象的协议??实体包括：商家、买家、节点、矿池服务器和矿池矿工。虽然比特币白皮书对比??特币协议模块进行了概述，但许多重要的协议交互细节都是被省略或者是过时??的，比特币协议具体实施的参考标准被分散在一系列“比特币改进建议”（ＢＩＰｓ）??以及开发人员的讨论记录中，本文结合实际被部署的比特币协议及其相关源码??及文档完成了对比特币各协议模块及其实体交互的抽象。??现有工作在形式化分析比特币安全性时，并未考虑比特币支付完整的生命??周期、合作挖矿的交互细节以及跨链交易的过程细节，将比特币协议主体抽象为??共识节点与外界环境，将比特币交易简化为被各节点已同步且验证的消息。然??而，比特币协议实体在不同协议模块实际上承担着不同功能，因此，现有工作对??比特币协议的抽象和简化处理无法满足本文的细粒度要求。??本文将交易相关的比特币节点抽象为商家和买家，其原因在于，生成并提交??
?第２章相关技术???区块?区块?区块??Ｘ?Ａ?／?Ａ?／?／??上一区块哈希??上一区块哈希??上一区块哈希??区块高度?区块髙度?区块高度??馱克尔树根?》尔克ｗｔｓ?狀尔克树根??＼?，??１????＼?＜发起者丨＾＿￥，＾＾名＞?０竺艺，金额，签名＞??＼?／?交》输出「?Ｙ交易输入?２??＼??＝＝ｉ???ｆｕＴＸＯ：?＊?交扮■＿＜■〇：?Ｊ??畎克尔树?ＬＩＥｅ’ｆｉ」??ＵＴＸＯ：未花费交易输出??ｆ哈希１?ｆ哈希＾??Ｃｏｌｎｂａｓｅ＝Ｃｏｉｎｂｉ?＋?Ｅｘｔｒａｎｏｎｃｅｉ?＋?Ｅｘｔｒａｎｏｎｃｅ２?＋?Ｃｏｉｎｂ２??Ｃｏｉｎｂｉ：区块链基本信息??’?Ｃ＾＂＂?＾?１＇＾?｜?Ｅｘｔｒａｎｏｎｃｅｉ：矿池固定标识倍息??哈希?｜哈希?｜哈希?｜哈希｜?Ｃｏｉｎｂ２：矿池矿工收益地址相鍊息??ＶＣｏｉｎｂａｓｅｙ?Ｊ?Ｊ使得ｈａｓｈ（区块）＜?区块最大哈希值??图２．１比特币ＵＴＸＯ交易模型??判断某笔待更新比特币资产是否已被花费，比特币账户地址对应的比特币余额，??即该地址对应所有ＵＴＸＯ中包含的比特币之和。??２．４本章小结??本章描述了区块链技术的基本原理和技术特点，通过介绍区块链的相关技??术，展示了区块链系统维护一条长度递增的链式公共交易账本；概述了比特币的??基础知识，通过介绍比特币的相关技术，展示了比特币节点如何确认并存储所有??发生在比特币网络中的历史交易数据；介绍了诸如工作量证明、难度值、双重支??付以及ＵＴＸＯ交易模型的比特币相关术语。??１９??
本文编号：2995008
【文章来源】：中国科学技术大学安徽省 211工程院校 985工程院校
【文章页数】：82 页
【学位级别】：硕士
【部分图文】：
图１．１现有工作形式化建模简化策略图示??全分析研究人员需要对各协议实体交互逻辑进行强抽象，并基于协议实际的安??
?！?！！?ｒ?＾???Ｉ?????????比特币?安全威胁?一＾?攻击者?一一＾?自动化?—??实际运行环境Ｉ？棋型定义?驗证工具???！??ｌ！?Ｕ￣存在的???！?????！！?安全漏柄??Ｉ?１１?＾?Ｉ??安全研宂人员?￣？安全目标?一＊???＞！?????ｉ：??｛?Ｉ?ｊ??规則抽象与细化的权衡??攻击者能力与证明难度的权衡?｜Ｉ??！?安全厲性集合的充整性?１１??Ｉ?Ｊ?Ｌ?Ｊ??图１．２比特币协议安全性分析整体框架??工，抽象定义了比特币各协议模块的交互细节及其实体功能，本文抽象的协议模??块包括：支付模块、共识模块、合作挖矿模块和跨链交易模块，本文抽象的协议??实体包括：商家、买家、节点、矿池服务器和矿池矿工。虽然比特币白皮书对比??特币协议模块进行了概述，但许多重要的协议交互细节都是被省略或者是过时??的，比特币协议具体实施的参考标准被分散在一系列“比特币改进建议”（ＢＩＰｓ）??以及开发人员的讨论记录中，本文结合实际被部署的比特币协议及其相关源码??及文档完成了对比特币各协议模块及其实体交互的抽象。??现有工作在形式化分析比特币安全性时，并未考虑比特币支付完整的生命??周期、合作挖矿的交互细节以及跨链交易的过程细节，将比特币协议主体抽象为??共识节点与外界环境，将比特币交易简化为被各节点已同步且验证的消息。然??而，比特币协议实体在不同协议模块实际上承担着不同功能，因此，现有工作对??比特币协议的抽象和简化处理无法满足本文的细粒度要求。??本文将交易相关的比特币节点抽象为商家和买家，其原因在于，生成并提交??
?第２章相关技术???区块?区块?区块??Ｘ?Ａ?／?Ａ?／?／??上一区块哈希??上一区块哈希??上一区块哈希??区块高度?区块髙度?区块高度??馱克尔树根?》尔克ｗｔｓ?狀尔克树根??＼?，??１????＼?＜发起者丨＾＿￥，＾＾名＞?０竺艺，金额，签名＞??＼?／?交》输出「?Ｙ交易输入?２??＼??＝＝ｉ???ｆｕＴＸＯ：?＊?交扮■＿＜■〇：?Ｊ??畎克尔树?ＬＩＥｅ’ｆｉ」??ＵＴＸＯ：未花费交易输出??ｆ哈希１?ｆ哈希＾??Ｃｏｌｎｂａｓｅ＝Ｃｏｉｎｂｉ?＋?Ｅｘｔｒａｎｏｎｃｅｉ?＋?Ｅｘｔｒａｎｏｎｃｅ２?＋?Ｃｏｉｎｂ２??Ｃｏｉｎｂｉ：区块链基本信息??’?Ｃ＾＂＂?＾?１＇＾?｜?Ｅｘｔｒａｎｏｎｃｅｉ：矿池固定标识倍息??哈希?｜哈希?｜哈希?｜哈希｜?Ｃｏｉｎｂ２：矿池矿工收益地址相鍊息??ＶＣｏｉｎｂａｓｅｙ?Ｊ?Ｊ使得ｈａｓｈ（区块）＜?区块最大哈希值??图２．１比特币ＵＴＸＯ交易模型??判断某笔待更新比特币资产是否已被花费，比特币账户地址对应的比特币余额，??即该地址对应所有ＵＴＸＯ中包含的比特币之和。??２．４本章小结??本章描述了区块链技术的基本原理和技术特点，通过介绍区块链的相关技??术，展示了区块链系统维护一条长度递增的链式公共交易账本；概述了比特币的??基础知识，通过介绍比特币的相关技术，展示了比特币节点如何确认并存储所有??发生在比特币网络中的历史交易数据；介绍了诸如工作量证明、难度值、双重支??付以及ＵＴＸＯ交易模型的比特币相关术语。??１９??
本文编号：2995008
本文链接：https://www.wllwen.com/shoufeilunwen/xixikjs/2995008.html
