基于SPIN的MIXCOIN协议形式化分析与验证  

Formal analysis and verification of MIXCOIN protocol based on SPIN

作　　者：王西忠 肖美华[1] 杨科 宋佳雯 朱志亮 WANG Xi-zhong;XIAO Mei-hua;YANG Ke;SONG Jia-wen;ZHU Zhi-liang(College of Software, East China Jiaotong University, Nanchang 330013, China)

机构地区：[1]华东交通大学软件学院,江西南昌330013

出　　处：《广西大学学报（自然科学版）》2020年第6期1404-1412,共9页Journal of Guangxi University（Natural Science Edition）

基　　金：国家自然科学基金资助项目(61562026,61962020);江西省主要学科学术和技术带头人资助计划项目(20172BCB22015)。

摘　　要：区块链混币机制协议是保障区块链安全和隐私的有效手段之一。MIXCOIN协议是一种典型的区块链混币机制协议,针对MIXCOIN协议可能存在泄漏用户地址关联性,导致协议不满足匿名性的问题,提出MIXCOIN协议形式化抽象表示方法,简化协议主体个数,约简加解密钥串表示,定义比特币转移函数,有效地解决了复杂协议难以形式化表示的问题。同时改进Dolev-Yao攻击者建模方法,引入敌手控制通道,可以更好地分析匿名通信协议。运用模型检测工具SPIN对MIXCOIN协议的认证性和匿名性进行验证,结果表明,协议存在中间人攻击和重放攻击,泄漏用户端混币地址的关联性,MIXCOIN协议只满足认证性而不满足匿名性。Blockchain mixed currency mechanism protocol is one of the effective means to ensure the security and privacy of blockchain.MIXCOIN protocol is a typical blockchain protocol with mixed currency mechanism.In order to solve the problem that MIXCOIN protocol may leak the user address association and cause the protocol not to satisfy anonymity,a formal and abstract representation method for MIXCOIN protocol is proposed.It reduces the number of protocol agents,simplifies the representation of encryption and decryption key strings and defines the bitcoin transfer function,which effectively solves the problem that complex protocols are difficult to be formally represented.At the same time,it improves the modeling method of Dolev-Yao model and introduces the adversary control channel,which can better analyze the anonymous communication protocol.By using the model detection tool SPIN,the authentication and anonymity of the MIXCOIN protocol are verified.The results show that there are man-in-the-middle attack and replay attack in the protocol,and the association of the mixed currency address of the client is revealed.The MIXCOIN protocol only satisfies the authentication but not the anonymity.

关 键 词：混币机制 MIXCOIN协议 匿名性 形式化方法 模型检测 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]