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

王西忠,肖美华,杨科,宋佳雯,朱志亮

(华东交通大学 软件学院, 江西 南昌 330013)

0 引言

区块链是对传统互联网的一种变革，被称作是下一代互联网[1]。混币作为区块链中一种密码货币，受到很大关注并广泛应用于区块链领域中。然而，因混币中第三方的存在，其面临着与传统中心化系统同样的安全问题，可信第三方存在泄漏混币地址之间关联的可能，使得混币操作失去意义[2]。区块链混币机制协议是保证区块链安全和隐私的关键方法，设计安全的区块链混币机制协议尤为重要。区块链混币机制协议是一种匿名通信协议，MIXCOIN协议是一种典型的区块链混币机制协议，由于MIXCOIN协议存在泄漏用户地址关联性的可能，所以MIXCOIN协议不满足匿名性。

为了保证第三方节点的可信度，BONNEAU等[3]提出一种改进的中心化混币方案——MIXCOIN。通过设置审计功能，使用户有权公布签名数据，揭露第三方节点的违规行为，混币服务商将付出失去信誉的代价。但是该方案没有从根源上解除第三方对信息泄露的威胁。VALENTA等[4]在MIXCOIN的基础上使用盲签名技术进一步优化，设计了BLINDCOIN方案，使第三方节点在正常提供混币服务的同时，无法得到所有交易中交易双方的真实信息，从而避免信息泄露的风险。但使用盲签名技术必然会增加混币过程中的计算量。SHENTU等[5]提出一种更加高效的盲签名混币方案，使用椭圆曲线加密算法提升计算效率。2015年上线运营的匿名数字货币达世币(Dash)[6]，从经济学的角度解决中心化混币方案面临的威胁。达世币中执行混币过程的中心节点被称为主节点，所有主节点必须向系统支付1 000达世币(达世币中的数字货币)的押金才能获得执行混币操作的权利。通过设置押金，增加了主节点违规操作的代价。

当前采用形式化方法[7-8]研究安全协议匿名性还处于发展阶段，通常使用形式化方法分析安全协议的认证性和机密性。但安全协议匿名性质却至关重要，因此，形式化分析协议匿名性是一个重要研究领域。

为了形式化地分析安全协议，需要对它们应满足的安全性质进行形式化定义。MORAN等[9]提出了采用CSP方法对协议匿名性质进行形式化定义，并讨论系统的匿名性。FANTI等[10]运用形式化方法分析匿名保证轻量级加密货币网络。BANERJEE等[11]提出了一种新的全球移动网络(GLOMONETs)匿名保护移动用户认证方案。KASSEM等[12]运用π演算的形式化方法分析e-reputation协议的隐私、身份验证和可验证属性等内容。

形式化方法主要分为两类，分别是模型检测[13]和定理证明[14]。SPIN[15]是一种通用的模型检测工具,通过使用LTL(线性时态逻辑), SPIN不仅能够检测系统设计过程中产生的一些逻辑错误，还可以用来验证密码协议是否满足自身刻画的性质。本文提出一种基于模型检测的形式化方法研究MIXCOIN协议匿名性安全问题。

1 MIXCOIN协议形式化抽象表示方法

由于区块链混币机制协议MIXCOIN所具备的特性，使用形式化方法很难对匿名通信协议MIXCOIN进行直接分析。因而，先对MIXCOIN协议进行形式化抽象表示，更好对协议进行分析，协议形式化抽象表示遵循以下规则：

① 简化MIXCOIN协议中实体个数。因区块链中用户数量巨大，混币中心供应商众多，所以将混币机制系统两个实体分为用户(User)和混币中心(Mix)，并简化为User和Mix。

② 约简加解密钥串表示。由于需要对用户和混币中心间消息的发送和接收进行加密解密操作，因而对协议中的加解密钥串约简为K1，K2，K3,…,并记为Key表示加解密钥元组，即Key = {K1,K2,K3,…}；

③ 定义一个比特币转移函数，该函数能够实现用户与混币中心的比特币转移操作；

④ 假设协议使用的密码系统是完备的。在对每一项消息进行加解密时没有缺陷，即只有掌握对应的公钥私钥才能对消息进行加解密操作，并抽象为函数。

通过上述操作，解决MIXCOIN协议难以使用形式化分析和形式化表示的问题。然后对MIXCOIN协议形式化抽象表示，得到MIXCOIN协议的抽象交互模型如图1所示。

图1 MIXCOIN协议抽象交互模型Fig.1 MIXCOIN protocol abstract interaction model

用户User先向混币中心Mix发送混币请求信息，混币中心Mix接受请求后并给用户User返回自己的公钥地址信息，根据图1对MIXCOIN协议再次进行抽象并进行形式化表示如下：

① User→Mix:{V,D,O}ANON Key;

② Mix→User:{P}ANON Key;

③ User:Transfer(V,D,P);

④ Mix:Transfer(V,E,O)。

协议交互中，V表示为一定数量比特币，t1表示截止时间之前用户User向混币中心Mix转移比特币操作，D表示用户User原有公钥地址信息，O表示用户新的公钥地址信息，t2表示截止时间之前混币中心Mix将同样数量的比特币发送给用户User，P表示Mix的旧的收款公钥地址，E为Mix新的公钥地址，Key为密钥元组，ANON()为加密函数，Transfer()是比特币转移函数。

2 MIXCOIN协议建模

MIXCOIN协议建模包括敌手控制消息通道构建,诚实主体建模和攻击者建模。

2.1 敌手控制消息通信模型假设

Dolev-Yao模型是形式化方法中构建攻击者模型的关键，是安全协议模型检测的基础。基于Dolev-Yao模型只能分析特定类型协议，笔者将对其进行改进，使其能够分析匿名通信协议MIXCOIN。先对Dolev-Yao模型引入假设控制通道。如对电子投票协议分析时，则引入的假设控制通道为匿名通信通道。

形式化建模时，通常不对攻击者进行独自建模。参与会话的协议主体间消息发送和接收都是通过环境来实现，攻击者从环境中获取信息，并对信息进行推理，这是攻击者能力的体现。但却无法分析匿名通信类协议，本文通过引入假设敌手控制消息通信对匿名通信协议进行分析。

由于MIXCOIN协议中主体间的通信是通过对应匿名通道来实现的，因此，通过引入敌手控制通道的方式实现主体间匿名通信。敌手控制通信通道的基本原理是两个合法主体间的匿名通信是没有直接通道相连的，即合法主体用户User和混币中心Mix间的信息交换只能通过攻击者来实现，攻击者总是可以窃取和转发合法主体间信息传送，合法主体收到的信息都是通过攻击者完成的。例如，当用户User向混币中心Mix发送混币请求时，实际上是User向攻击者Attacker发送请求信息，而Mix收到的是攻击者发送的请求信息。敌手控制通道建模如图2所示。

图2 敌手控制通信建模Fig.2 Modeling adversary control communications

模型定义的两个通道是用户与攻击者的通道以及混币中心与攻击者的通道。

2.2 诚实主体建模

通过构建数据项的有限集合，方便表示各种数据。有限集合中包含诚实主体名称、关键消息项、加解密钥信息及泛型数据类型，定义描述如下：

mtype={User,Mix,V,D,O,P,E,V2,D2,O2,P2,E2,Key,gD,R}；

集合{V,D,O,P,V2,D2,O2,P2}中的各元素代表协议交互的信息项。其中，E表示混币中心Mix产生的新公钥地址，Key表示加解密钥信息，gD表示为泛型数据类型，R表示不可识别的主体名，后面会对R的作用会做出对应说明。

对协议进行抽象操作，根据不同的信息结构，所构建的敌手控制消息通道也不相同。根据协议消息所需元素数目，对MIXCOIN协议可定义两种敌手控制消息通道：

Chan ch1 =[0]of {mtype, mtype, mtype, mtype, mtype,byte}；

Chan ch2 =[0]of {mtype, mtype, mtype,byte}；

对MIXCOIN协议诚实主体用户User的描述，具体代码为：

proctypeP_User(声明参数){

声明变量g1；

声明变量g2；

atomic {

构建协商双方公钥地址信息函数；

初始化进程；

通过ch1通道接收信息；

}

atomic {

通过ch2通道发送信息ch2；

调用比特币转移函数；

提交进程；

}

}

MIXCOIN协议交互初始时，用户User和混币中心Mix先沟通公钥地址信息，然后定义比特币转移函数Transfer(x,y,z)。通过函数Key_Negotiate()协商双方公钥地址信息，得到对应公钥地址信息后，诚实主体通过假设敌手控制通信ch1，ch2发送和接收对应消息。由于atomic块具有代码顺序执行，不能被外部中断特点。进程P_User()和P_Mix()通过使用语句atomic，将相关操作定义其中，减少进程空间状态迁移量，进而降低状态爆炸风险。进程代码中运用宏定义方式对Ini_Part_UM、Ini_Submit_UM等原子谓词值进行更新操作，具体操作表示如下：

#define Anonymity_Check()//定义匿名性检查函数

定义初始化进程；

定义提交进程；

定义回复进程；

定义回复提交进程。

2.3 运用LTL刻画MIXCOIN协议安全性质

使用LTL公式对MIXCOIN协议的安全性质进行刻画，再使用模型检测工具SPIN进行验证。代码中表示安全性质的布尔值，若为假，则说明协议存在安全漏洞，并产生对应的攻击序列图，若为真，则不产生攻击序列图。

MIXCOIN协议中的认证性是指用户User和混币中心Mix间的相互认证，即完成对应的公钥地址信息交换以及转移一定数量比特币操作。MIXCOIN匿名性是指用户User和混币中心Mix完成比特币转移操作后，用户User输入、输出地址关联性不被泄漏，即用户的输入和输出地址联系不会被混币中心所发现。

MIXCOIN协议的认证性、匿名性使用原子谓词进行描述，其关键全局变量如下：

bit Anonymity_UM=1; //初始化匿名值为1

bit Ini_Part_UM = 0;//初始化进程，进程为0表示该进程未发生

bit Ini_Submit_UM = 0;

bit Res_Part_UM = 0;

bit Res_Submit_UM = 0。

MIXCOIN协议满足认证性表示为：Mix对User的认证，即在Ini_Submit_UM前，Res_Part_UM值必须保持为真；User对Mix的认证，即在Res_Submit_UM前，Ini_Part_UM值必须保持为真。MIXCOIN协议满足匿名性是指Anonymity_UM总保持为真。

用LTL对对应安全性质进行表示如下：

-[]( ([]!Ini_Submit_UM ) || ( !Ini_Submit_UM U Res_Part_UM) )//对进程认证性LTL表示

-[]( ([]!Res_Submit_UM) || ( !Res_Submit_UM U Ini_Part_UM) )

-[]Anonymity_UM//对进程匿名性LTL表示

至此，对MIXCOIN协议的安全性质刻画已完成。下一步是通过模型检测SPIN工具对MIXCOIN协议进行分析验证。

2.4 攻击者建模

本节基于改进的Dolev-Yao攻击者建模方法，引入敌手控制通信，扩展网络通信通道，对MIXCOIN协议的匿名性进行建模。

在两方匿名认证通信协议模型中，定义攻击者进程PI()，通过假设敌手控制通信通道，攻击者通过特定单独通道与各主体进行信息交换。攻击者进程PI()通过ch1和ch2通道接收和发送其他主体所传来的信息，且发送对应信息给其他对应主体。攻击者总能窃取到用户User和混币中心Mix间的信息交互，但只有掌握消息的解密密钥才能对消息进行解密操作，所以模型先对攻击者知识库求解，再对攻击者行为进行描述。

形式化分析MIXCOIN协议，利用敌手控制通道窃取发送信息，表1中为攻击者可学会知识，对不能解密信息进行整条学习操作。

表1 攻击者可学会的知识Tab.1 Attacker can learn knowledge

对用户User和混币中心Mix的接收语句分析，可知攻击者要求学会的知识项信息。

ch1 ? eval(self), g1, g2, g3, eval(Key), eval(User_Key_use);

ch2 ? eval(self), g1, eval(Key), eval(Mix_Key_use)。

其中，接收语句g1、g2、g3取值范围有{(V,D,O,P,E),(V2,D2,O2,P2,E2)}。通过敌手控制通道ch1，攻击者可构建信息项数量为250条；攻击者通过敌手控制通道ch2，可构建10条信息项。表2中为攻击者要求学会知识。

表2 攻击者要求学会的知识Tab.2 Knowledge that the attacker demands to learn

通过表1和表2可知，攻击者获取的最有价值信息是通过两个表中第二列信息交集所得，具体信息如下：

{V,D,O}ANONKey；{V2,D2,O2} ANONKey；{P}ANON Key；{P2}ANONKey

根据以上分析，将攻击者进程定义为PI，行为操作代码如下所示：

proctype PI(){

初始化变量值为0；

初始化变量为0；

攻击者向假设敌手ch1、ch2通道发送消息；

发送不同类型的消息；

构建攻击者库；

接收该类型的消息进行对应的判断；

满足条件后执行k3函数；

接收该类型的消息进行对应的判断；

满足条件后执行k2函数；

执行匿名性检查函数；

}

3 实验结果与分析

对MIXCOIN协议各个主体进程定义后，运用SPIN 5.1.6版本对MIXCOIN协议进行形式化验证分析，得到如图3所示的攻击序列图形。

图3 MIXCOIN协议中的攻击序列Fig.3 Attack sequence in MIXCOIN protocol

根据图3，可发现MIXCOIN协议中存在重放攻击漏洞和中间人攻击漏洞，具体攻击过程如下：

① User→I:{V,D,O}ANON Key

②I→Mix:{V,D,O}ANON Key

③ Mix→I:{P}ANON Key

④I→User:{P}ANON Key

⑤ User→I:{V2,D2,O2}ANON Key

⑥I→Mix:{V2,D2,O2}ANON Key

⑦ Mix→I:{P2}ANON Key

⑧I→User:{P2}ANON Key

⑨I→User:{P}ANON Key(from ③)

⑩I→User:{P2}ANON Key(from ⑦)

用户User运用旧公钥地址与混币中心Mix进行通信并转移对应数量比特币，攻击者通过⑤和⑧信息完成用户User与混币中心Mix间通信。在阶段3完成结束后，用户User和混币中心Mix端的公钥地址均变成{1,3}。然后，攻击者在⑨阶段和⑩阶段进行重放攻击，通过冒充混币中心Mix与用户User进行通信。 混币中心Mix和用户User无法发现攻击者获取用户地址间联系时的信息窃取、篡改和重放操作。MIXCOIN协议定义的相关原子谓词变化及对应变量的值由图4可知。

根据图4中数据，Anonymity_UM值为0，Ini_Part_UM、Res_Part_UM、Ini_Submit_UM、Res_Submit_UM值均为1表示MIXCOIN协议满足认证性但不满足匿名性，即协议存在中间人攻击漏洞和重放攻击漏洞，用户端混币地址的关联性被泄露会导致用户的输入和输出地址映射被攻击者发现。此外，分析MIXCOIN协议基于SPIN的模型检测结果，还能得到系统的更多信息，如图5所示。

图4 MIXCOIN协议性质信息Fig.4 MIXCOIN protocol nature information

由图5可得，对MIXCOIN协议进行形式化验证，花费68字节内存(state-vector)，系统遍历深度(depth reached)为83，性质发生违反(errors为1)存储状态(state stored)数为45，状态迁移(transitions)数为83。在模型检测中各状态属性数值表示验证效率，对应数值越小表明验证效率越高，对应数值越大表明验证效率越低。

图5 MIXCOIN模型验证结果信息Fig.5 MIXCOIN model validation result information

4 总结

在区块链中，完全公开的交易存储机制使区块链交易存在隐私泄露风险，因此有必要在区块链系统中采用相应的隐私保护机制。在满足区块链共识机制的条件下，需要尽可能隐藏数据信息和数据背后的知识，但区块链本身特性给区块链交易的安全带来极大的挑战。因此，为了实现混币机制协议更高的安全性和更丰富的功能，协议还需进一步改进。本文以MIXCOIN协议为例，基于改进的Dolev-Yao攻击者建模方法，通过引入假设敌手控制通道，扩展网络通信假设两个方法分析匿名通信协议，运用线性时态逻辑刻画MIXCOIN协议认证性和匿名性，实现User和Mix主体的公钥地址选择以及转移一定数量比特币操作，最后通过SPIN工具对MIXCOIN协议模型进行形式化验证。实验结果表明，MIXCOIN协议存在中间人攻击漏洞和重放攻击漏洞，会导致用户端混币地址的关联性的泄露，即发送者匿名性不足的情况下用户的输入和输出地址映射易被混币中心发现。下一步研究将尝试对MIXCOIN协议进行改进，并对其安全性进行验证。