基于SmartVerif的比特币底层协议算力盗取漏洞发现

包象琳; 熊焰; 黄文超; 陈凯杰; 汪万森; 孟昭逸; 徐晓峰; 方贤进

doi:10.12263/DZXB.20201194

您当前的位置：

首页 >

文章列表页 >

基于SmartVerif的比特币底层协议算力盗取漏洞发现

学术论文 | 更新时间：2025-12-08

- 基于SmartVerif的比特币底层协议算力盗取漏洞发现
- Detection of the Computational Power Stealing Attack in Bitcoin Protocols Based on SmartVerif
- 电子学报 2021年49卷第12期页码：2390-2398
- 作者机构：
  
  1.安徽工程大学计算机与信息学院, 安徽芜湖 241000
  2.中国科学技术大学计算机科学与技术学院，安徽合肥 230026
  3.安徽理工大学计算机科学与工程学院，安徽淮南 232001
- 作者简介：
  
  [ "包象琳　女，1994年12月生于安徽芜湖，安徽工程大学计算机与信息学院教师.研究方向包括：区块链，形式化方法，网络与信息安全等.E-mail：baoxianglin@ahpu.edu.cn" ]
  [ "熊焰　男，1960年8月生于安徽合肥，中国科学技术大学计算机科学与技术学院教授、博士生导师.研究方向包括：计算机网络与信息安全，移动计算与移动网络，分布式处理等.E-mail：yxiong@ustc.edu.cn" ]
  [ "黄文超（通讯作者）男，1982年6月生于湖北宜昌，中国科学技术大学计算机科学与技术学院副教授.研究方向包括：信息安全，人工智能，移动计算，网络与系统安全自动化验证技术，Android系统安全等.E-mail：hangwc@ustc.edu.cn" ]
  [ "陈凯杰　男，1997年6月出生于安徽合肥，中国科技大学计算机科学与技术学院在读硕士研究生.研究方向包括：区块链，形式化方法.E-mail：ckjkevin@mail.ustc.edu.cn" ]
  [ "汪万森　男，1995年9月生于安徽合肥，中国科学技术大学计算机科学与技术学院在读博士生.研究方向包括：协议形式化验证，区块链.E-mail：wangws@mail.ustc.edu.cn" ]
  [ "孟昭逸　男，1992年5月生于安徽合肥，中国科学技术大学计算机科学与技术学院博士后研究员.研究方向包括：安卓安全，软件形式化验证等.E-mail：mzy516@ustc.edu.cn" ]
  [ "徐晓峰　男，1992年12月生于安徽芜湖，安徽工程大学计算机与信息学院讲师.研究方向包括：零样本学习，深度学习，机器学习，信息安全等.E-mail：xuxiaofeng@ahpu.edu.cn" ]
  [ "方贤进　男，1970年11月生于安徽舒城，安徽理工大学计算机科学与工程学院教授、博士生导师.研究方向包括：信息安全，数据挖掘等.E-mail：xjfang@aust.edu.cn" ]
- 基金信息：
  
  国家自然科学基金(61972369;61572453;61572454);国家重点研发计划(2018YFB2100300);安徽工程大学校级科研项目(XJKY2020122;XJKY2020119;XJKY2020120);安徽工程大学引进人才科研启动基金项目(2020YQQ062)
- DOI：10.12263/DZXB.20201194
  中图分类号： TP309
- 收稿：2020-10-26，
  
  修回：2021-04-19，
  
  纸质出版：2021-12-25
- 稿件说明：
移动端阅览
包象琳,熊焰,黄文超等.基于SmartVerif的比特币底层协议算力盗取漏洞发现[J].电子学报,2021,49(12):2390-2398.

BAO Xiang-lin,XIONG Yan,HUANG Wen-chao,et al.Detection of the Computational Power Stealing Attack in Bitcoin Protocols Based on SmartVerif[J].ACTA ELECTRONICA SINICA,2021,49(12):2390-2398.
包象琳,熊焰,黄文超等.基于SmartVerif的比特币底层协议算力盗取漏洞发现[J].电子学报,2021,49(12):2390-2398. DOI： 10.12263/DZXB.20201194.

BAO Xiang-lin,XIONG Yan,HUANG Wen-chao,et al.Detection of the Computational Power Stealing Attack in Bitcoin Protocols Based on SmartVerif[J].ACTA ELECTRONICA SINICA,2021,49(12):2390-2398. DOI： 10.12263/DZXB.20201194.

摘要

比特币引入了一种新的P2P(Peer to Peer)交易方法，并依靠其底层协议实现去中心化交易.然而，由于目前缺乏对比特币各底层协议的细粒度形式化分析和系统建模，比特币安全性并未被保证.本文通过设计多维度的比特币安全模型引理和细粒度的比特币模型规则，系统地抽象了多协议组合运行考虑下的比特币协议实体交互，完成了对比特币的形式化符号建模与自动化安全分析.与以前的工作相比，本文更细粒度地建模了比特币协议实体及其相关操作，并全面设计了满足比特币各实体需求的安全属性.此外，本文利用自动化形式化验证系统SmartVerif实现了无需额外手工推导证明的形式化验证实验，通过将本文所建模的符号模型规则与引理作为SmartVerif的输入，发现了比特币底层协议算力盗取攻击.

Abstract

Bitcoin introduces a new P2P(Peer to Peer) trading method to the public and relies on its protocols to achieve decentralization. However

due to the lack of fine-grained formal analysis and systematic modeling of bitcoin

the security of bitcoin protocols is not guaranteed. We provide a comprehensive symbolic analysis of bitcoin protocols. Our work develops bitcoin model rules and model lemmas with the abstraction of in-protocol interactions and inter-protocols interactions. We refine the modeling of bitcoin protocol entities and their related protocol operations compared to the previous work

along with the comprehensive design of the security lemmas that bitcoin protocols should guarantee. The symbolic model rules and lemmas developed in our work are inputted into the automatic formal verification system SmartVerif. We find the computational power stealing attack and no additional manual work is needed for the model verification with the help of the SmartVerif.

关键词

Keywords

references

Nakamoto S . Bitcoin: A peer-to-peer electronic cash system [EB/OL]. https://mronline.org/wp-content/uploads/2018/06/bitcoin.pdf https://mronline.org/wp-content/uploads/2018/06/bitcoin.pdf ， 2020-2-13 .

Tschorsch F , Scheuermann B . Bitcoin and beyond: A technical survey on decentralized digital currencies [J]. IEEE Communications Surveys & Tutorials , 2016 , 18 ( 3 ): 2084 - 2123 .

秦超霞 , 郭兵 , 沈艳 , 等 . 区块链的安全风险评估模型 [J]. 电子学报 , 2021 , 49 ( 1 ): 117 - 124 .

Qin C X , Guo B , Shen Y , et al . Security risk assessment model of blockchain [J]. Acta Electronica Sinica , 2021 , 49 ( 1 ): 117 - 124 . (in Chinese)

陈露 , 相峰 , 孙知信 . 基于属性密码体制的区块链安全技术研究进展 [J]. 电子学报 , 2021 , 49 ( 1 ): 192 - 200 .

Chen L , Xiang F , Sun Z X . A survey of blockchain security technologies based on attribute-based cryptography [J]. Acta Electronica Sinica , 2021 , 49 ( 1 ): 192 - 200 . (in Chinese)

Conti M , Sandeep Kumar E , Lal C , et al . A survey on security and privacy issues of bitcoin [J]. IEEE Communications Surveys & Tutorials , 2018 , 20 ( 4 ): 3416 - 3452 .

Bastiaan M . Preventing the 51%-attack: a stochastic analysis of two phase proof of work in bitcoin [EB/OL]. http://referaat.cs. utwente. nl/conference/22/paper/7473/preventing-the-51-attack-a-stochasticanalysis-of-two-phase-proof-of-work in bitcoin.pdf http://referaat.cs.utwente.nl/conference/22/paper/7473/preventing-the-51-attack-a-stochasticanalysis-of-two-phase-proof-of-workinbitcoin.pdf , 2020-2-14 .

Miller A , LaViola Jr J J . Anonymous byzantine consensus from moderately-hard puzzles: A model for bitcoin [EB/OL]. https://socrates1024.s3.amazonaws.com/consensus.pdf https://socrates1024.s3.amazonaws.com/consensus.pdf , 2020-2-13 .

Eyal I , Sirer E G . Majority is not enough: Bitcoin mining is vulnerable [A]. International Conference on Financial Cryptography and Data Security [C]. Berlin, Heidelberg : Springer , 2014 . 436 - 454 .

Blanchet B . Security protocol verification: Symbolic and computational models [A]. International Conference on Principles of Security and Trust [C]. Tallinn, Estonia : Springer , 2012 . 3 - 29 .

Garay J , Kiayias A , Leonardos N . The bitcoin backbone protocol: Analysis and applications [A]. Annual International Conference on the Theory and Applications of Cryptographic Techniques [C]. Sofia, Bulgaria : Springer , 2015 . 281 - 310 .

Garay J , Kiayias A , Leonardos N . The bitcoin backbone protocol with chains of variable difficulty [A]. Annual International Cryptology Conference [C]. Cham : Springer , 2017 . 291 - 323 .

Kiayias A , Panagiotakos G . Speed-security tradeoffs in blockchain protocols [EB/OL]. https://eprint.iacr.org/2015/1019.pdf https://eprint.iacr.org/2015/1019.pdf , 2016 .

Das P , Faust S , Loss J . A formal treatment of deterministic wallets [A]. Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security [C]. London, United Kingdom : ACM , 2019 . 651 - 668 .

Cremers C , Horvat M , Hoyland J , et al . A comprehensive symbolic analysis of TLS 1.3 [A]. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security [C]. Dallas, Texas, USA : ACM , 2017 . 1773 - 1788 .

Basin D , Dreier J , Hirschi L , et al . A formal analysis of 5G authentication [A]. Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security[ A ]. Toronto , Canada : ACM , 2018 . 1383 - 1396 .

Xiong Y , Su C , Huang W , et al . Smartverif: Push the limit of automation capability of verifying security protocols by dynamic strategies [A]. 29th {USENIX} Security Symposium ({USENIX} Security 20) [C]. USA ： {USENIX} Association , 2020 . 253 - 270 .

Lowe G . A hierarchy of authentication specifications [A]. Proceedings 10th Computer Security Foundations Workshop [C]. Rockport, MA, USA : IEEE , 1997 . 31 - 43 .

üsters R K , Truderung T , Vogt A . Accountability: definition and relation-ship to verifiability [A]. Proceedings of the 17th ACM conference on Computer and Communications Security [C]. Chicago, Illinois, USA : ACM , 2010 . 526 - 535 .

Dreier J , Kassem A , Lafourcade P . Formal analysis of e-cash protocols [A]. 2015 12th International Joint Conference on e-Business and Telecommunications (ICETE)(Volum:04) [C]. Colmar, France : IEEE , 2015 . 65 - 75 .

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

面向LLM开放域问答中多方私有表格筛选：一种MPC可公开聚合审计与动态信誉的增强方法

基于区块链的分层联邦学习系统

基于分片技术的区块链可扩展性研究综述

区块链赋能的战场分布式频谱分配：一种快速匹配算法

基于区块链的RFID供应链产品所有权转移方案