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

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.