王西忠,肖美華,楊科,宋佳雯,朱志亮

(華東交通大學(xué) 軟件學(xué)院, 江西 南昌 330013)

0 引言

區(qū)塊鏈?zhǔn)菍?duì)傳統(tǒng)互聯(lián)網(wǎng)的一種變革，被稱作是下一代互聯(lián)網(wǎng)[1]?；鞄抛鳛閰^(qū)塊鏈中一種密碼貨幣，受到很大關(guān)注并廣泛應(yīng)用于區(qū)塊鏈領(lǐng)域中。然而，因混幣中第三方的存在，其面臨著與傳統(tǒng)中心化系統(tǒng)同樣的安全問(wèn)題，可信第三方存在泄漏混幣地址之間關(guān)聯(lián)的可能，使得混幣操作失去意義[2]。區(qū)塊鏈混幣機(jī)制協(xié)議是保證區(qū)塊鏈安全和隱私的關(guān)鍵方法，設(shè)計(jì)安全的區(qū)塊鏈混幣機(jī)制協(xié)議尤為重要。區(qū)塊鏈混幣機(jī)制協(xié)議是一種匿名通信協(xié)議，MIXCOIN協(xié)議是一種典型的區(qū)塊鏈混幣機(jī)制協(xié)議，由于MIXCOIN協(xié)議存在泄漏用戶地址關(guān)聯(lián)性的可能，所以MIXCOIN協(xié)議不滿足匿名性。

為了保證第三方節(jié)點(diǎn)的可信度，BONNEAU等[3]提出一種改進(jìn)的中心化混幣方案——MIXCOIN。通過(guò)設(shè)置審計(jì)功能，使用戶有權(quán)公布簽名數(shù)據(jù)，揭露第三方節(jié)點(diǎn)的違規(guī)行為，混幣服務(wù)商將付出失去信譽(yù)的代價(jià)。但是該方案沒(méi)有從根源上解除第三方對(duì)信息泄露的威脅。VALENTA等[4]在MIXCOIN的基礎(chǔ)上使用盲簽名技術(shù)進(jìn)一步優(yōu)化，設(shè)計(jì)了BLINDCOIN方案，使第三方節(jié)點(diǎn)在正常提供混幣服務(wù)的同時(shí)，無(wú)法得到所有交易中交易雙方的真實(shí)信息，從而避免信息泄露的風(fēng)險(xiǎn)。但使用盲簽名技術(shù)必然會(huì)增加混幣過(guò)程中的計(jì)算量。SHENTU等[5]提出一種更加高效的盲簽名混幣方案，使用橢圓曲線加密算法提升計(jì)算效率。2015年上線運(yùn)營(yíng)的匿名數(shù)字貨幣達(dá)世幣(Dash)[6]，從經(jīng)濟(jì)學(xué)的角度解決中心化混幣方案面臨的威脅。達(dá)世幣中執(zhí)行混幣過(guò)程的中心節(jié)點(diǎn)被稱為主節(jié)點(diǎn)，所有主節(jié)點(diǎn)必須向系統(tǒng)支付1 000達(dá)世幣(達(dá)世幣中的數(shù)字貨幣)的押金才能獲得執(zhí)行混幣操作的權(quán)利。通過(guò)設(shè)置押金，增加了主節(jié)點(diǎn)違規(guī)操作的代價(jià)。

當(dāng)前采用形式化方法[7-8]研究安全協(xié)議匿名性還處于發(fā)展階段，通常使用形式化方法分析安全協(xié)議的認(rèn)證性和機(jī)密性。但安全協(xié)議匿名性質(zhì)卻至關(guān)重要，因此，形式化分析協(xié)議匿名性是一個(gè)重要研究領(lǐng)域。

為了形式化地分析安全協(xié)議，需要對(duì)它們應(yīng)滿足的安全性質(zhì)進(jìn)行形式化定義。MORAN等[9]提出了采用CSP方法對(duì)協(xié)議匿名性質(zhì)進(jìn)行形式化定義，并討論系統(tǒng)的匿名性。FANTI等[10]運(yùn)用形式化方法分析匿名保證輕量級(jí)加密貨幣網(wǎng)絡(luò)。BANERJEE等[11]提出了一種新的全球移動(dòng)網(wǎng)絡(luò)(GLOMONETs)匿名保護(hù)移動(dòng)用戶認(rèn)證方案。KASSEM等[12]運(yùn)用π演算的形式化方法分析e-reputation協(xié)議的隱私、身份驗(yàn)證和可驗(yàn)證屬性等內(nèi)容。

形式化方法主要分為兩類，分別是模型檢測(cè)[13]和定理證明[14]。SPIN[15]是一種通用的模型檢測(cè)工具,通過(guò)使用LTL(線性時(shí)態(tài)邏輯), SPIN不僅能夠檢測(cè)系統(tǒng)設(shè)計(jì)過(guò)程中產(chǎn)生的一些邏輯錯(cuò)誤，還可以用來(lái)驗(yàn)證密碼協(xié)議是否滿足自身刻畫(huà)的性質(zhì)。本文提出一種基于模型檢測(cè)的形式化方法研究MIXCOIN協(xié)議匿名性安全問(wèn)題。

1 MIXCOIN協(xié)議形式化抽象表示方法

由于區(qū)塊鏈混幣機(jī)制協(xié)議MIXCOIN所具備的特性，使用形式化方法很難對(duì)匿名通信協(xié)議MIXCOIN進(jìn)行直接分析。因而，先對(duì)MIXCOIN協(xié)議進(jìn)行形式化抽象表示，更好對(duì)協(xié)議進(jìn)行分析，協(xié)議形式化抽象表示遵循以下規(guī)則：

① 簡(jiǎn)化MIXCOIN協(xié)議中實(shí)體個(gè)數(shù)。因區(qū)塊鏈中用戶數(shù)量巨大，混幣中心供應(yīng)商眾多，所以將混幣機(jī)制系統(tǒng)兩個(gè)實(shí)體分為用戶(User)和混幣中心(Mix)，并簡(jiǎn)化為User和Mix。

② 約簡(jiǎn)加解密鑰串表示。由于需要對(duì)用戶和混幣中心間消息的發(fā)送和接收進(jìn)行加密解密操作，因而對(duì)協(xié)議中的加解密鑰串約簡(jiǎn)為K1，K2，K3,…,并記為Key表示加解密鑰元組，即Key = {K1,K2,K3,…}；

③ 定義一個(gè)比特幣轉(zhuǎn)移函數(shù)，該函數(shù)能夠?qū)崿F(xiàn)用戶與混幣中心的比特幣轉(zhuǎn)移操作；

④ 假設(shè)協(xié)議使用的密碼系統(tǒng)是完備的。在對(duì)每一項(xiàng)消息進(jìn)行加解密時(shí)沒(méi)有缺陷，即只有掌握對(duì)應(yīng)的公鑰私鑰才能對(duì)消息進(jìn)行加解密操作，并抽象為函數(shù)。

通過(guò)上述操作，解決MIXCOIN協(xié)議難以使用形式化分析和形式化表示的問(wèn)題。然后對(duì)MIXCOIN協(xié)議形式化抽象表示，得到MIXCOIN協(xié)議的抽象交互模型如圖1所示。

圖1 MIXCOIN協(xié)議抽象交互模型Fig.1 MIXCOIN protocol abstract interaction model

用戶User先向混幣中心Mix發(fā)送混幣請(qǐng)求信息，混幣中心Mix接受請(qǐng)求后并給用戶User返回自己的公鑰地址信息，根據(jù)圖1對(duì)MIXCOIN協(xié)議再次進(jìn)行抽象并進(jìn)行形式化表示如下：

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

② Mix→User:{P}ANON Key;

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

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

協(xié)議交互中，V表示為一定數(shù)量比特幣，t1表示截止時(shí)間之前用戶User向混幣中心Mix轉(zhuǎn)移比特幣操作，D表示用戶User原有公鑰地址信息，O表示用戶新的公鑰地址信息，t2表示截止時(shí)間之前混幣中心Mix將同樣數(shù)量的比特幣發(fā)送給用戶User，P表示Mix的舊的收款公鑰地址，E為Mix新的公鑰地址，Key為密鑰元組，ANON()為加密函數(shù)，Transfer()是比特幣轉(zhuǎn)移函數(shù)。

2 MIXCOIN協(xié)議建模

MIXCOIN協(xié)議建模包括敵手控制消息通道構(gòu)建,誠(chéng)實(shí)主體建模和攻擊者建模。

2.1 敵手控制消息通信模型假設(shè)

Dolev-Yao模型是形式化方法中構(gòu)建攻擊者模型的關(guān)鍵，是安全協(xié)議模型檢測(cè)的基礎(chǔ)?；贒olev-Yao模型只能分析特定類型協(xié)議，筆者將對(duì)其進(jìn)行改進(jìn)，使其能夠分析匿名通信協(xié)議MIXCOIN。先對(duì)Dolev-Yao模型引入假設(shè)控制通道。如對(duì)電子投票協(xié)議分析時(shí)，則引入的假設(shè)控制通道為匿名通信通道。

形式化建模時(shí)，通常不對(duì)攻擊者進(jìn)行獨(dú)自建模。參與會(huì)話的協(xié)議主體間消息發(fā)送和接收都是通過(guò)環(huán)境來(lái)實(shí)現(xiàn)，攻擊者從環(huán)境中獲取信息，并對(duì)信息進(jìn)行推理，這是攻擊者能力的體現(xiàn)。但卻無(wú)法分析匿名通信類協(xié)議，本文通過(guò)引入假設(shè)敵手控制消息通信對(duì)匿名通信協(xié)議進(jìn)行分析。

由于MIXCOIN協(xié)議中主體間的通信是通過(guò)對(duì)應(yīng)匿名通道來(lái)實(shí)現(xiàn)的，因此，通過(guò)引入敵手控制通道的方式實(shí)現(xiàn)主體間匿名通信。敵手控制通信通道的基本原理是兩個(gè)合法主體間的匿名通信是沒(méi)有直接通道相連的，即合法主體用戶User和混幣中心Mix間的信息交換只能通過(guò)攻擊者來(lái)實(shí)現(xiàn)，攻擊者總是可以竊取和轉(zhuǎn)發(fā)合法主體間信息傳送，合法主體收到的信息都是通過(guò)攻擊者完成的。例如，當(dāng)用戶User向混幣中心Mix發(fā)送混幣請(qǐng)求時(shí)，實(shí)際上是User向攻擊者Attacker發(fā)送請(qǐng)求信息，而Mix收到的是攻擊者發(fā)送的請(qǐng)求信息。敵手控制通道建模如圖2所示。

圖2 敵手控制通信建模Fig.2 Modeling adversary control communications

模型定義的兩個(gè)通道是用戶與攻擊者的通道以及混幣中心與攻擊者的通道。

2.2 誠(chéng)實(shí)主體建模

通過(guò)構(gòu)建數(shù)據(jù)項(xiàng)的有限集合，方便表示各種數(shù)據(jù)。有限集合中包含誠(chéng)實(shí)主體名稱、關(guān)鍵消息項(xiàng)、加解密鑰信息及泛型數(shù)據(jù)類型，定義描述如下：

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

集合{V,D,O,P,V2,D2,O2,P2}中的各元素代表協(xié)議交互的信息項(xiàng)。其中，E表示混幣中心Mix產(chǎn)生的新公鑰地址，Key表示加解密鑰信息，gD表示為泛型數(shù)據(jù)類型，R表示不可識(shí)別的主體名，后面會(huì)對(duì)R的作用會(huì)做出對(duì)應(yīng)說(shuō)明。

對(duì)協(xié)議進(jìn)行抽象操作，根據(jù)不同的信息結(jié)構(gòu)，所構(gòu)建的敵手控制消息通道也不相同。根據(jù)協(xié)議消息所需元素?cái)?shù)目，對(duì)MIXCOIN協(xié)議可定義兩種敵手控制消息通道：

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

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

對(duì)MIXCOIN協(xié)議誠(chéng)實(shí)主體用戶User的描述，具體代碼為：

proctypeP_User(聲明參數(shù)){

聲明變量g1；

聲明變量g2；

atomic {

構(gòu)建協(xié)商雙方公鑰地址信息函數(shù)；

初始化進(jìn)程；

通過(guò)ch1通道接收信息；

}

atomic {

通過(guò)ch2通道發(fā)送信息ch2；

調(diào)用比特幣轉(zhuǎn)移函數(shù)；

提交進(jìn)程；

}

}

MIXCOIN協(xié)議交互初始時(shí)，用戶User和混幣中心Mix先溝通公鑰地址信息，然后定義比特幣轉(zhuǎn)移函數(shù)Transfer(x,y,z)。通過(guò)函數(shù)Key_Negotiate()協(xié)商雙方公鑰地址信息，得到對(duì)應(yīng)公鑰地址信息后，誠(chéng)實(shí)主體通過(guò)假設(shè)敵手控制通信ch1，ch2發(fā)送和接收對(duì)應(yīng)消息。由于atomic塊具有代碼順序執(zhí)行，不能被外部中斷特點(diǎn)。進(jìn)程P_User()和P_Mix()通過(guò)使用語(yǔ)句atomic，將相關(guān)操作定義其中，減少進(jìn)程空間狀態(tài)遷移量，進(jìn)而降低狀態(tài)爆炸風(fēng)險(xiǎn)。進(jìn)程代碼中運(yùn)用宏定義方式對(duì)Ini_Part_UM、Ini_Submit_UM等原子謂詞值進(jìn)行更新操作，具體操作表示如下：

#define Anonymity_Check()//定義匿名性檢查函數(shù)

定義初始化進(jìn)程；

定義提交進(jìn)程；

定義回復(fù)進(jìn)程；

定義回復(fù)提交進(jìn)程。

2.3 運(yùn)用LTL刻畫(huà)MIXCOIN協(xié)議安全性質(zhì)

使用LTL公式對(duì)MIXCOIN協(xié)議的安全性質(zhì)進(jìn)行刻畫(huà)，再使用模型檢測(cè)工具SPIN進(jìn)行驗(yàn)證。代碼中表示安全性質(zhì)的布爾值，若為假，則說(shuō)明協(xié)議存在安全漏洞，并產(chǎn)生對(duì)應(yīng)的攻擊序列圖，若為真，則不產(chǎn)生攻擊序列圖。

MIXCOIN協(xié)議中的認(rèn)證性是指用戶User和混幣中心Mix間的相互認(rèn)證，即完成對(duì)應(yīng)的公鑰地址信息交換以及轉(zhuǎn)移一定數(shù)量比特幣操作。MIXCOIN匿名性是指用戶User和混幣中心Mix完成比特幣轉(zhuǎn)移操作后，用戶User輸入、輸出地址關(guān)聯(lián)性不被泄漏，即用戶的輸入和輸出地址聯(lián)系不會(huì)被混幣中心所發(fā)現(xiàn)。

MIXCOIN協(xié)議的認(rèn)證性、匿名性使用原子謂詞進(jìn)行描述，其關(guān)鍵全局變量如下：

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

bit Ini_Part_UM = 0;//初始化進(jìn)程，進(jìn)程為0表示該進(jìn)程未發(fā)生

bit Ini_Submit_UM = 0;

bit Res_Part_UM = 0;

bit Res_Submit_UM = 0。

MIXCOIN協(xié)議滿足認(rèn)證性表示為：Mix對(duì)User的認(rèn)證，即在Ini_Submit_UM前，Res_Part_UM值必須保持為真；User對(duì)Mix的認(rèn)證，即在Res_Submit_UM前，Ini_Part_UM值必須保持為真。MIXCOIN協(xié)議滿足匿名性是指Anonymity_UM總保持為真。

用LTL對(duì)對(duì)應(yīng)安全性質(zhì)進(jìn)行表示如下：

-[]( ([]!Ini_Submit_UM ) || ( !Ini_Submit_UM U Res_Part_UM) )//對(duì)進(jìn)程認(rèn)證性LTL表示

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

-[]Anonymity_UM//對(duì)進(jìn)程匿名性LTL表示

至此，對(duì)MIXCOIN協(xié)議的安全性質(zhì)刻畫(huà)已完成。下一步是通過(guò)模型檢測(cè)SPIN工具對(duì)MIXCOIN協(xié)議進(jìn)行分析驗(yàn)證。

2.4 攻擊者建模

本節(jié)基于改進(jìn)的Dolev-Yao攻擊者建模方法，引入敵手控制通信，擴(kuò)展網(wǎng)絡(luò)通信通道，對(duì)MIXCOIN協(xié)議的匿名性進(jìn)行建模。

在兩方匿名認(rèn)證通信協(xié)議模型中，定義攻擊者進(jìn)程PI()，通過(guò)假設(shè)敵手控制通信通道，攻擊者通過(guò)特定單獨(dú)通道與各主體進(jìn)行信息交換。攻擊者進(jìn)程PI()通過(guò)ch1和ch2通道接收和發(fā)送其他主體所傳來(lái)的信息，且發(fā)送對(duì)應(yīng)信息給其他對(duì)應(yīng)主體。攻擊者總能竊取到用戶User和混幣中心Mix間的信息交互，但只有掌握消息的解密密鑰才能對(duì)消息進(jìn)行解密操作，所以模型先對(duì)攻擊者知識(shí)庫(kù)求解，再對(duì)攻擊者行為進(jìn)行描述。

形式化分析MIXCOIN協(xié)議，利用敵手控制通道竊取發(fā)送信息，表1中為攻擊者可學(xué)會(huì)知識(shí)，對(duì)不能解密信息進(jìn)行整條學(xué)習(xí)操作。

表1 攻擊者可學(xué)會(huì)的知識(shí)Tab.1 Attacker can learn knowledge

對(duì)用戶User和混幣中心Mix的接收語(yǔ)句分析，可知攻擊者要求學(xué)會(huì)的知識(shí)項(xiàng)信息。

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

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

其中，接收語(yǔ)句g1、g2、g3取值范圍有{(V,D,O,P,E),(V2,D2,O2,P2,E2)}。通過(guò)敵手控制通道ch1，攻擊者可構(gòu)建信息項(xiàng)數(shù)量為250條；攻擊者通過(guò)敵手控制通道ch2，可構(gòu)建10條信息項(xiàng)。表2中為攻擊者要求學(xué)會(huì)知識(shí)。

表2 攻擊者要求學(xué)會(huì)的知識(shí)Tab.2 Knowledge that the attacker demands to learn

通過(guò)表1和表2可知，攻擊者獲取的最有價(jià)值信息是通過(guò)兩個(gè)表中第二列信息交集所得，具體信息如下：

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

根據(jù)以上分析，將攻擊者進(jìn)程定義為PI，行為操作代碼如下所示：

proctype PI(){

初始化變量值為0；

初始化變量為0；

攻擊者向假設(shè)敵手ch1、ch2通道發(fā)送消息；

發(fā)送不同類型的消息；

構(gòu)建攻擊者庫(kù)；

接收該類型的消息進(jìn)行對(duì)應(yīng)的判斷；

滿足條件后執(zhí)行k3函數(shù)；

接收該類型的消息進(jìn)行對(duì)應(yīng)的判斷；

滿足條件后執(zhí)行k2函數(shù)；

執(zhí)行匿名性檢查函數(shù)；

}

3 實(shí)驗(yàn)結(jié)果與分析

對(duì)MIXCOIN協(xié)議各個(gè)主體進(jìn)程定義后，運(yùn)用SPIN 5.1.6版本對(duì)MIXCOIN協(xié)議進(jìn)行形式化驗(yàn)證分析，得到如圖3所示的攻擊序列圖形。

圖3 MIXCOIN協(xié)議中的攻擊序列Fig.3 Attack sequence in MIXCOIN protocol

根據(jù)圖3，可發(fā)現(xiàn)MIXCOIN協(xié)議中存在重放攻擊漏洞和中間人攻擊漏洞，具體攻擊過(guò)程如下：

① 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運(yùn)用舊公鑰地址與混幣中心Mix進(jìn)行通信并轉(zhuǎn)移對(duì)應(yīng)數(shù)量比特幣，攻擊者通過(guò)⑤和⑧信息完成用戶User與混幣中心Mix間通信。在階段3完成結(jié)束后，用戶User和混幣中心Mix端的公鑰地址均變成{1,3}。然后，攻擊者在⑨階段和⑩階段進(jìn)行重放攻擊，通過(guò)冒充混幣中心Mix與用戶User進(jìn)行通信。 混幣中心Mix和用戶User無(wú)法發(fā)現(xiàn)攻擊者獲取用戶地址間聯(lián)系時(shí)的信息竊取、篡改和重放操作。MIXCOIN協(xié)議定義的相關(guān)原子謂詞變化及對(duì)應(yīng)變量的值由圖4可知。

根據(jù)圖4中數(shù)據(jù)，Anonymity_UM值為0，Ini_Part_UM、Res_Part_UM、Ini_Submit_UM、Res_Submit_UM值均為1表示MIXCOIN協(xié)議滿足認(rèn)證性但不滿足匿名性，即協(xié)議存在中間人攻擊漏洞和重放攻擊漏洞，用戶端混幣地址的關(guān)聯(lián)性被泄露會(huì)導(dǎo)致用戶的輸入和輸出地址映射被攻擊者發(fā)現(xiàn)。此外，分析MIXCOIN協(xié)議基于SPIN的模型檢測(cè)結(jié)果，還能得到系統(tǒng)的更多信息，如圖5所示。

圖4 MIXCOIN協(xié)議性質(zhì)信息Fig.4 MIXCOIN protocol nature information

由圖5可得，對(duì)MIXCOIN協(xié)議進(jìn)行形式化驗(yàn)證，花費(fèi)68字節(jié)內(nèi)存(state-vector)，系統(tǒng)遍歷深度(depth reached)為83，性質(zhì)發(fā)生違反(errors為1)存儲(chǔ)狀態(tài)(state stored)數(shù)為45，狀態(tài)遷移(transitions)數(shù)為83。在模型檢測(cè)中各狀態(tài)屬性數(shù)值表示驗(yàn)證效率，對(duì)應(yīng)數(shù)值越小表明驗(yàn)證效率越高，對(duì)應(yīng)數(shù)值越大表明驗(yàn)證效率越低。

圖5 MIXCOIN模型驗(yàn)證結(jié)果信息Fig.5 MIXCOIN model validation result information

4 總結(jié)

在區(qū)塊鏈中，完全公開(kāi)的交易存儲(chǔ)機(jī)制使區(qū)塊鏈交易存在隱私泄露風(fēng)險(xiǎn)，因此有必要在區(qū)塊鏈系統(tǒng)中采用相應(yīng)的隱私保護(hù)機(jī)制。在滿足區(qū)塊鏈共識(shí)機(jī)制的條件下，需要盡可能隱藏?cái)?shù)據(jù)信息和數(shù)據(jù)背后的知識(shí)，但區(qū)塊鏈本身特性給區(qū)塊鏈交易的安全帶來(lái)極大的挑戰(zhàn)。因此，為了實(shí)現(xiàn)混幣機(jī)制協(xié)議更高的安全性和更豐富的功能，協(xié)議還需進(jìn)一步改進(jìn)。本文以MIXCOIN協(xié)議為例，基于改進(jìn)的Dolev-Yao攻擊者建模方法，通過(guò)引入假設(shè)敵手控制通道，擴(kuò)展網(wǎng)絡(luò)通信假設(shè)兩個(gè)方法分析匿名通信協(xié)議，運(yùn)用線性時(shí)態(tài)邏輯刻畫(huà)MIXCOIN協(xié)議認(rèn)證性和匿名性，實(shí)現(xiàn)User和Mix主體的公鑰地址選擇以及轉(zhuǎn)移一定數(shù)量比特幣操作，最后通過(guò)SPIN工具對(duì)MIXCOIN協(xié)議模型進(jìn)行形式化驗(yàn)證。實(shí)驗(yàn)結(jié)果表明，MIXCOIN協(xié)議存在中間人攻擊漏洞和重放攻擊漏洞，會(huì)導(dǎo)致用戶端混幣地址的關(guān)聯(lián)性的泄露，即發(fā)送者匿名性不足的情況下用戶的輸入和輸出地址映射易被混幣中心發(fā)現(xiàn)。下一步研究將嘗試對(duì)MIXCOIN協(xié)議進(jìn)行改進(jìn)，并對(duì)其安全性進(jìn)行驗(yàn)證。