Detection of the Computational Power Stealing Attack in Bitcoin Protocols Based on SmartVerif

BAO Xiang-lin; XIONG Yan; HUANG Wen-chao; CHEN Kai-jie; WANG Wan-sen; MENG Zhao-yi; XU Xiao-feng; FANG Xian-jin

doi:10.12263/DZXB.20201194

您当前的位置：

首页 >

文章列表页 >

Detection of the Computational Power Stealing Attack in Bitcoin Protocols Based on SmartVerif

PAPERS | 更新时间：2025-12-08

- Detection of the Computational Power Stealing Attack in Bitcoin Protocols Based on SmartVerif
- ACTA ELECTRONICA SINICA Vol. 49, Issue 12, Pages: 2390-2398(2021)
- 作者机构：
  
  1.安徽工程大学计算机与信息学院, 安徽芜湖 241000
  2.中国科学技术大学计算机科学与技术学院，安徽合肥 230026
  3.安徽理工大学计算机科学与工程学院，安徽淮南 232001
- 作者简介：
- 基金信息：
- DOI：10.12263/DZXB.20201194
  CLC： TP309
- Received：26 October 2020，
  
  Revised：2021-04-19，
  
  Published：25 December 2021
- 稿件说明：
移动端阅览
包象琳,熊焰,黄文超等.基于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 .

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Multi-Party Private Table Screening for LLM-Driven ODQA: An Enhanced Method with MPC, Publicly Aggregable Audit, and Dynamic Reputation

Blockchain-Based Hierarchical Federated Learning System

Research on Scalability of Blockchain Based on Sharding: A Survey

Blockchain-Enabled Distributed Spectrum Allocation in Battlefield: A Fast Matching Algorithm

Product Ownership Transfer Scheme of RFID-Enabled Supply Chain Based on Blockchain

Related Author

HU Rui

WU Hao

PAN Yu-xuan

ZHANG Lin

LIU Yu

ZHU Kong-lin

HU Rong-lei

LIU Si-hui

Related Institution

Department of Artificial Intelligence, Beijing University of Posts and Telecommunications

Department of Electronics and Information Engineering, Beijing Electronic Science and Technology Institute

School of Computer Science, Nanjing University of Posts and Telecommunications

School of Mechanical Engineering, Nanjing University of Science and Technology

School of Electronic and Optical Engineering, Nanjing University of Science and Technology

⁰