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

1、匿名協(xié)議WonGoo的概率模型驗證分析l 是一個有限狀態(tài)的集合；l 是初始狀態(tài)；l 是一個轉(zhuǎn)移概率矩陣，滿足，對任意的；l 是一個標記函數(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（ComputationalTr

2、eeLogic）7的擴充和發(fā)展。它在CTL基礎(chǔ)之上增加了概率算子，其中，。PCTL的語法如下：          其中是原子命題，是一個整數(shù)，是一個狀態(tài)公式，是一個路徑公式。概率算子的意思是，如果一條路徑源于狀態(tài)且滿足路徑公式的概率滿足條件，則認為公式在狀態(tài)是滿足的。可以表示成下列公式：     其中。文獻8對這一概率的計算過程進行了討論。PRISM支持三種類型的路徑公式：，和。路徑滿足路徑公式，記為。下面給出PCTL在DTMCs上的語義描述。對

3、于一條路徑：  （的第二個狀態(tài)滿足公式）   （的前個狀態(tài)中的某個滿足，同時該狀態(tài)以前的所有狀態(tài)都滿足）  對于一個狀態(tài):  forall        對于公式來說，常用的形式是。如果一個狀態(tài)s滿足性質(zhì)，則從狀態(tài)到達滿足公式的狀態(tài)的概率滿足條件。2.3PRISM模型驗證器PRISM6是由英國伯明翰大學開發(fā)的一個概率模型驗證器。它支持三種模型，DTMCs，CTMCs和MDPs。在PRISM中，系統(tǒng)的行為用PRISM語言進行描述

4、。一個系統(tǒng)被構(gòu)建成幾個模塊，這些模塊之間利用標準的進程代數(shù)運算進行交互。一個模塊包括一些變量，用于表示系統(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>:

5、<command>+<prob>:<command>PRISM根據(jù)對系統(tǒng)的描述進行建模并確定可達狀態(tài)的集合。待驗證的系統(tǒng)性質(zhì)用時序邏輯PCTL或CTL進行描述。對于本文用到的DTMCs來說，我們是用PCTL進行描述的。3WonGoo協(xié)議設(shè)Alice與Bob進行通信，Alice首先選擇一些WonGoo節(jié)點，我們稱之為固定接收點。固定接收點的功能與Chaum描述的Mix節(jié)點的功能相似。Alice利用這些固定接收點的公鑰對要發(fā)送的消息進行分層加密，構(gòu)造出WonGoo數(shù)據(jù)包，然后以概率轉(zhuǎn)發(fā)給一個隨機選定的節(jié)點，稱為概率接收點，以概率轉(zhuǎn)發(fā)給下一個固定接收點。隨后的每個

6、節(jié)點（包括固定接收點和概率接收點）都進行類似的操作。當WonGoo數(shù)據(jù)包到達接收者Bob以后，就形成了一條WonGoo路徑。隨后的所有消息以及從Bob返回到Alice的消息都沿著這條路徑進行傳遞。我們在文獻1中分析了攻擊者不能分辨出一條路徑上的固定接收點和概率接收點。在一個大的點對點匿名通信系統(tǒng)中，由于節(jié)點只擁有局部的拓撲信息，因此，在進行下一跳選擇時，可能會選擇到已經(jīng)在路徑上出現(xiàn)過的節(jié)點，即節(jié)點可能會在路徑上重復出現(xiàn)。為了提高系統(tǒng)的匿名性，必須盡量減少重復節(jié)點出現(xiàn)的概率。WonGoo在路徑構(gòu)造過程中，由發(fā)送者Alice確定的固定節(jié)點不允許重復。而且，每一個節(jié)點在進行概率轉(zhuǎn)發(fā)時，所選擇的下一跳

7、節(jié)點不能與該節(jié)點本身以及上一跳節(jié)點相同。為了使分析變得簡單，本文假定節(jié)點可在WonGoo路徑上的任何位置重復出現(xiàn)。因此，WonGoo系統(tǒng)的匿名性實際上比本文分析的要高。為了后面敘述方便，我們定義固定路徑和變化路徑兩個概念。由一個固定接收點直接到達另一個固定接收點的一條路稱為固定路徑（發(fā)送者和接收者也被看成是固定接收點）。兩個固定接收點之間依據(jù)概率轉(zhuǎn)發(fā)所形成的路徑稱為變化路徑。顯然，當變化路徑長度為1時，則成為固定路徑。4WonGoo的模型構(gòu)造我們僅僅對WonGoo的路徑建立過程進行模型驗證，而對路徑建立完成以后的通信沒有進行模型驗證，原因是路徑一旦建立，那么路徑上的每一個轉(zhuǎn)發(fā)節(jié)點都是從固定的上

8、一個節(jié)點接收消息，而且通信的內(nèi)容是不會泄漏發(fā)送者的身份信息的。因此攻擊者不會從隨后的通信中獲得更多的關(guān)于發(fā)送者的信息。我們的Markov鏈模型中的狀態(tài)代表匿名路徑建立過程中系統(tǒng)所處的狀態(tài)。一個狀態(tài)完全由模型中的狀態(tài)變量所確定，見表1。   runCount Numberofpathsconstructedsofar(<=TotalRuns).good Theselectedforwarderishonest.bad Theselectedforwarderisbad.lastSeen Identityoftheprec

9、edingforwarderonthepath.observei Numberoftimescorruptmembersobservedmemberi.new Readytoconstructanotherpath.start Beginningofnewpathconstruction.run Continuepathconstruction.deliver Terminatethepath.recordLast Recordtheidentityoftheprecedingforwarder.badObserve Hav

10、eacorruptmemberrecorditsobservations.fixedNodeNum NumberoffixedWonGoonodesinapath.FwLength ForwardpathlengthbetweentwofixedWonGoonodes.我們假定攻擊者除了有能力運行自己的WonGoo節(jié)點之外，還能控制部分其他的節(jié)點。我們把攻擊者自己的節(jié)點及被其控制的其他節(jié)點統(tǒng)稱為泄密節(jié)點，也叫泄密者；把沒有被攻擊者控制的節(jié)點，即非泄密者，稱為誠實的節(jié)點。誠實的節(jié)點不會為攻擊者提供任何信息。假設(shè)個成員的WonGoo網(wǎng)絡(luò)中有個泄密者，發(fā)送者Alice已經(jīng)利用節(jié)點

11、選擇算法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ā)送者(

12、observe0)發(fā)起的。這是通過在協(xié)議開始時設(shè)置變量lastSeen的值為零來實現(xiàn)的。同時，我們還要設(shè)置分別用于表示固定節(jié)點數(shù)和變化路徑長度的變量fixedNodeNum和FwLength的值。/Setupanewprotocolinstancenew&(runCount>0)->(runCount"=runCount-1)&new"=false&start"=true&fixedNodeNum"=MaxfixedNodeNum&FwLength"=MaxFwLength;/Startthe

13、protocolstart->lastSeen"=0&run"=true&deliver"=false&start"=false;4.2轉(zhuǎn)發(fā)節(jié)點的選擇發(fā)送者隨機的從個節(jié)點中選擇第一個概率接收點。假定個節(jié)點被選中的概率是相等的。我們把轉(zhuǎn)發(fā)節(jié)點的選擇模型化為兩次狀態(tài)轉(zhuǎn)移，一次確定所選擇的轉(zhuǎn)發(fā)節(jié)點是否是誠實的，另外一次確定轉(zhuǎn)發(fā)節(jié)點的身份。隨機選擇的轉(zhuǎn)發(fā)節(jié)點是惡意節(jié)點的概率為badC=C/N，是誠實節(jié)點的概率為goodC=1-badC。/GoodorbadWonGoomember(!good&!bad&!delive

14、r&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é)點可以

15、記錄下該轉(zhuǎn)發(fā)節(jié)點的IP地址。/RecordthelastWonGoomemberwhotouchedthemessage,allgoodmembersmayappearwithequal/probabilityrecordLast&WonGooSize=10->  0.1:(lastSeen"=0)&(recordLast"=false)&(run"=true)+    0.1:(lastSeen"=9)&(recordLast"=false)&a

16、mp;(run"=true);WonGoo協(xié)議中，每一個節(jié)點（包括惡意節(jié)點）都必須確定下一跳。轉(zhuǎn)發(fā)者以概率將數(shù)據(jù)轉(zhuǎn)發(fā)給隨機選定的概率接收點，以概率轉(zhuǎn)發(fā)給已經(jīng)選好的下一個固定接收點。/Goodmembers,forwardtoarandomselectednodewithprobabilityPF,elsedelivertothenextfixednode.(good&!deliver&run&FwLength>0)->PF:(good"=false)&(FwLength"=FwLength-1)+notPF:(good&

17、quot;=false)&(fixedNodeNum"=fixedNodeNum-1)&(FwLength"=MaxFwLength); 4.3惡意節(jié)點的模型化顯然，匿名路徑上的節(jié)點是知道它前一跳的地址的。如果是惡意節(jié)點，則它將記錄下其上一跳的IP地址。這是通過讀取lastSeen變量的值并紀錄在observei中而實現(xiàn)的。/Badmembers,rememberfromwhomthemessagewasreceivedandterminatetheprotocollastSeen=0&badObserve->(observe0&qu

18、ot;=observe0+1)&deliver"=true&run"=true&badObserve"=false;  lastSeen=9&badObserve->(observe9"=observe9+1)&deliver"=true&run"=true&badObserve"=false; 對每一次路徑建立過程來說，計數(shù)器observei并不清零，而是進行累加。這使得攻擊者可以將對源自同一個發(fā)起者的多條路徑的觀察信息進行累加。我

19、們假定攻擊者可以驗證出兩條路經(jīng)是否源自同一個發(fā)送者。4.4協(xié)議的結(jié)束當遇到攻擊者時我們就結(jié)束路徑建立過程，這是因為一旦碰到了惡意節(jié)點，則隨后的建立過程不會提供更多的關(guān)于發(fā)送者的信息給攻擊者，攻擊者所能獲知的就是上一跳的地址。這一點與Shmatikov9用PRISM分析Crowds協(xié)議時所采用的方法相同。但是如果在路徑建立過程沒有碰到惡意節(jié)點，Shmatikov的方法在理論上會產(chǎn)生死鎖狀態(tài)，原因是Shmatikov沒有對匿名路徑的長度進行限制。我們用fixedNodeNum表示固定接收點數(shù)，F(xiàn)wLength表示變化路徑長度，而且我們認為接收者也是一個固定接收點。這樣，如果在路徑建立過程中沒有碰到

20、惡意節(jié)點，則當fixedNodeNum的值為零時，路徑建立結(jié)束，避免了死鎖。/Ifallmembersinapatharehonest,terminatethepathsetupwhenitslengthincreasestothemaxlength.(!good&!deliver&run&FwLength=0)->(fixedNodeNum"=fixedNodeNum-1)&(FwLength"=MaxFwLength);fixedNodeNum=0->deliver"=true;/Terminatetheprotoc

21、oldeliver&run->done"=true&deliver"=false&run"=false&good"=false&bad"=false;/Startanewinstancedone->new"=true&done"=false&run"=false;5匿名性質(zhì)的形式化與對Crowds的分析39類似，我們假定攻擊者能夠把源自同一個發(fā)送者的幾條路經(jīng)關(guān)聯(lián)起來。在攻擊者看來，如果某一個節(jié)點比其他節(jié)點更像是發(fā)送者，則他有理由認為該節(jié)點就是真正的

22、發(fā)送者。我們要回答的問題就是攻擊者猜測出發(fā)送者的概率有多大。我們將在表示W(wǎng)onGoo系統(tǒng)的Markov鏈上構(gòu)造PCTL公式對這個問題進行討論。我們用表示攻擊者觀察到WonGoo成員的次數(shù)。其意思是在由同一發(fā)送者發(fā)起的多條路徑中，經(jīng)過節(jié)點并且的下一跳是惡意節(jié)點的路徑有條。用表示發(fā)送者被觀察到的次數(shù)。這包括兩種情況，一是惡意節(jié)點被選為第一個轉(zhuǎn)發(fā)者；二是發(fā)送者本身被選為一個中轉(zhuǎn)節(jié)點，其下一跳是一個惡意節(jié)點。我們采用Shmatikov在文獻9中提出的方法來驗證WonGoo成員。如果一個成員被觀察到的次數(shù)比其他成員的都多，即，則我們認為該成員是發(fā)送者。為此，定義以下事件：，（發(fā)起者被觀察到次數(shù)大于其他任

23、何成員的）。于是我們要驗證的概率為：（猜測到真正的發(fā)起者）。上述匿名性質(zhì)用PCTL描述如下：/DetectionP=?trueU(new&runCount=0&observe0>observe1&&observe0>observe9)6驗證結(jié)果我們利用PRISM模型驗證器對WonGoo系統(tǒng)的不同配置進行概率模型驗證。表2描述了不同規(guī)模下的狀態(tài)空間，其中，固定節(jié)點數(shù)fixedNodeNum=3，變化路徑長度FwLength=3。從表中可知，與其他的模型驗證一樣，隨著系統(tǒng)規(guī)模的增大，狀態(tài)空間增長很快，這使得分析大規(guī)模WonGoo系統(tǒng)變得困難。如何解決模型驗證中狀態(tài)空間爆炸問題是該領(lǐng)域的一個難題。WonGoo 源自同一發(fā)送者的路徑數(shù)（TotalRuns） 3 4 5 610honestmembers states 112,890