信息安全研究2024，Vol.10Issue(4)：311-317,7.DOI:10.12379/j.issn.2096-1057.2024.04.04
一种比特币支付协议的形式化建模验证方法
A Formal Modeling and Verification Method for Bitcoin Payment Protocol
摘要
Abstract
As a mainstream digital Cryptocurrency,the security of Bitcoin had received widespread attention,with significant research conducted around it.However,there is currently a lack of analysis on the Bitcoin payment process,along with a deficiency in relevant security standards and detailed modeling analysis,making it challenging to ensure the security of relevant protocols.Addressing this issue,this study began with the concept of consensus and established a symbolic model of the Bitcoin payment protocol based on the Bitcoin community specification and Bitcoin's digital currency attributes.Corresponding adversary models and security attributes were proposed.Finally the relevant models underwent formal validation using the automatic verification tool Tamarin,completing the verification process of the Bitcoin payment protocol.Consequently,a security vulnerability in the Bitcoin payment protocol was discovered.The potential impact of this vulnerability were discussed.关键词
比特币/形式化验证/网络协议安全/支付过程/符号模型Key words
bitcoin/formal verification/network protocol security/payment process/symbolic model分类
信息技术与安全科学引用本文复制引用
王炯涵,黄文超,汪万森,熊焰..一种比特币支付协议的形式化建模验证方法[J].信息安全研究,2024,10(4):311-317,7.基金项目
国家重点研发计划项目(2021QY2104) （2021QY2104）
中央高校基本科研业务费专项资金项目(WK2150110024) （WK2150110024）
国家自然科学基金项目(61972369,62102385,62372422) （61972369,62102385,62372422）
安徽省自然科学基金项目(2108085QF262) （2108085QF262）
