一种比特币支付协议的形式化建模验证方法

A Formal Modeling and Verification Method for Bitcoin Payment Protocol

作为主流的数字加密货币,比特币的安全性受到广泛关注,并且围绕其展开大量的研究工作.然而目前针对比特币支付过程的分析还比较欠缺,缺乏相关的安全标准和精细的建模分析,难以确保相关协议的安全.针对这一问题,基于比特币社区规范与比特币的数字货币功能属性,为比特币支付协议建立了形式化的符号模型与对应的安全属性,并使用自动验证工具Tamarin对相关模型及属性进行了形式化验证,完成了对比特币支付协议的验证工作,并且发现一种未被讨论过的比特币支付协议中的安全威胁,对该问题可能产生的影响进行了分析。

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.