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

摘要

区块链混币机制协议是保障区块链安全和隐私的有效手段之一。MIXCOIN协议是一种典型的区块链混币机制协议,针对MIXCOIN协议可能存在泄漏用户地址关联性,导致协议不满足匿名性的问题,提出MIXCOIN协议形式化抽象表示方法,简化协议主体个数,约简加解密钥串表示,定义比特币转移函数,有效地解决了复杂协议难以形式化表示的问题。同时改进Dolev-Yao攻击者建模方法,引入敌手控制通道,可以更好地分析匿名通信协议。运用模型检测工具SPIN对MIXCOIN协议的认证性和匿名性进行验证,结果表明,协议存在中间人攻击和重放攻击,泄漏用户端混币地址的关联性,MIXCOIN协议只满足认证性而不满足匿名性。