匿名協(xié)議WonGoo的概率模型驗(yàn)證分析

1、匿名協(xié)議wongoo的概率模型驗(yàn)證分析摘 要internet隱私的一個(gè)主要問(wèn)題是缺乏匿名保護(hù)。近年來(lái)，人們已經(jīng)針對(duì)這一問(wèn)題做了很多工作。然而，如何利用已有的形式化方法分析匿名技術(shù)卻是一個(gè)極具挑戰(zhàn)的問(wèn)題。對(duì)p2p匿名通信協(xié)議wongoo進(jìn)行了形式化分析。利用離散時(shí)間markov鏈模型化節(jié)點(diǎn)和攻擊者的行為。系統(tǒng)的匿名性質(zhì)采用時(shí)序邏輯pctl進(jìn)行描述。利用概率模型驗(yàn)證器prism對(duì)wongoo系統(tǒng)的匿名性進(jìn)行了自動(dòng)驗(yàn)證。結(jié)果表明wongoo的匿名性隨著系統(tǒng)規(guī)模的增加而增加；但卻隨著攻擊者觀(guān)察到的源自同一個(gè)發(fā)送者的路徑的增加而降低。另外，匿名路徑越長(zhǎng)，系統(tǒng)的匿名性越強(qiáng)。關(guān)鍵詞匿名；點(diǎn)對(duì)點(diǎn)；wongoo

2、；概率模型驗(yàn)證analysis of anonymity protocol wongoo with probabilistic model checkingabtract one of the main privacy problems in internet is lack of anonymity. much work has been done on this problem in recent years. however, it is a challenge to analyze anonymity protocol formally. this paper presents for

3、mal analysis of peer-to-peer anonymous communication protocol wongoo. the behavior of group members and the adversary is modeled as a discrete-time markov chain, and security properties are expressed as pctl formulas. using the probabilistic model checker prism, it analyzes the anonymity guarantees

4、the protocol is intended to provide. as a result, it not only finds that anonymity provided by wongoo increases with the increase in group size and degrades with the increase in the number of random routing paths, but it also shows the relationship between anonymity and path length.key words anonymi

5、ty, peer-to-peer, wongoo, probabilistic model checking 1引言internet的一個(gè)缺陷是不提供匿名保護(hù)，攻擊者可以根據(jù)通信流之間的關(guān)系對(duì)發(fā)送者和接收者進(jìn)行追蹤。隨著internet的快速發(fā)展并被人們廣為接受，以及搜索引擎和數(shù)據(jù)挖掘等技術(shù)的發(fā)展，人們已經(jīng)開(kāi)始關(guān)注internet上的隱私和匿名。隱私不僅意味著信息的機(jī)密性，而且意味著信息發(fā)布者身份的機(jī)密性。匿名技術(shù)是internet上保護(hù)用戶(hù)隱私的一種有效手段，它通過(guò)一定的方法將通信流中的通信關(guān)系加以隱藏，使攻擊者無(wú)法獲知雙方的通信關(guān)系或通信的一方。用戶(hù)在通信過(guò)程中，通過(guò)隱藏自己的ip地址來(lái)保

6、護(hù)自己的隱私。例如，用戶(hù)訪(fǎng)問(wèn)了某個(gè)網(wǎng)站，但是由于用戶(hù)使用了匿名技術(shù)，使得該訪(fǎng)問(wèn)活動(dòng)無(wú)法與用戶(hù)身份信息（指ip地址）關(guān)聯(lián)起來(lái)，這在一定程度上保護(hù)了用戶(hù)的隱私。加密技術(shù)可以保護(hù)通信的內(nèi)容，但是攻擊者可以通過(guò)通信流分析(traffic analysis)手段觀(guān)察出誰(shuí)和誰(shuí)在通信，通信的時(shí)間以及通信流的多少等。因此，加密技術(shù)并不能保證通信的安全，尤其是在一個(gè)大的開(kāi)放的環(huán)境中，保護(hù)通信者的身份就顯得更加困難。本文中通信者的身份是指其ip地址，因此發(fā)送者是指發(fā)送者的ip地址，同樣，接收者是指接收者的ip地址。我們所提出的wongoo協(xié)議1是一個(gè)綜合了mix2和crowds3的優(yōu)點(diǎn)的可擴(kuò)展點(diǎn)對(duì)點(diǎn)協(xié)議，提供三種

7、形式的匿名保護(hù)：發(fā)送方匿名（sender anonymity），即消息無(wú)法被關(guān)聯(lián)到其發(fā)送者；接收方匿名（receiver anonymity），即消息無(wú)法被關(guān)聯(lián)到其接收者；關(guān)系匿名（relationship anonymity），即消息的發(fā)送方和接收方是不可關(guān)聯(lián)的（unlinkability）4。wongoo克服了mix效率低和crowds抗攻擊性差的缺點(diǎn)，通過(guò)分層加密和隨機(jī)轉(zhuǎn)發(fā)取得了強(qiáng)匿名和高效率。我們?cè)谖墨I(xiàn)1中分析了wongoo的效率和匿名性介于crowds 和mix之間，是crowds和mix的折中。模型驗(yàn)證（model checking）技術(shù)是安全協(xié)議形式化分析的一項(xiàng)重要技術(shù)，它最早應(yīng)

8、用于硬件的性能驗(yàn)證中。隨著信息安全技術(shù)的不斷發(fā)展，被逐漸應(yīng)用于安全協(xié)議的形式化分析中。本文利用概率模型驗(yàn)證（probabilistic model checking）技術(shù)分析了wongoo系統(tǒng)的匿名性。我們把wongoo系統(tǒng)形式化為一個(gè)離散時(shí)間markov鏈（discrete-time markov chains，dtmcs）模型，利用時(shí)序邏輯pctl（probabilistic computational tree logic）5來(lái)描述wongoo系統(tǒng)的匿名性質(zhì)，并用概率模型驗(yàn)證器prism6進(jìn)行驗(yàn)證。我們所考慮的問(wèn)題是攻擊者是否能夠確定誰(shuí)是一條匿名路徑的發(fā)起者。我們假定攻擊者可以觀(guān)察部分網(wǎng)

9、絡(luò)通信流，可以運(yùn)行自己的wongoo節(jié)點(diǎn)，可以控制其他的部分wongoo節(jié)點(diǎn)。但是，攻擊者不能破壞系統(tǒng)所采用的加密技術(shù)。2概率模型驗(yàn)證技術(shù)模型驗(yàn)證是一種驗(yàn)證有限狀態(tài)系統(tǒng)的自動(dòng)化分析技術(shù)。系統(tǒng)被模型化為一個(gè)狀態(tài)轉(zhuǎn)化圖，系統(tǒng)的性質(zhì)用時(shí)序邏輯描述。它通過(guò)一個(gè)有效的搜索過(guò)程來(lái)驗(yàn)證狀態(tài)轉(zhuǎn)化圖是否滿(mǎn)足某種性質(zhì)。我們可以把模型驗(yàn)證抽象的描述為：給定一個(gè)模型m和邏輯描述的性質(zhì)p，檢查mp，即在模型m中性質(zhì)p是否成立。模型驗(yàn)證的最大優(yōu)點(diǎn)在于驗(yàn)證過(guò)程是全自動(dòng)化的，并且如果一個(gè)性質(zhì)不滿(mǎn)足，它能給出反例說(shuō)明這個(gè)性質(zhì)不滿(mǎn)足的理由。概率模型驗(yàn)證是模型驗(yàn)證技術(shù)的擴(kuò)充，主要用于自動(dòng)驗(yàn)證具有隨機(jī)行為的系統(tǒng)中某些事件發(fā)生的概率。

10、例如在系統(tǒng)運(yùn)行過(guò)程中驗(yàn)證事件“停機(jī)的概率不超過(guò)0.1”和“視頻幀在5毫秒內(nèi)到達(dá)的概率不低于0.9”等。概率模型驗(yàn)證中系統(tǒng)的形式化模型被賦予了概率信息，典型的情況是模型的每一個(gè)狀態(tài)轉(zhuǎn)化都標(biāo)記有一個(gè)概率，用于說(shuō)明狀態(tài)轉(zhuǎn)化的可能性。我們?cè)诒疚闹杏玫降哪Ｐ褪请x散時(shí)間markov鏈（dtmcs），其他兩個(gè)常用的模型是連續(xù)時(shí)間markov鏈（continuous-time markov chains，ctmcs）和markov決策過(guò)程（markov decision processes，mdps）。2.1離散時(shí)間markov鏈（dtmcs）一個(gè)帶標(biāo)記函數(shù)的離散時(shí)間markov鏈d是一個(gè)四元組 ，其中l(wèi) 是

11、一個(gè)有限狀態(tài)的集合；l 是初始狀態(tài)；l 是一個(gè)轉(zhuǎn)移概率矩陣，滿(mǎn)足 ，對(duì)任意的；l 是一個(gè)標(biāo)記函數(shù)，表示原子命題在狀態(tài)s成立，其中ap是一個(gè)原子命題集合。轉(zhuǎn)移概率矩陣的元素給出了從狀態(tài)到狀態(tài)的轉(zhuǎn)移概率。系統(tǒng)的一次執(zhí)行可用一條通過(guò)dtmcs的路徑表示。本文中wongoo系統(tǒng)的一次執(zhí)行是指一條wongoo路徑的建立過(guò)程。一條通過(guò)dtmcs的路徑是一個(gè)有窮（或者無(wú)窮）的狀態(tài)序列，其中對(duì)任意的，有。我們把始于狀態(tài)的路徑的集合記為。2.2 dtmcs上的pctl模型驗(yàn)證pctl是對(duì)時(shí)序邏輯ctl（computational tree logic）7的擴(kuò)充和發(fā)展。它在ctl基礎(chǔ)之上增加了概率算子，其中，。p

12、ctl的語(yǔ)法如下：其中是原子命題，是一個(gè)整數(shù)，是一個(gè)狀態(tài)公式，是一個(gè)路徑公式。概率算子的意思是，如果一條路徑源于狀態(tài)且滿(mǎn)足路徑公式的概率滿(mǎn)足條件，則認(rèn)為公式在狀態(tài)是滿(mǎn)足的?？梢员硎境上铝泄剑?其中。文獻(xiàn)8對(duì)這一概率的計(jì)算過(guò)程進(jìn)行了討論。prism支持三種類(lèi)型的路徑公式：，和。路徑滿(mǎn)足路徑公式，記為。下面給出pctl在dtmcs上的語(yǔ)義描述。對(duì)于一條路徑： （的第二個(gè)狀態(tài)滿(mǎn)足公式） （的前個(gè)狀態(tài)中的某個(gè)滿(mǎn)足，同時(shí)該狀態(tài)以前的所有狀態(tài)都滿(mǎn)足） 對(duì)于一個(gè)狀態(tài): for all 對(duì)于公式來(lái)說(shuō)，常用的形式是。如果一個(gè)狀態(tài)s滿(mǎn)足性質(zhì)，則從狀態(tài)到達(dá)滿(mǎn)足公式的狀態(tài)的概率滿(mǎn)足條件。2.3 prism模型驗(yàn)證器

13、prism6是由英國(guó)伯明翰大學(xué)開(kāi)發(fā)的一個(gè)概率模型驗(yàn)證器。它支持三種模型，dtmcs，ctmcs和mdps。在prism中，系統(tǒng)的行為用prism語(yǔ)言進(jìn)行描述。一個(gè)系統(tǒng)被構(gòu)建成幾個(gè)模塊，這些模塊之間利用標(biāo)準(zhǔn)的進(jìn)程代數(shù)運(yùn)算進(jìn)行交互。一個(gè)模塊包括一些變量，用于表示系統(tǒng)的狀態(tài)。系統(tǒng)的行為用一些監(jiān)視命令（guarded command）表示。監(jiān)視命令的格式如下： - ;其中，guard是系統(tǒng)變量上的斷言，command描述狀態(tài)轉(zhuǎn)移，其轉(zhuǎn)移的條件是guard為真。如果狀態(tài)轉(zhuǎn)移是不確定的，則command的形式為： : + + : prism根據(jù)對(duì)系統(tǒng)的描述進(jìn)行建模并確定可達(dá)狀態(tài)的集合。待驗(yàn)證的系統(tǒng)性質(zhì)用時(shí)

14、序邏輯pctl或ctl進(jìn)行描述。對(duì)于本文用到的dtmcs來(lái)說(shuō)，我們是用pctl進(jìn)行描述的。3 wongoo協(xié)議設(shè)alice與bob進(jìn)行通信，alice首先選擇一些wongoo節(jié)點(diǎn)，我們稱(chēng)之為固定接收點(diǎn)。固定接收點(diǎn)的功能與chaum描述的mix節(jié)點(diǎn)的功能相似。alice利用這些固定接收點(diǎn)的公鑰對(duì)要發(fā)送的消息進(jìn)行分層加密，構(gòu)造出wongoo數(shù)據(jù)包，然后以概率轉(zhuǎn)發(fā)給一個(gè)隨機(jī)選定的節(jié)點(diǎn)，稱(chēng)為概率接收點(diǎn)，以概率轉(zhuǎn)發(fā)給下一個(gè)固定接收點(diǎn)。隨后的每個(gè)節(jié)點(diǎn)（包括固定接收點(diǎn)和概率接收點(diǎn)）都進(jìn)行類(lèi)似的操作。當(dāng)wongoo數(shù)據(jù)包到達(dá)接收者bob以后，就形成了一條wongoo路徑。隨后的所有消息以及從bob返回到ali

15、ce的消息都沿著這條路徑進(jìn)行傳遞。我們?cè)谖墨I(xiàn)1中分析了攻擊者不能分辨出一條路徑上的固定接收點(diǎn)和概率接收點(diǎn)。在一個(gè)大的點(diǎn)對(duì)點(diǎn)匿名通信系統(tǒng)中，由于節(jié)點(diǎn)只擁有局部的拓?fù)湫畔?，因此，在進(jìn)行下一跳選擇時(shí)，可能會(huì)選擇到已經(jīng)在路徑上出現(xiàn)過(guò)的節(jié)點(diǎn)，即節(jié)點(diǎn)可能會(huì)在路徑上重復(fù)出現(xiàn)。為了提高系統(tǒng)的匿名性，必須盡量減少重復(fù)節(jié)點(diǎn)出現(xiàn)的概率。wongoo在路徑構(gòu)造過(guò)程中，由發(fā)送者alice確定的固定節(jié)點(diǎn)不允許重復(fù)。而且，每一個(gè)節(jié)點(diǎn)在進(jìn)行概率轉(zhuǎn)發(fā)時(shí)，所選擇的下一跳節(jié)點(diǎn)不能與該節(jié)點(diǎn)本身以及上一跳節(jié)點(diǎn)相同。為了使分析變得簡(jiǎn)單，本文假定節(jié)點(diǎn)可在wongoo路徑上的任何位置重復(fù)出現(xiàn)。因此，wongoo系統(tǒng)的匿名性實(shí)際上比本文分析的

16、要高。為了后面敘述方便，我們定義固定路徑和變化路徑兩個(gè)概念。由一個(gè)固定接收點(diǎn)直接到達(dá)另一個(gè)固定接收點(diǎn)的一條路稱(chēng)為固定路徑（發(fā)送者和接收者也被看成是固定接收點(diǎn)）。兩個(gè)固定接收點(diǎn)之間依據(jù)概率轉(zhuǎn)發(fā)所形成的路徑稱(chēng)為變化路徑。顯然，當(dāng)變化路徑長(zhǎng)度為1時(shí)，則成為固定路徑。4 wongoo的模型構(gòu)造我們僅僅對(duì)wongoo的路徑建立過(guò)程進(jìn)行模型驗(yàn)證，而對(duì)路徑建立完成以后的通信沒(méi)有進(jìn)行模型驗(yàn)證，原因是路徑一旦建立，那么路徑上的每一個(gè)轉(zhuǎn)發(fā)節(jié)點(diǎn)都是從固定的上一個(gè)節(jié)點(diǎn)接收消息，而且通信的內(nèi)容是不會(huì)泄漏發(fā)送者的身份信息的。因此攻擊者不會(huì)從隨后的通信中獲得更多的關(guān)于發(fā)送者的信息。我們的markov鏈模型中的狀態(tài)代表匿名路

17、徑建立過(guò)程中系統(tǒng)所處的狀態(tài)。一個(gè)狀態(tài)完全由模型中的狀態(tài)變量所確定，見(jiàn)表1。表1 狀態(tài)變量table 1 state variablesruncountnumber of paths constructed so far ( 0) - (runcount = runcount-1) & new = false & start = true & fixednodenum = maxfixednodenum & fwlength = maxfwlength;/ start the protocol start - lastseen=0 & run=true & deliver=false & sta

18、rt=false;4.2 轉(zhuǎn)發(fā)節(jié)點(diǎn)的選擇發(fā)送者隨機(jī)的從個(gè)節(jié)點(diǎn)中選擇第一個(gè)概率接收點(diǎn)。假定個(gè)節(jié)點(diǎn)被選中的概率是相等的。我們把轉(zhuǎn)發(fā)節(jié)點(diǎn)的選擇模型化為兩次狀態(tài)轉(zhuǎn)移，一次確定所選擇的轉(zhuǎn)發(fā)節(jié)點(diǎn)是否是誠(chéng)實(shí)的，另外一次確定轉(zhuǎn)發(fā)節(jié)點(diǎn)的身份。隨機(jī)選擇的轉(zhuǎn)發(fā)節(jié)點(diǎn)是惡意節(jié)點(diǎn)的概率為badc=c/n，是誠(chéng)實(shí)節(jié)點(diǎn)的概率為goodc=1-badc。/ good or bad wongoo member (!good & !bad & !deliver & run) - goodc: (good=true) & (recordlast=true) & (run=false) +badc: bad=true & badobs

19、erve=true & run=false;如果轉(zhuǎn)發(fā)節(jié)點(diǎn)是誠(chéng)實(shí)的，則它可能為n-c個(gè)誠(chéng)實(shí)節(jié)點(diǎn)中的任意一個(gè)。轉(zhuǎn)發(fā)者的身份記錄在lastseen變量中。記錄轉(zhuǎn)發(fā)者的身份是為了模擬以下行為：如果該轉(zhuǎn)發(fā)節(jié)點(diǎn)的下一個(gè)節(jié)點(diǎn)是惡意節(jié)點(diǎn)，則該惡意節(jié)點(diǎn)可以記錄下該轉(zhuǎn)發(fā)節(jié)點(diǎn)的ip地址。/ record the last wongoo member who touched the message, all good members may appear with equal / probability recordlast & wongoosize=10 -0.1: (lastseen=0) & (recordla

20、st=false) & (run=true) + 0.1: (lastseen=9) & (recordlast=false) & (run=true);wongoo協(xié)議中，每一個(gè)節(jié)點(diǎn)（包括惡意節(jié)點(diǎn)）都必須確定下一跳。轉(zhuǎn)發(fā)者以概率將數(shù)據(jù)轉(zhuǎn)發(fā)給隨機(jī)選定的概率接收點(diǎn)，以概率轉(zhuǎn)發(fā)給已經(jīng)選好的下一個(gè)固定接收點(diǎn)。/ good members, forward to a random selected node with probability pf, else deliver to the next fixed node. (good & !deliver & run & fwlength 0) - p

21、f: (good=false) & (fwlength=fwlength-1) + notpf: (good=false) & (fixednodenum=fixednodenum-1) & (fwlength=maxfwlength); 4.3 惡意節(jié)點(diǎn)的模型化顯然，匿名路徑上的節(jié)點(diǎn)是知道它前一跳的地址的。如果是惡意節(jié)點(diǎn)，則它將記錄下其上一跳的ip地址。這是通過(guò)讀取lastseen變量的值并紀(jì)錄在observei中而實(shí)現(xiàn)的。/ bad members, remember from whom the message was received and terminate the protocol

22、 lastseen=0 & badobserve - (observe0 = observe0 + 1) & deliver=true & run=true & badobserve=false; lastseen=9 & badobserve - (observe9 = observe9 + 1) & deliver=true & run=true & badobserve=false;對(duì)每一次路徑建立過(guò)程來(lái)說(shuō)，計(jì)數(shù)器observei并不清零，而是進(jìn)行累加。這使得攻擊者可以將對(duì)源自同一個(gè)發(fā)起者的多條路徑的觀(guān)察信息進(jìn)行累加。我們假定攻擊者可以驗(yàn)證出兩條路經(jīng)是否源自同一個(gè)發(fā)送者。4.4 協(xié)議的結(jié)

23、束當(dāng)遇到攻擊者時(shí)我們就結(jié)束路徑建立過(guò)程，這是因?yàn)橐坏┡龅搅藧阂夤?jié)點(diǎn)，則隨后的建立過(guò)程不會(huì)提供更多的關(guān)于發(fā)送者的信息給攻擊者，攻擊者所能獲知的就是上一跳的地址。這一點(diǎn)與shmatikov9用prism分析crowds協(xié)議時(shí)所采用的方法相同。但是如果在路徑建立過(guò)程沒(méi)有碰到惡意節(jié)點(diǎn)，shmatikov的方法在理論上會(huì)產(chǎn)生死鎖狀態(tài)，原因是shmatikov沒(méi)有對(duì)匿名路徑的長(zhǎng)度進(jìn)行限制。我們用fixednodenum表示固定接收點(diǎn)數(shù)，fwlength表示變化路徑長(zhǎng)度，而且我們認(rèn)為接收者也是一個(gè)固定接收點(diǎn)。這樣，如果在路徑建立過(guò)程中沒(méi)有碰到惡意節(jié)點(diǎn)，則當(dāng)fixednodenum的值為零時(shí)，路徑建立結(jié)束，避

24、免了死鎖。/ if all members in a path are honest, terminate the path set up when its length increases to the max length. (!good & !deliver & run & fwlength = 0) - (fixednodenum = fixednodenum-1) & (fwlength = maxfwlength); fixednodenum=0 - deliver=true;/ terminate the protocol deliver & run - done=true &

25、deliver=false & run=false & good=false & bad=false; / start a new instance done - new=true & done=false & run=false;5 匿名性質(zhì)的形式化與對(duì)crowds的分析39類(lèi)似，我們假定攻擊者能夠把源自同一個(gè)發(fā)送者的幾條路經(jīng)關(guān)聯(lián)起來(lái)。在攻擊者看來(lái)，如果某一個(gè)節(jié)點(diǎn)比其他節(jié)點(diǎn)更像是發(fā)送者，則他有理由認(rèn)為該節(jié)點(diǎn)就是真正的發(fā)送者。我們要回答的問(wèn)題就是攻擊者猜測(cè)出發(fā)送者的概率有多大。我們將在表示wongoo系統(tǒng)的markov鏈上構(gòu)造pctl公式對(duì)這個(gè)問(wèn)題進(jìn)行討論。我們用表示攻擊者觀(guān)察到wongoo成

26、員的次數(shù)。其意思是在由同一發(fā)送者發(fā)起的多條路徑中，經(jīng)過(guò)節(jié)點(diǎn)并且的下一跳是惡意節(jié)點(diǎn)的路徑有條。用表示發(fā)送者被觀(guān)察到的次數(shù)。這包括兩種情況，一是惡意節(jié)點(diǎn)被選為第一個(gè)轉(zhuǎn)發(fā)者；二是發(fā)送者本身被選為一個(gè)中轉(zhuǎn)節(jié)點(diǎn)，其下一跳是一個(gè)惡意節(jié)點(diǎn)。我們采用shmatikov在文獻(xiàn)9中提出的方法來(lái)驗(yàn)證wongoo成員。如果一個(gè)成員被觀(guān)察到的次數(shù)比其他成員的都多，即，則我們認(rèn)為該成員是發(fā)送者。為此，定義以下事件：，（發(fā)起者被觀(guān)察到次數(shù)大于其他任何成員的）。于是我們要驗(yàn)證的概率為： （猜測(cè)到真正的發(fā)起者）。上述匿名性質(zhì)用pctl描述如下：/detection p = ? true u (new & runcount =

27、0 & observe0 observe1 & & observe0 observe9)6 驗(yàn)證結(jié)果我們利用prism模型驗(yàn)證器對(duì)wongoo系統(tǒng)的不同配置進(jìn)行概率模型驗(yàn)證。表2描述了不同規(guī)模下的狀態(tài)空間，其中，固定節(jié)點(diǎn)數(shù)fixednodenum=3，變化路徑長(zhǎng)度f(wàn)wlength=3。從表中可知，與其他的模型驗(yàn)證一樣，隨著系統(tǒng)規(guī)模的增大，狀態(tài)空間增長(zhǎng)很快，這使得分析大規(guī)模wongoo系統(tǒng)變得困難。如何解決模型驗(yàn)證中狀態(tài)空間爆炸問(wèn)題是該領(lǐng)域的一個(gè)難題。表2 狀態(tài)空間table 2 size of state spacewongoo源自同一發(fā)送者的路徑數(shù)（totalruns）345610 hone

28、st membersstates112,890524,0261,955,8526,232,410transitions308,7701,439,3065,391,23217,232,49015 honest membersstates332,9002,099,87610,460,61243,785,236transitions1,126,5957,130,77135,631,407149,556,43120 honest membersstates734,9605,860,62636,518,022189,355,322transitions2,964,72023,708,786148,121

29、,382769,919,48225 honest membersstates1,373,82013,244,27699,077,582612,790,418transitions6,434,77062,186,726466,274,6572,890,100,243表3計(jì)算了不同路徑數(shù)下的驗(yàn)證概率，從中可以看出以下兩點(diǎn)：l 隨著攻擊者所觀(guān)察到的源自同一發(fā)送者的路徑的增多，系統(tǒng)的匿名性降低。因此，在wongoo中，一次會(huì)話(huà)（發(fā)送者和接收者之間的一次通信）只通過(guò)一條路徑完成，而不像peekabooty所建議的那樣，一次會(huì)話(huà)通過(guò)多條路徑完成，既所謂的多路徑路由。l 在惡意節(jié)點(diǎn)比例（badc=0.167

30、）不變時(shí)，驗(yàn)證概率隨著系統(tǒng)規(guī)模的增大而減小。這說(shuō)明系統(tǒng)的匿名性隨著規(guī)模的增加而增加。 表3 不同路徑數(shù)下的驗(yàn)證概率（pf=0.3, fixednodenum=3, fwlength=3）。 table 3 probabilities of detecting the initiator increase with increasing totalruns wongoo源自同一發(fā)送者的路徑數(shù)（totalruns）345610 honest, 1 corruptpr(%)17.2917.8618.5119.1215 honest, 2 corruptpr(%)17.4718.0019.3219.8

31、910 honest, 2 corruptpr(%)21.8524.2528.0932.2115 honest, 3 corruptpr(%)19.9322.0725.8728.4320 honest, 4 corruptpr(%)18.9620.9723.5125.3725 honest, 5 corruptpr(%)18.3919.9822.8324.78yong guan等人10研究指出，通常情況下，匿名性隨著匿名路徑長(zhǎng)度的增加而增加。wongoo正是在保證足夠匿名的前提下，通過(guò)延長(zhǎng)匿名路徑，從而進(jìn)一步提高了系統(tǒng)的匿名性。表4和表5分別描述了wongoo的匿名性隨路徑長(zhǎng)度的變化關(guān)系。表4

32、通過(guò)調(diào)整轉(zhuǎn)發(fā)概率pf的大小來(lái)調(diào)整路徑長(zhǎng)度。表5通過(guò)調(diào)整固定節(jié)點(diǎn)數(shù)fixednodenum來(lái)調(diào)整路徑長(zhǎng)度。可以看出，隨著匿名路徑的增長(zhǎng)，驗(yàn)證概率降低，從而系統(tǒng)的匿名性得到了提高。表4 不同轉(zhuǎn)發(fā)概率下的驗(yàn)證概率（fixednodenum=4, fwlength=5, totalrun=3）table 4 probabilities of detecting the initiator decrease with increasing forward probabilitieswongoopf 0.10.20.30.40.50.60.70.80.910 honest, 1 corruptpr(%)1

33、7.9417.1016.0614.6712.7910.397.735.403.8715 honest, 2 corruptpr(%)17.7216.5415.2013.6311.799.747.736.094.9710 honest, 2 corruptpr(%)21.8420.5819.2617.8816.4415.0113.6612.4411.2815 honest, 3 corruptpr(%)19.7818.4617.0815.6614.2012.7711.4910.419.4620 honest, 4 corruptpr(%)18.7517.4016.0014.5513.0911.6

34、810.439.428.5725 honest, 5 corruptpr(%)18.1516.7915.3813.9212.4511.059.838.858.07表5 不同固定節(jié)點(diǎn)數(shù)下的驗(yàn)證概率（pf=0.3, fwlength=5, totalrun=3）table 5 probabilities of detecting the initiator decrease with increasing fixed node numberswongoofixednodenum2468101210 honest, 1 corruptpr(%)20.6216.0612.8010.709.468.78

35、15 honest, 2 corruptpr(%)22.1815.2011.439.538.648.2610 honest, 2 corruptpr(%)27.7019.2616.2115.3215.1815.1615 honest, 3 corruptpr(%)26.0017.0813.8212.7612.4912.4720 honest, 4 corruptpr(%)25.1316.0012.6511.5211.1811.1225 honest, 5 corruptpr(%)24.6215.3811.9810.8110.4410.357 結(jié)論形式化方法是對(duì)安全協(xié)議進(jìn)行驗(yàn)證的一種有力工具。如

36、何利用已有的形式化方法對(duì)匿名協(xié)議進(jìn)行分析是一個(gè)極具挑戰(zhàn)的問(wèn)題。概率模型驗(yàn)證是一種十分有效的協(xié)議形式化分析工具。本文利用prism模型驗(yàn)證器對(duì)匿名通信協(xié)議wongoo進(jìn)行了分析。wongoo通過(guò)隨機(jī)轉(zhuǎn)發(fā)和分層加密建立匿名通信路徑。因此，我們把wongoo的路徑建立過(guò)程模型化為一個(gè)離散時(shí)間markov鏈，并在攻擊者可以識(shí)別出兩條鏈路是否源自同一發(fā)送者的假設(shè)下，分析了攻擊者識(shí)別出一條匿名路徑的發(fā)起者的概率。wongoo協(xié)議的分析表明了利用概率模型驗(yàn)證技術(shù)分析安全協(xié)議的可行性。references:1 t. lu, b. fang, y. sun, x. cheng. wongoo: a peer-to-peer protocol for anonymous communication, in proceedings of the 2004 international conference on parallel and distributed processing techniques and applications (pdpta04), june 2004: 1102-1106.2 d. chaum. untraceable electronic mail, return addresses and digital pseudonyms. com