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

AnalysisofAnonymityProtocolWonGoowithProbabilisticModelCheckingAbtractOneofthemainprivacyproblemsinInternetislackofanonymity.Muchworkhasbeendoneonthisprobleminrecentyears.However,itisachallengetoanalyzeanonymityprotocolformally.Thispaperpresentsformalanalysisofpeer-to-peeranonymouscommunicationprotocolWonGoo.Thebehaviorofgroupmembersandtheadversaryismodeledasadiscrete-timeMarkovchain,andsecuritypropertiesareexpressedasPCTLformulas.UsingtheprobabilisticmodelcheckerPRISM,itanalyzestheanonymityguaranteestheprotocolisintendedtoprovide.Asaresult,itnotonlyfindsthatanonymityprovidedbyWonGooincreaseswiththeincreaseingroupsizeanddegradeswiththeincreaseinthenumberofrandomroutingpaths,butitalsoshowstherelationshipbetweenanonymityandpathlength.Keywords anonymity,Peer-to-Peer,WonGoo,ProbabilisticModelChecking

1 引言Internet的一個缺陷是不提供匿名保護(hù)，攻擊者可以根據(jù)通信流之間的關(guān)系對發(fā)送者和接收者進(jìn)行追蹤。隨著Internet的快速發(fā)展并被人們廣為接受，以及搜索引擎和數(shù)據(jù)挖掘等技術(shù)的發(fā)展，人們已經(jīng)開始關(guān)注Internet上的隱私和匿名。隱私不僅意味著信息的機(jī)密性，而且意味著信息發(fā)布者身份的機(jī)密性。匿名技術(shù)是Internet上保護(hù)用戶隱私的一種有效手段，它通過一定的方法將通信流中的通信關(guān)系加以隱藏，使攻擊者無法獲知雙方的通信關(guān)系或通信的一方。用戶在通信過程中，通過隱藏自己的IP地址來保護(hù)自己的隱私。例如，用戶訪問了某個網(wǎng)站，但是由于用戶使用了匿名技術(shù)，使得該訪問活動無法與用戶身份信息（指IP地址）關(guān)聯(lián)起來，這在一定程度上保護(hù)了用戶的隱私。加密技術(shù)可以保護(hù)通信的內(nèi)容，但是攻擊者可以通過通信流分析(Trafficanalysis)手段觀察出誰和誰在通信，通信的時間以及通信流的多少等。因此，加密技術(shù)并不能保證通信的安全，尤其是在一個大的開放的環(huán)境中，保護(hù)通信者的身份就顯得更加困難。本文中通信者的身份是指其IP地址，因此發(fā)送者是指發(fā)送者的IP地址，同樣，接收者是指接收者的IP地址。我們所提出的WonGoo協(xié)議[1]是一個綜合了Mix[2]和Crowds[3]的優(yōu)點的可擴(kuò)展點對點協(xié)議，提供三種形式的匿名保護(hù)：發(fā)送方匿名（senderanonymity），即消息無法被關(guān)聯(lián)到其發(fā)送者；接收方匿名（receiveranonymity），即消息無法被關(guān)聯(lián)到其接收者；關(guān)系匿名（relationshipanonymity），即消息的發(fā)送方和接收方是不可關(guān)聯(lián)的（unlinkability）[4]。WonGoo克服了Mix效率低和Crowds抗攻擊性差的缺點，通過分層加密和隨機(jī)轉(zhuǎn)發(fā)取得了強(qiáng)匿名和高效率。我們在文獻(xiàn)[1]中分析了WonGoo的效率和匿名性介于Crowds和Mix之間，是Crowds和Mix的折中。模型驗證（ModelChecking）技術(shù)是安全協(xié)議形式化分析的一項重要技術(shù)，它最早應(yīng)用于硬件的性能驗證中。隨著信息安全技術(shù)的不斷發(fā)展，被逐漸應(yīng)用于安全協(xié)議的形式化分析中。本文利用概率模型驗證（ProbabilisticModelChecking）技術(shù)分析了WonGoo系統(tǒng)的匿名性。我們把WonGoo系統(tǒng)形式化為一個離散時間Markov鏈（discrete-timeMarkovchains，DTMCs）模型，利用時序邏輯PCTL（ProbabilisticComputationalTreeLogic）[5]來描述WonGoo系統(tǒng)的匿名性質(zhì)，并用概率模型驗證器PRISM[6]進(jìn)行驗證。我們所考慮的問題是攻擊者是否能夠確定誰是一條匿名路徑的發(fā)起者。我們假定攻擊者可以觀察部分網(wǎng)絡(luò)通信流，可以運(yùn)行自己的WonGoo節(jié)點，可以控制其他的部分WonGoo節(jié)點。但是，攻擊者不能破壞系統(tǒng)所采用的加密技術(shù)。2概率模型驗證技術(shù)模型驗證是一種驗證有限狀態(tài)系統(tǒng)的自動化分析技術(shù)。系統(tǒng)被模型化為一個狀態(tài)轉(zhuǎn)化圖，系統(tǒng)的性質(zhì)用時序邏輯描述。它通過一個有效的搜索過程來驗證狀態(tài)轉(zhuǎn)化圖是否滿足某種性質(zhì)。我們可以把模型驗證抽象的描述為：給定一個模型M和邏輯描述的性質(zhì)P，檢查M╞P，即在模型M中性質(zhì)P是否成立。模型驗證的最大優(yōu)點在于驗證過程是全自動化的，并且如果一個性質(zhì)不滿足，它能給出反例說明這個性質(zhì)不滿足的理由。概率模型驗證是模型驗證技術(shù)的擴(kuò)充，主要用于自動驗證具有隨機(jī)行為的系統(tǒng)中某些事件發(fā)生的概率。例如在系統(tǒng)運(yùn)行過程中驗證事件“停機(jī)的概率不超過0.1”和“視頻幀在5毫秒內(nèi)到達(dá)的概率不低于0.9概率模型驗證中系統(tǒng)的形式化模型被賦予了概率信息，典型的情況是模型的每一個狀態(tài)轉(zhuǎn)化都標(biāo)記有一個概率，用于說明狀態(tài)轉(zhuǎn)化的可能性。我們在本文中用到的模型是離散時間Markov鏈（DTMCs），其他兩個常用的模型是連續(xù)時間Markov鏈（continuous-timeMarkovchains，CTMCs）和Markov決策過程（Markovdecisionprocesses，MDPs）。2.1離散時間Markov鏈（DTMCs）一個帶標(biāo)記函數(shù)的離散時間Markov鏈D是一個四元組，其中是一個有限狀態(tài)的集合；是初始狀態(tài)；是一個轉(zhuǎn)移概率矩陣，滿足，對任意的；是一個標(biāo)記函數(shù)，表示原子命題在狀態(tài)s成立，其中AP是一個原子命題集合。轉(zhuǎn)移概率矩陣的元素給出了從狀態(tài)到狀態(tài)的轉(zhuǎn)移概率。系統(tǒng)的一次執(zhí)行可用一條通過DTMCs的路徑表示。本文中WonGoo系統(tǒng)的一次執(zhí)行是指一條WonGoo路徑的建立過程。一條通過DTMCs的路徑是一個有窮（或者無窮）的狀態(tài)序列，其中對任意的，有。我們把始于狀態(tài)的路徑的集合記為。2.2DTMCs上的PCTL模型驗證PCTL是對時序邏輯CTL（ComputationalTreeLogic）[7]的擴(kuò)充和發(fā)展。它在CTL基礎(chǔ)之上增加了概率算子，其中，。PCTL的語法如下： 其中是原子命題，是一個整數(shù)，是一個狀態(tài)公式，是一個路徑公式。概率算子的意思是，如果一條路徑源于狀態(tài)且滿足路徑公式的概率滿足條件，則認(rèn)為公式在狀態(tài)是滿足的?？梢员硎境上铝泄剑? ╞其中。文獻(xiàn)[8]對這一概率的計算過程進(jìn)行了討論。PRISM支持三種類型的路徑公式：，和。路徑滿足路徑公式，記為╞。下面給出PCTL在DTMCs上的語義描述。對于一條路徑： （的第二個狀態(tài)滿足公式） （的前個狀態(tài)中的某個滿足，同時該狀態(tài)以前的所有狀態(tài)都滿足） 對于一個狀態(tài): forall 對于公式來說，常用的形式是。如果一個狀態(tài)s滿足性質(zhì)，則從狀態(tài)到達(dá)滿足公式的狀態(tài)的概率滿足條件。2.3PRISM模型驗證器PRISM[6]是由英國伯明翰大學(xué)開發(fā)的一個概率模型驗證器。它支持三種模型，DTMCs，CTMCs和MDPs。在PRISM中，系統(tǒng)的行為用PRISM語言進(jìn)行描述。一個系統(tǒng)被構(gòu)建成幾個模塊，這些模塊之間利用標(biāo)準(zhǔn)的進(jìn)程代數(shù)運(yùn)算進(jìn)行交互。一個模塊包括一些變量，用于表示系統(tǒng)的狀態(tài)。系統(tǒng)的行為用一些監(jiān)視命令（guardedcommand）表示。監(jiān)視命令的格式如下： []<guard>-><command>;其中，guard是系統(tǒng)變量上的斷言，command描述狀態(tài)轉(zhuǎn)移，其轉(zhuǎn)移的條件是guard為真。如果狀態(tài)轉(zhuǎn)移是不確定的，則command的形式為： <prob>:<command>+···+<prob>:<command>PRISM根據(jù)對系統(tǒng)的描述進(jìn)行建模并確定可達(dá)狀態(tài)的集合。待驗證的系統(tǒng)性質(zhì)用時序邏輯PCTL或CTL進(jìn)行描述。對于本文用到的DTMCs來說，我們是用PCTL進(jìn)行描述的。3WonGoo協(xié)議設(shè)Alice與Bob進(jìn)行通信，Alice首先選擇一些WonGoo節(jié)點，我們稱之為固定接收點。固定接收點的功能與Chaum描述的Mix節(jié)點的功能相似。Alice利用這些固定接收點的公鑰對要發(fā)送的消息進(jìn)行分層加密，構(gòu)造出WonGoo數(shù)據(jù)包，然后以概率轉(zhuǎn)發(fā)給一個隨機(jī)選定的節(jié)點，稱為概率接收點，以概率轉(zhuǎn)發(fā)給下一個固定接收點。隨后的每個節(jié)點（包括固定接收點和概率接收點）都進(jìn)行類似的操作。當(dāng)WonGoo數(shù)據(jù)包到達(dá)接收者Bob以后，就形成了一條WonGoo路徑。隨后的所有消息以及從Bob返回到Alice的消息都沿著這條路徑進(jìn)行傳遞。我們在文獻(xiàn)[1]中分析了攻擊者不能分辨出一條路徑上的固定接收點和概率接收點。在一個大的點對點匿名通信系統(tǒng)中，由于節(jié)點只擁有局部的拓?fù)湫畔?，因此，在進(jìn)行下一跳選擇時，可能會選擇到已經(jīng)在路徑上出現(xiàn)過的節(jié)點，即節(jié)點可能會在路徑上重復(fù)出現(xiàn)。為了提高系統(tǒng)的匿名性，必須盡量減少重復(fù)節(jié)點出現(xiàn)的概率。WonGoo在路徑構(gòu)造過程中，由發(fā)送者Alice確定的固定節(jié)點不允許重復(fù)。而且，每一個節(jié)點在進(jìn)行概率轉(zhuǎn)發(fā)時，所選擇的下一跳節(jié)點不能與該節(jié)點本身以及上一跳節(jié)點相同。為了使分析變得簡單，本文假定節(jié)點可在WonGoo路徑上的任何位置重復(fù)出現(xiàn)。因此，WonGoo系統(tǒng)的匿名性實際上比本文分析的要高。為了后面敘述方便，我們定義固定路徑和變化路徑兩個概念。由一個固定接收點直接到達(dá)另一個固定接收點的一條路稱為固定路徑（發(fā)送者和接收者也被看成是固定接收點）。兩個固定接收點之間依據(jù)概率轉(zhuǎn)發(fā)所形成的路徑稱為變化路徑。顯然，當(dāng)變化路徑長度為1時，則成為固定路徑。4WonGoo的模型構(gòu)造我們僅僅對WonGoo的路徑建立過程進(jìn)行模型驗證，而對路徑建立完成以后的通信沒有進(jìn)行模型驗證，原因是路徑一旦建立，那么路徑上的每一個轉(zhuǎn)發(fā)節(jié)點都是從固定的上一個節(jié)點接收消息，而且通信的內(nèi)容是不會泄漏發(fā)送者的身份信息的。因此攻擊者不會從隨后的通信中獲得更多的關(guān)于發(fā)送者的信息。我們的Markov鏈模型中的狀態(tài)代表匿名路徑建立過程中系統(tǒng)所處的狀態(tài)。一個狀態(tài)完全由模型中的狀態(tài)變量所確定，見表1。表1表1狀態(tài)變量Table1StatevariablesrunCountNumberofpathsconstructedsofar(<=TotalRuns).goodTheselectedforwarderishonest.badTheselectedforwarderisbad.lastSeenIdentityoftheprecedingforwarderonthepath.observeiNumberoftimescorruptmembersobservedmemberi.newReadytoconstructanotherpath.startBeginningofnewpathconstruction.runContinuepathconstruction.deliverTerminatethepath.recordLastRecordtheidentityoftheprecedingforwarder.badObserveHaveacorruptmemberrecorditsobservations.fixedNodeNumNumberoffixedWonGoonodesinapath.FwLengthForwardpathlengthbetweentwofixedWonGoonodes.我們假定攻擊者除了有能力運(yùn)行自己的WonGoo節(jié)點之外，還能控制部分其他的節(jié)點。我們把攻擊者自己的節(jié)點及被其控制的其他節(jié)點統(tǒng)稱為泄密節(jié)點，也叫泄密者；把沒有被攻擊者控制的節(jié)點，即非泄密者，稱為誠實的節(jié)點。誠實的節(jié)點不會為攻擊者提供任何信息。假設(shè)個成員的WonGoo網(wǎng)絡(luò)中有個泄密者，發(fā)送者Alice已經(jīng)利用節(jié)點選擇算法[1]選定了個固定接收點。我們所考慮的問題是攻擊者是否能夠確定一條路徑的發(fā)送者是誰。對接收者的分析與對發(fā)送者的類似。如果發(fā)送者本身是一個泄密者，則對攻擊者來說，系統(tǒng)已經(jīng)被攻破。我們考慮由非泄密節(jié)點發(fā)起的一條路徑。在這條路徑上，泄密節(jié)點占據(jù)了一個位置。泄密者的目的是確定誰是該路徑的發(fā)起者。由于我們采用了加密技術(shù)，因此通信的內(nèi)容是不會暴露發(fā)起者的身份的。所以，攻擊者有理由相信第一個泄密者的前驅(qū)節(jié)點比其他節(jié)點更像是發(fā)起者。這種假設(shè)是合理的，因為從攻擊者來看第一個泄密者的前者最有可能是發(fā)起者。后面的敘述中假設(shè)WonGoo網(wǎng)絡(luò)中誠實節(jié)點數(shù)為10。4.1協(xié)議的開始我們要求每一次會話都是由同一個發(fā)送者(observe0)發(fā)起的。這是通過在協(xié)議開始時設(shè)置變量lastSeen的值為零來實現(xiàn)的。同時，我們還要設(shè)置分別用于表示固定節(jié)點數(shù)和變化路徑長度的變量fixedNodeNum和FwLength的值。//Setupanewprotocolinstance[]new&(runCount>0)->(runCount'=runCount-1)&new'=false&start'=true&fixedNodeNum'=MaxfixedNodeNum&FwLength'=MaxFwLength;//Starttheprotocol[]start->lastSeen'=0&run'=true&deliver'=false&start'=false;4.2轉(zhuǎn)發(fā)節(jié)點的選擇發(fā)送者隨機(jī)的從個節(jié)點中選擇第一個概率接收點。假定個節(jié)點被選中的概率是相等的。我們把轉(zhuǎn)發(fā)節(jié)點的選擇模型化為兩次狀態(tài)轉(zhuǎn)移，一次確定所選擇的轉(zhuǎn)發(fā)節(jié)點是否是誠實的，另外一次確定轉(zhuǎn)發(fā)節(jié)點的身份。隨機(jī)選擇的轉(zhuǎn)發(fā)節(jié)點是惡意節(jié)點的概率為badC=C/N，是誠實節(jié)點的概率為goodC=1-badC。//GoodorbadWonGoomember[](!good&!bad&!deliver&run)->goodC:(good'=true)&(recordLast'=true)&(run'=false)+ badC:bad'=true&badObserve'=true&run'=false;如果轉(zhuǎn)發(fā)節(jié)點是誠實的，則它可能為N-C個誠實節(jié)點中的任意一個。轉(zhuǎn)發(fā)者的身份記錄在lastSeen變量中。記錄轉(zhuǎn)發(fā)者的身份是為了模擬以下行為：如果該轉(zhuǎn)發(fā)節(jié)點的下一個節(jié)點是惡意節(jié)點，則該惡意節(jié)點可以記錄下該轉(zhuǎn)發(fā)節(jié)點的IP地址。//RecordthelastWonGoomemberwhotouchedthemessage,allgoodmembersmayappearwithequal//probability[]recordLast&WonGooSize=10-> 0.1:(lastSeen'=0)&(recordLast'=false)&(run'=true)+ … 0.1:(lastSeen'=9)&(recordLast'=false)&(run'=true);WonGoo協(xié)議中，每一個節(jié)點（包括惡意節(jié)點）都必須確定下一跳。轉(zhuǎn)發(fā)者以概率將數(shù)據(jù)轉(zhuǎn)發(fā)給隨機(jī)選定的概率接收點，以概率轉(zhuǎn)發(fā)給已經(jīng)選好的下一個固定接收點。//Goodmembers,forwardtoarandomselectednodewithprobabilityPF,elsedelivertothenextfixednode.[](good&!deliver&run&FwLength>0)->PF:(good'=false)&(FwLength'=FwLength-1)+notPF:(good'=false)&(fixedNodeNum'=fixedNodeNum-1)&(FwLength'=MaxFwLength); 4.3惡意節(jié)點的模型化顯然，匿名路徑上的節(jié)點是知道它前一跳的地址的。如果是惡意節(jié)點，則它將記錄下其上一跳的IP地址。這是通過讀取lastSeen變量的值并紀(jì)錄在observei中而實現(xiàn)的。//Badmembers,rememberfromwhomthemessagewasreceivedandterminatetheprotocol[]lastSeen=0&badObserve->(observe0'=observe0+1)&deliver'=true&run'=true&badObserve'=false; …[]lastSeen=9&badObserve->(observe9'=observe9+1)&deliver'=true&run'=true&badObserve'=false; 對每一次路徑建立過程來說，計數(shù)器observei并不清零，而是進(jìn)行累加。這使得攻擊者可以將對源自同一個發(fā)起者的多條路徑的觀察信息進(jìn)行累加。我們假定攻擊者可以驗證出兩條路經(jīng)是否源自同一個發(fā)送者。4.4協(xié)議的結(jié)束當(dāng)遇到攻擊者時我們就結(jié)束路徑建立過程，這是因為一旦碰到了惡意節(jié)點，則隨后的建立過程不會提供更多的關(guān)于發(fā)送者的信息給攻擊者，攻擊者所能獲知的就是上一跳的地址。這一點與Shmatikov[9]用PRISM分析Crowds協(xié)議時所采用的方法相同。但是如果在路徑建立過程沒有碰到惡意節(jié)點，Shmatikov的方法在理論上會產(chǎn)生死鎖狀態(tài)，原因是Shmatikov沒有對匿名路徑的長度進(jìn)行限制。我們用fixedNodeNum表示固定接收點數(shù)，F(xiàn)wLength表示變化路徑長度，而且我們認(rèn)為接收者也是一個固定接收點。這樣，如果在路徑建立過程中沒有碰到惡意節(jié)點，則當(dāng)fixedNodeNum的值為零時，路徑建立結(jié)束，避免了死鎖。//Ifallmembersinapatharehonest,terminatethepathsetupwhenitslengthincreasestothemaxlength.[](!good&!deliver&run&FwLength=0)->(fixedNodeNum'=fixedNodeNum-1)&(FwLength'=MaxFwLength);[]fixedNodeNum=0->deliver'=true;//Terminatetheprotocol[]deliver&run->done'=true&deliver'=false&run'=false&good'=false&bad'=false;//Startanewinstance[]done->new'=true&done'=false&run'=false;5匿名性質(zhì)的形式化與對Crowds的分析[3][9]類似，我們假定攻擊者能夠把源自同一個發(fā)送者的幾條路經(jīng)關(guān)聯(lián)起來。在攻擊者看來，如果某一個節(jié)點比其他節(jié)點更像是發(fā)送者，則他有理由認(rèn)為該節(jié)點就是真正的發(fā)送者。我們要回答的問題就是攻擊者猜測出發(fā)送者的概率有多大。我們將在表示W(wǎng)onGoo系統(tǒng)的Markov鏈上構(gòu)造PCTL公式對這個問題進(jìn)行討論。我們用表示攻擊者觀察到WonGoo成員的次數(shù)。其意思是在由同一發(fā)送者發(fā)起的多條路徑中，經(jīng)過節(jié)點并且的下一跳是惡意節(jié)點的路徑有條。用表示發(fā)送者被觀察到的次數(shù)。這包括兩種情況，一是惡意節(jié)點被選為第一個轉(zhuǎn)發(fā)者；二是發(fā)送者本身被選為一個中轉(zhuǎn)節(jié)點，其下一跳是一個惡意節(jié)點。我們采用Shmatikov在文獻(xiàn)[9]中提出的方法來驗證WonGoo成員。如果一個成員被觀察到的次數(shù)比其他成員的都多，即，，則我們認(rèn)為該成員是發(fā)送者。為此，定義以下事件：，（發(fā)起者被觀察到次數(shù)大于其他任何成員的）。于是我們要驗證的概率為：（猜測到真正的發(fā)起者）。上述匿名性質(zhì)用PCTL描述如下：//DetectionP=?[trueU(new&runCount=0&observe0>observe1&…&observe0>observe9)]6驗證結(jié)果我們利用PRISM模型驗證器對WonGoo系統(tǒng)的不同配置進(jìn)行概率模型驗證。表2描述了不同規(guī)模下的狀態(tài)空間，其中，固定節(jié)點數(shù)fixedNodeNum=3，變化路徑長度FwLength=3。從表中可知，與其他的模型驗證一樣，隨著系統(tǒng)規(guī)模的增大，狀態(tài)空間增長很快，這使得分析大規(guī)模WonGoo系統(tǒng)變得困難。如何解決模型驗證中狀態(tài)空間爆炸問題是該領(lǐng)域的一個難題。表表2狀態(tài)空間Table2SizeofstatespaceWonGoo源自同一發(fā)送者的路徑數(shù)（TotalRuns）345610honestmembersstates112,890524,0261,955,8526,232,410transitions308,7701,439,3065,391,23217,232,49015honestmembersstates332,9002,099,87610,460,61243,785,236transitions1,126,5957,130,77135,631,407149,556,43120honestmembersstates734,9605,860,62636,518,022189,355,322transitions2,964,72023,708,786148,121,382769,919,48225honestmembersstates1,373,82013,244,27699,077,582612,790,418transitions6,434,77062,186,726466,274,6572,890,100,243表3計算了不同路徑數(shù)下的驗證概率，從中可以看出以下兩點：隨著攻擊者所觀察到的源自同一發(fā)送者的路徑的增多，系統(tǒng)的匿名性降低。因此，在WonGoo中，一次會話（發(fā)送者和接收者之間的一次通信）只通過一條路徑完成，而不像Peekabooty所建議的那樣，一次會話通過多條路徑完成，既所謂的多路徑路由。在惡意節(jié)點比例（badC=0.167）不變時，驗證概率隨著系統(tǒng)規(guī)模的增大而減小。這說明系統(tǒng)的匿名性隨著規(guī)模的增加而增加。表3不同路徑數(shù)下的驗證概率（PF=0.3,fixedNodeNum=3,FwLength=3）。Table3ProbabilitiesofdetectingtheinitiatorincreasewithincreasingTotalRunsTable3ProbabilitiesofdetectingtheinitiatorincreasewithincreasingTotalRunsWonGoo源自同一發(fā)送者的路徑數(shù)（TotalRuns）345610honest,1corruptPr(%)17.2917.8618.5119.1215honest,2corruptPr(%)17.4718.0019.3219.8910honest,2corruptPr(%)21.8524.2528.0932.2115honest,3corruptPr(%)19.9322.0725.8728.4320honest,4corruptPr(%)18.9620.9723.5125.3725honest,5corruptPr(%)18.3919.9822.8324.78YongGuan等人[10]研究指出，通常情況下，匿名性隨著匿名路徑長度的增加而增加。WonGoo正是在保證足夠匿名的前提下，通過延長匿名路徑，從而進(jìn)一步提高了系統(tǒng)的匿名性。表4和表5分別描述了WonGoo的匿名性隨路徑長度的變化關(guān)系。表4通過調(diào)整轉(zhuǎn)發(fā)概率Pf的大小來調(diào)整路徑長度。表5通過調(diào)整固定節(jié)點數(shù)fixedNodeNum來調(diào)整路徑長度。可以看出，隨著匿名路徑的增長，驗證概率降低，從而系統(tǒng)的匿名性得到了提高。表表4不同轉(zhuǎn)發(fā)概率下的驗證概率（fixedNodeNum=4,FwLength=5,Totalrun=3）Table4Probabilitiesofdetectingtheinitiatordecreasewithincreasingforwardprobabilities WonGooPF10honest,1corruptPr(%)17.9417.1016.0614.6712.7910.397.735.403.8715honest,2corruptPr(%)17.7216.5415.2013.6311.799.747.736.094.9710honest,2corruptPr(%)21.8420.5819.2617.8816.4415.0113.6612.4411.2815honest,3corruptPr(%)19.7818.4617.0815.6614.2012.7711.4910.419.4620honest,4corruptPr(%)18.7517.4016.0014.5513.0911.6810.439.428.5725honest,5corruptPr(%)18.1516.7915.3813.9212.4511.059.838.858.07表表5不同固定節(jié)點數(shù)下的驗證概率（PF=0.3,FwLength=5,Totalrun=3）Table5ProbabilitiesofdetectingtheinitiatordecreasewithincreasingfixednodenumbersWonGoofixedNodeNum2468101210honest,1corruptPr(%)20.6216.0612.8010.709.468.7815honest,2corruptPr(%)22.1815.2011.439.538.648.2610honest,2corruptPr(%)27.7019.2616.2115.3215.1815.1615honest,3corruptPr(%)26.0017.0813.8212.7612.4912.4720honest,4corruptPr(%)25.1316.0012.6511.5211.1811.1225honest,5corruptPr(%)24.6215.3811.9810.8110.4410.35

7結(jié)論形式化方法是對安全協(xié)議進(jìn)行驗證的一種有力工具。如何利用已有的形式化方法對匿名協(xié)議進(jìn)行分析是一個極具挑戰(zhàn)的問題。概率模型驗證是一種十分有效的協(xié)議形式化分析工具。本文利用PRISM模型驗證器對匿名通信協(xié)議WonGoo進(jìn)行了分析。WonGoo通過隨機(jī)轉(zhuǎn)發(fā)和分層加密建立匿名通信路徑。因此，我們把WonGoo的路徑建立過程模型化為一個離散時間Markov鏈，并在攻擊者可以識別出兩條鏈路是否源自同一發(fā)送者的假設(shè)下，分析了攻擊者識別出一條匿名路徑的發(fā)起者的概率。WonGoo協(xié)議的分析表明了利用概率模型驗證技術(shù)分析安全協(xié)議的可行性。

References: T.Lu,B.Fang,Y.Sun,X.Cheng.WonGoo:APeer-to-PeerProtocolforAnonymousCommunication,InProceedingsofthe2004InternationalConferenceonParallelandDistributedProcessingTechniquesandApplications(PDPTA04),June2004:1102-1106.D.Chaum.Untraceableelectronicmail,returnaddressesanddigitalpseudonyms.CommunicationsoftheACM,February1981,24(2):84-88. M.K.ReiterandA.D.Rubin.Crowds:AnonymityforWebTransactions.ACMTransactionsonInformationandSystemSecurity,November1998,1(1):66-92. A.PfitzmannandM.K?hntopp.Anonymity,Unobservability,andPseudonymity–AProposalforTerminology,Draftv0.14./anonbib/papers/Anon_Terminology_v0.14.pdf,May2003.H.HanssonandB.Jonsson.Alogicforreasoningabouttimeandreliability.FormalAspectsofComputing,1994,6(5):512-535.http://www.cs.bham.ac.uk/~dxp/prismE.M.Clarke,E.A.Emerson,andA.P.Sistla.Automaticverificationoffinite-stateconcurrentsystemsusingtemporallogicspecification.ACMTrans.onProgrammingLanguagesandSystems,1986,8(2):244-263.D.Parker.ImplementationofSymbolicModelCheckingforProbabilisticSystems.Ph.D.Thesis,UniversityofBirmingham,AugustV.Shmatikov.ProbabilisticAnalysisofAnonymity.InProc.15thIEEEComputerSecurityFoundationsWorkshop(CSFW'02),June2002:119-128.Y.Guan,X.Fu,R.Bettati,andW.Zhao,"AnOptimalStrategyforAnonymousCommunicationProtocols,"inProceedingsofthe22ndIEEEInternationalConferenceonDistributedComputingSystems(ICDCS2002),July2002:257-266.派遣員工檔案管理制度為進(jìn)一步健全我單位規(guī)章制度，維護(hù)單位