区块链是对传统互联网的一种变革,被称作是下一代互联网。混币作为区块链中一种密码货币,受到很大关注并广泛应用于区块链领域中。然而,因混币中第三方的存在,其面临着与传统中心化系统同样的安全问题,可信第三方存在泄漏混币地址之间关联的可能,使得混币操作失去意义。区块链混币机制协议是保证区块链安全和隐私的关键方法,设计安全的区块链混币机制协议尤为重要。区块链混币机制协议是一种匿名通信协议,形式化分析区块链混币机制协议匿名性还处于发展阶段。MIXCOIN协议是一种典型的区块链混币机制协议,针对MIXCOIN协议存在可能泄漏用户地址关联性,使得MIXCOIN协议不满足匿名性。本文提出一种基于模型检测的形式化方法研究MIXCOIN协议匿名性安全问题。论文主要工作如下:(1)提出MIXCOIN协议形式化抽象表示方法。该方法在假设协议使用的密码系统是完备的情况下,首先简化MIXCOIN协议中实体个数,其次约简加解密钥串表示,最后定义比特币转移函数。通过该方法解决MIXCOIN协议难以使用形式化分析和形式化表示问题。(2)改进Dolev-Yao攻击者建模方法。该方法通过引入敌手控制通道,对网络通信假设进行扩展,可以更好地分析匿名通信协议。采用改进后的Dolev-Yao攻击者建模方法对MIXCOIN协议进行建模,运用线性时态逻辑对MIXCOIN协议性质进行刻画,通过SPIN工具对协议验证,实验生成攻击序列图,表明MIXCOIN协议不满足匿名性。(3)提出基于椭圆曲线盲签名机制和数组方式,对MIXCOIN协议关键信息进行盲签名和公钥地址更新的改进方法。该方法在椭圆曲线盲签名机制基础上引入辅助进程通道操作,通过该辅助进程通道实现协议盲签操作,同时用数组方式模拟实现公钥地址更新操作,可以更好地分析改进协议。MIXCOIN协议在消息项内增加盲签名操作和用数组方式模拟实现公钥地址更新操作,利用敌手控制通道,对改进后的MIXCOIN协议进行建模,通过SPIN验证,实验得出改进后的MIXCOIN协议是安全的,匿名性更强。本文所提出MIXCOIN协议形式化抽象表示方法以及改进的Dolev-Yao攻击者建模方法对此类区块链混币机制协议形式化分析具有重要意义;提出采用椭圆曲线盲签名机制对协议关键信息进行盲签名和用数组方式模拟实现公钥地址更新的改进方法,并引入辅助进程通道实现协议盲签操作,证明能提高协议发送者匿名性。可用于此类区块链混币机制协议的设计与分析。