首页 | 本学科首页   官方微博 | 高级检索  
     

基于SmartVerif的比特币底层协议算力盗取漏洞发现
引用本文:包象琳,熊焰,黄文超,陈凯杰,汪万森,孟昭逸,徐晓峰,方贤进.基于SmartVerif的比特币底层协议算力盗取漏洞发现[J].电子学报,2021,49(12):2390-2398.
作者姓名:包象琳  熊焰  黄文超  陈凯杰  汪万森  孟昭逸  徐晓峰  方贤进
作者单位:安徽工程大学计算机与信息学院,安徽芜湖241000;中国科学技术大学计算机科学与技术学院,安徽合肥230026;中国科学技术大学计算机科学与技术学院,安徽合肥230026;安徽工程大学计算机与信息学院,安徽芜湖241000;安徽理工大学计算机科学与工程学院,安徽淮南232001
基金项目:国家自然科学基金;国家自然科学基金;国家自然科学基金;国家重点研发计划;安徽工程大学校级科研项目;安徽工程大学校级科研项目;安徽工程大学校级科研项目;安徽工程大学引进人才科研启动基金
摘    要:比特币引入了一种新的P2P(Peer to Peer)交易方法,并依靠其底层协议实现去中心化交易.然而,由于目前缺乏对比特币各底层协议的细粒度形式化分析和系统建模,比特币安全性并未被保证.本文通过设计多维度的比特币安全模型引理和细粒度的比特币模型规则,系统地抽象了多协议组合运行考虑下的比特币协议实体交互,完成了对比特币的形式化符号建模与自动化安全分析.与以前的工作相比,本文更细粒度地建模了比特币协议实体及其相关操作,并全面设计了满足比特币各实体需求的安全属性.此外,本文利用自动化形式化验证系统SmartVerif实现了无需额外手工推导证明的形式化验证实验,通过将本文所建模的符号模型规则与引理作为SmartVerif的输入,发现了比特币底层协议算力盗取攻击.

关 键 词:比特币  区块链  协议安全  符号模型  形式化分析

Detection of the Computational Power Stealing Attack in Bitcoin Proto-cols 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.Detection of the Computational Power Stealing Attack in Bitcoin Proto-cols Based on SmartVerif[J].Acta Electronica Sinica,2021,49(12):2390-2398.
Authors:BAO Xiang-lin  XIONG Yan  HUANG Wen-chao  CHEN Kai-jie  WANG Wan-sen  MENG Zhao-yi  XU Xiao-feng  FANG Xian-jin
Abstract:
Keywords:
本文献已被 万方数据 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号