学术论文DOl:10.12379/j.issn.2096-1057.2024.04.04ResearchPapers一种比特币支付协议的形式化建模验证方法王炯涵黄文超汪万森熊焰（中国科学技术大学计算机科学与技术学院(wangjhl@mail.ustc.edu.cn)AFormalModelingandVerificationMethodforBitcoinPaymentProtocol完合肥230026)WangJionghan,HuangWenchao,WangWansen,andXiongYan(CollegeofComputerScienceandTechnology,UniversityofScienceandTechnologyofChina,Hefei230026)AbstractAsamainstreamdigitalCryptocurrency,thesecurityofBitcoinhadreceivedwidespreadattention,withsignificantresearchconductedaroundit.However,thereiscurrentlyalackofanalysisontheBitcoinpaymentprocess,alongwithadeficiencyinrelevantsecuritystandardsanddetailedmodelinganalysis,makingitchallengingtoensurethesecurityofrelevantprotocols.Addressingthisissue,thisstudybeganwiththeconceptofconsensusandestablishedasymbolicmodeloftheBitcoinpaymentprotocolbasedontheBitcoincommunityspecificationandBitcoin'sdigitalcurrencyattributes.Correspondingadversarymodelsandsecurityattributeswereproposed.FinallytherelevantmodelsunderwentformalvalidationusingtheautomaticverificationtoolTamarin,completingtheverificationprocessoftheBitcoinpaymentprotocol.Consequently,asecurityvulnerabilityintheBitcoinpaymentprotocolwasdiscovered.Thepotentialimpactofthisvulnerabilitywerediscussed.Keywordsbitcoin;formalverification;networkprotocolsecurity;paymentprocess;symbolicmodel摘要作为主流的数字加密货币，比特币的安全性受到广泛关注，并且围绕其展开大量的研究工作.然而目前针对比特币支付过程的分析还比较欠缺，缺乏相关的安全标准和精细的建模分析，难以确保相关协议的安全.针对这一问题，基于比特币社区规范与比特币的数字货币功能属性，为比特币支付协议建立了形式化的符号模型与对应的安全属性，并使用自动验证工具Tamarin对相关模型及属性进行了形式化验证，完成了对比特币支付协议的验证工作，并且发现一种未被讨论过的比特币支付协议中的安全威胁，对该问题可能产生的影响进行了分析。关键词比特币；形式化验证；网络协议安全；支付过程；符号模型中图法分类号TP309收稿日期：2023-09-21基金项目：国家重点研发计划项目（2021QY2104）；中央高校基本科研业务费...
