匿名協議WonGoo的概率模型驗證分析.doc

匿名協議WonGoo的概率模型驗證分析陸天波，方濱興，孫毓忠，郭麗（中國科學院計算技術研究所軟件研究室 北京 100080）（中國科學院研究生院 北京 100039）（）摘 要Internet隱私的一個主要問題是缺乏匿名保護。近年來，人們已經針對這一問題做了很多工作。然而，如何利用已有的形式化方法分析匿名技術卻是一個極具挑戰(zhàn)的問題。對P2P匿名通信協議WonGoo進行了形式化分析。利用離散時間Markov鏈模型化節(jié)點和攻擊者的行為。系統的匿名性質采用時序邏輯PCTL進行描述。利用概率模型驗證器PRISM對WonGoo系統的匿名性進行了自動驗證。結果表明WonGoo的匿名性隨著系統規(guī)模的增加而增加；但卻隨著攻擊者觀察到的源自同一個發(fā)送者的路徑的增加而降低。另外，匿名路徑越長，系統的匿名性越強。關鍵詞匿名；點對點；WonGoo；概率模型驗證中圖法分類號TP393Analysis of Anonymity Protocol WonGoo with Probabilistic Model CheckingLU Tian-bo, FANG Bin-xing, SUN Yu-zhong, GUO Li(Institute of Computing Technology, Chinese Academy of Sciences, Beijing, P.R.China, 100080)(Graduate School of the Chinese Academy of Sciences, Beijing, P.R.China, 100039)Abtract 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 formal 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 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 anonymity, Peer-to-Peer, WonGoo, Probabilistic Model Checking 1引言Internet的一個缺陷是不提供匿名保護，攻擊者可以根據通信流之間的關系對發(fā)送者和接收者進行追蹤。隨著Internet的快速發(fā)展并被人們廣為接受，以及搜索引擎和數據挖掘等技術的發(fā)展，人們已經開始關注Internet上的隱私和匿名。隱私不僅意味著信息的機密性，而且意味著信息發(fā)布者身份的機密性。匿名技術是Internet上保護用戶隱私的一種有效手段，它通過一定的方法將通信流中的通信關系加以隱藏，使攻擊者無法獲知雙方的通信關系或通信的一方。用戶在通信過程中，通過隱藏自己的IP地址來保護自己的隱私。例如，用戶訪問了某個網站，但是由于用戶使用了匿名技術，使得該訪問活動無法與用戶身份信息（指IP地址）關聯起來，這在一定程度上保護了用戶的隱私。加密技術可以保護通信的內容，但是攻擊者可以通過通信流分析(Traffic analysis)手段觀察出誰和誰在通信，通信的時間以及通信流的多少等。因此，加密技術并不能保證通信的安全，尤其是在一個大的開放的環(huán)境中，保護通信者的身份就顯得更加困難。本文中通信者的身份是指其IP地址，因此發(fā)送者是指發(fā)送者的IP地址，同樣，接收者是指接收者的IP地址。我們所提出的WonGoo協議1是一個綜合了Mix2和Crowds3的優(yōu)點的可擴展點對點協議，提供三種形式的匿名保護：發(fā)送方匿名（sender anonymity），即消息無法被關聯到其發(fā)送者；接收方匿名（receiver anonymity），即消息無法被關聯到其接收者；關系匿名（relationship anonymity），即消息的發(fā)送方和接收方是不可關聯的（unlinkability）4。WonGoo克服了Mix效率低和Crowds抗攻擊性差的缺點，通過分層加密和隨機轉發(fā)取得了強匿名和高效率。我們在文獻1中分析了WonGoo的效率和匿名性介于Crowds 和Mix之間，是Crowds和Mix的折中。模型驗證（Model Checking）技術是安全協議形式化分析的一項重要技術，它最早應用于硬件的性能驗證中。隨著信息安全技術的不斷發(fā)展，被逐漸應用于安全協議的形式化分析中。本文利用概率模型驗證（Probabilistic Model Checking）技術分析了WonGoo系統的匿名性。我們把WonGoo系統形式化為一個離散時間Markov鏈（discrete-time Markov chains，DTMCs）模型，利用時序邏輯PCTL（Probabilistic Computational Tree Logic）5來描述WonGoo系統的匿名性質，并用概率模型驗證器PRISM6進行驗證。我們所考慮的問題是攻擊者是否能夠確定誰是一條匿名路徑的發(fā)起者。我們假定攻擊者可以觀察部分網絡通信流，可以運行自己的WonGoo節(jié)點，可以控制其他的部分WonGoo節(jié)點。但是，攻擊者不能破壞系統所采用的加密技術。2概率模型驗證技術模型驗證是一種驗證有限狀態(tài)系統的自動化分析技術。系統被模型化為一個狀態(tài)轉化圖，系統的性質用時序邏輯描述。它通過一個有效的搜索過程來驗證狀態(tài)轉化圖是否滿足某種性質。我們可以把模型驗證抽象的描述為：給定一個模型M和邏輯描述的性質P，檢查MP，即在模型M中性質P是否成立。模型驗證的最大優(yōu)點在于驗證過程是全自動化的，并且如果一個性質不滿足，它能給出反例說明這個性質不滿足的理由。概率模型驗證是模型驗證技術的擴充，主要用于自動驗證具有隨機行為的系統中某些事件發(fā)生的概率。例如在系統運行過程中驗證事件“停機的概率不超過0.1”和“視頻幀在5毫秒內到達的概率不低于0.9”等。概率模型驗證中系統的形式化模型被賦予了概率信息，典型的情況是模型的每一個狀態(tài)轉化都標記有一個概率，用于說明狀態(tài)轉化的可能性。我們在本文中用到的模型是離散時間Markov鏈（DTMCs），其他兩個常用的模型是連續(xù)時間Markov鏈（continuous-time Markov chains，CTMCs）和Markov決策過程（Markov decision processes，MDPs）。2.1離散時間Markov鏈（DTMCs）一個帶標記函數的離散時間Markov鏈D是一個四元組 ，其中l(wèi) 是一個有限狀態(tài)的集合；l 是初始狀態(tài)；l 是一個轉移概率矩陣，滿足 ，對任意的；l 是一個標記函數，表示原子命題在狀態(tài)s成立，其中AP是一個原子命題集合。轉移概率矩陣的元素給出了從狀態(tài)到狀態(tài)的轉移概率。系統的一次執(zhí)行可用一條通過DTMCs的路徑表示。本文中WonGoo系統的一次執(zhí)行是指一條WonGoo路徑的建立過程。一條通過DTMCs的路徑是一個有窮（或者無窮）的狀態(tài)序列，其中對任意的，有。我們把始于狀態(tài)的路徑的集合記為。2.2 DTMCs上的PCTL模型驗證PCTL是對時序邏輯CTL（Computational Tree Logic）7的擴充和發(fā)展。它在CTL基礎之上增加了概率算子，其中，。PCTL的語法如下：其中是原子命題，是一個整數，是一個狀態(tài)公式，是一個路徑公式。概率算子的意思是，如果一條路徑源于狀態(tài)且滿足路徑公式的概率滿足條件，則認為公式在狀態(tài)是滿足的?？梢员硎境上铝泄剑?其中。文獻8對這一概率的計算過程進行了討論。PRISM支持三種類型的路徑公式：，和。路徑滿足路徑公式，記為。下面給出PCTL在DTMCs上的語義描述。對于一條路徑： （的第二個狀態(tài)滿足公式） （的前個狀態(tài)中的某個滿足，同時該狀態(tài)以前的所有狀態(tài)都滿足） 對于一個狀態(tài): for all 對于公式來說，常用的形式是。如果一個狀態(tài)s滿足性質，則從狀態(tài)到達滿足公式的狀態(tài)的概率滿足條件。2.3 PRISM模型驗證器PRISM6是由英國伯明翰大學開發(fā)的一個概率模型驗證器。它支持三種模型，DTMCs，CTMCs和MDPs。在PRISM中，系統的行為用PRISM語言進行描述。一個系統被構建成幾個模塊，這些模塊之間利用標準的進程代數運算進行交互。一個模塊包括一些變量，用于表示系統的狀態(tài)。系統的行為用一些監(jiān)視命令（guarded command）表示。監(jiān)視命令的格式如下： - ;其中，guard是系統變量上的斷言，command描述狀態(tài)轉移，其轉移的條件是guard為真。如果狀態(tài)轉移是不確定的，則command的形式為： : + + : PRISM根據對系統的描述進行建模并確定可達狀態(tài)的集合。待驗證的系統性質用時序邏輯PCTL或CTL進行描述。對于本文用到的DTMCs來說，我們是用PCTL進行描述的。3 WonGoo協議設Alice與Bob進行通信，Alice首先選擇一些WonGoo節(jié)點，我們稱之為固定接收點。固定接收點的功能與Chaum描述的Mix節(jié)點的功能相似。Alice利用這些固定接收點的公鑰對要發(fā)送的消息進行分層加密，構造出WonGoo數據包，然后以概率轉發(fā)給一個隨機選定的節(jié)點，稱為概率接收點，以概率轉發(fā)給下一個固定接收點。隨后的每個節(jié)點（包括固定接收點和概率接收點）都進行類似的操作。當WonGoo數據包到達接收者Bob以后，就形成了一條WonGoo路徑。隨后的所有消息以及從Bob返回到Alice的消息都沿著這條路徑進行傳遞。我們在文獻1中分析了攻擊者不能分辨出一條路徑上的固定接收點和概率接收點。在一個大的點對點匿名通信系統中，由于節(jié)點只擁有局部的拓撲信息，因此，在進行下一跳選擇時，可能會選擇到已經在路徑上出現過的節(jié)點，即節(jié)點可能會在路徑上重復出現。為了提高系統的匿名性，必須盡量減少重復節(jié)點出現的概率。WonGoo在路徑構造過程中，由發(fā)送者Alice確定的固定節(jié)點不允許重復。而且，每一個節(jié)點在進行概率轉發(fā)時，所選擇的下一跳節(jié)點不能與該節(jié)點本身以及上一跳節(jié)點相同。為了使分析變得簡單，本文假定節(jié)點可在WonGoo路徑上的任何位置重復出現。因此，WonGoo系統的匿名性實際上比本文分析的要高。為了后面敘述方便，我們定義固定路徑和變化路徑兩個概念。由一個固定接收點直接到達另一個固定接收點的一條路稱為固定路徑（發(fā)送者和接收者也被看成是固定接收點）。兩個固定接收點之間依據概率轉發(fā)所形成的路徑稱為變化路徑。顯然，當變化路徑長度為1時，則成為固定路徑。4 WonGoo的模型構造我們僅僅對WonGoo的路徑建立過程進行模型驗證，而對路徑建立完成以后的通信沒有進行模型驗證，原因是路徑一旦建立，那么路徑上的每一個轉發(fā)節(jié)點都是從固定的上一個節(jié)點接收消息，而且通信的內容是不會泄漏發(fā)送者的身份信息的。因此攻擊者不會從隨后的通信中獲得更多的關于發(fā)送者的信息。我們的Markov鏈模型中的狀態(tài)代表匿名路徑建立過程中系統所處的狀態(tài)。一個狀態(tài)完全由模型中的狀態(tài)變量所確定，見表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 & start=false;4.2 轉發(fā)節(jié)點的選擇發(fā)送者隨機的從個節(jié)點中選擇第一個概率接收點。假定個節(jié)點被選中的概率是相等的。我們把轉發(fā)節(jié)點的選擇模型化為兩次狀態(tài)轉移，一次確定所選擇的轉發(fā)節(jié)點是否是誠實的，另外一次確定轉發(fā)節(jié)點的身份。隨機選擇的轉發(fā)節(jié)點是惡意節(jié)點的概率為badC=C/N，是誠實節(jié)點的概率為goodC=1-badC。/ Good or bad WonGoo member (!good & !bad & !deliver & run) - goodC: (good=true) & (recordLast=true) & (run=false) +badC: bad=true & badObserve=true & run=false;如果轉發(fā)節(jié)點是誠實的，則它可能為N-C個誠實節(jié)點中的任意一個。轉發(fā)者的身份記錄在lastSeen變量中。記錄轉發(fā)者的身份是為了模擬以下行為：如果該轉發(fā)節(jié)點的下一個節(jié)點是惡意節(jié)點，則該惡意節(jié)點可以記錄下該轉發(fā)節(jié)點的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) & (recordLast=false) & (run=true) + 0.1: (lastSeen=9) & (recordLast=false) & (run=true);WonGoo協議中，每一個節(jié)點（包括惡意節(jié)點）都必須確定下一跳。轉發(fā)者以概率將數據轉發(fā)給隨機選定的概率接收點，以概率轉發(fā)給已經選好的下一個固定接收點。/ Good members, forward to a random selected node with probability PF, else deliver to the next fixed node. (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變量的值并紀錄在observei中而實現的。/ Bad members, remember from whom the message was received and terminate the protocol lastSeen=0 & badObserve - (observe0 = observe0 + 1) & deliver=true & run=true & badObserve=false; lastSeen=9 & badObserve - (observe9 = observe9 + 1) & deliver=true & run=true & badObserve=false;對每一次路徑建立過程來說，計數器observei并不清零，而是進行累加。這使得攻擊者可以將對源自同一個發(fā)起者的多條路徑的觀察信息進行累加。我們假定攻擊者可以驗證出兩條路經是否源自同一個發(fā)送者。4.4 協議的結束當遇到攻擊者時我們就結束路徑建立過程，這是因為一旦碰到了惡意節(jié)點，則隨后的建立過程不會提供更多的關于發(fā)送者的信息給攻擊者，攻擊者所能獲知的就是上一跳的地址。這一點與Shmatikov9用PRISM分析Crowds協議時所采用的方法相同。但是如果在路徑建立過程沒有碰到惡意節(jié)點，Shmatikov的方法在理論上會產生死鎖狀態(tài)，原因是Shmatikov沒有對匿名路徑的長度進行限制。我們用fixedNodeNum表示固定接收點數，FwLength表示變化路徑長度，而且我們認為接收者也是一個固定接收點。這樣，如果在路徑建立過程中沒有碰到惡意節(jié)點，則當fixedNodeNum的值為零時，路徑建立結束，避免了死鎖。/ 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 & deliver=false & run=false & good=false & bad=false; / Start a new instance done - new=true & done=false & run=false;5 匿名性質的形式化與對Crowds的分析39類似，我們假定攻擊者能夠把源自同一個發(fā)送者的幾條路經關聯起來。在攻擊者看來，如果某一個節(jié)點比其他節(jié)點更像是發(fā)送者，則他有理由認為該節(jié)點就是真正的發(fā)送者。我們要回答的問題就是攻擊者猜測出發(fā)送者的概率有多大。我們將在表示WonGoo系統的Markov鏈上構造PCTL公式對這個問題進行討論。我們用表示攻擊者觀察到WonGoo成員的次數。其意思是在由同一發(fā)送者發(fā)起的多條路徑中，經過節(jié)點并且的下一跳是惡意節(jié)點的路徑有條。用表示發(fā)送者被觀察到的次數。這包括兩種情況，一是惡意節(jié)點被選為第一個轉發(fā)者；二是發(fā)送者本身被選為一個中轉節(jié)點，其下一跳是一個惡意節(jié)點。我們采用Shmatikov在文獻9中提出的方法來驗證WonGoo成員。如果一個成員被觀察到的次數比其他成員的都多，即，則我們認為該成員是發(fā)送者。為此，定義以下事件：，（發(fā)起者被觀察到次數大于其他任何成員的）。于是我們要驗證的概率為： （猜測到真正的發(fā)起者）。上述匿名性質用PCTL描述如下：/Detection P = ? true U (new & runCount = 0 & observe0 observe1 & & observe0 observe9)6 驗證結果我們利用PRISM模型驗證器對WonGoo系統的不同配置進行概率模型驗證。表2描述了不同規(guī)模下的狀態(tài)空間，其中，固定節(jié)點數fixedNodeNum=3，變化路徑長度FwLength=3。從表中可知，與其他的模型驗證一樣，隨著系統規(guī)模的增大，狀態(tài)空間增長很快，這使得分析大規(guī)模WonGoo系統變得困難。如何解決模型驗證中狀態(tài)空間爆炸問題是該領域的一個難題。表2 狀態(tài)空間Table 2 Size of state spaceWonGoo源自同一發(fā)送者的路徑數（TotalRuns）345610 honest 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,382769,919,48225 honest membersstates1,373,82013,244,27699,077,582612,790,418transitions6,434,77062,186,726466,274,6572,890,100,243表3計算了不同路徑數下的驗證概率，從中可以看出以下兩點：l 隨著攻擊者所觀察到的源自同一發(fā)送者的路徑的增多，系統的匿名性降低。因此，在WonGoo中，一次會話（發(fā)送者和接收者之間的一次通信）只通過一條路徑完成，而不像Peekabooty所建議的那樣，一次會話通過多條路徑完成，既所謂的多路徑路由。l 在惡意節(jié)點比例（badC=0.167）不變時，驗證概率隨著系統規(guī)模的增大而減小。這說明系統的匿名性隨著規(guī)模的增加而增加。 表3 不同路徑數下的驗證概率（PF=0.3, fixedNodeNum=3, FwLength=3）。 Table 3 Probabilities of detecting the initiator increase with increasing TotalRuns WonGoo源自同一發(fā)送者的路徑數（TotalRuns）345610 honest, 1 corruptPr(%)17.2917.8618.5119.1215 honest, 2 corruptPr(%)17.4718.0019.3219.8910 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研究指出，通常情況下，匿名性隨著匿名路徑長度的增加而增加。WonGoo正是在保證足夠匿名的前提下，通過延長匿名路徑，從而進一步提高了系統的匿名性。表4和表5分別描述了WonGoo的匿名性隨路徑長度的變化關系。表4通過調整轉發(fā)概率Pf的大小來調整路徑長度。表5通過調整固定節(jié)點數fixedNodeNum來調整路徑長度?？梢钥闯?，隨著匿名路徑的增長，驗證概率降低，從而系統的匿名性得到了提高。表4 不同轉發(fā)概率下的驗證概率（fixedNodeNum=4, FwLength=5, Totalrun=3）Table 4 Probabilities of detecting the initiator decrease with increasing forward probabilitiesWonGooPF 10 honest, 1 corruptPr(%)17.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.6810.439.428.5725 honest, 5 corruptPr(%)18.1516.7915.3813.9212.4511.059.838.858.07表5 不同固定節(jié)點數下的驗證概率（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.7815 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 結論形式化方法是對安全協議進行驗證的一種有力工具。如何利用已有的形式化方法對匿名協議進行分析是一個極具挑戰(zhàn)的問題。概率模型驗證是一種十分有效的協議形式化分析工具。本文利用PRISM模型驗證器對匿名通信協議WonGoo進行了分析。WonGoo通過隨機轉發(fā)和分層加密建立匿名通信路徑。因此，我們把WonGoo的路徑建立過程模型化為一個離散時間Markov鏈，并在攻擊者可以識別出兩條鏈路是否源自同一發(fā)送者的假設下，分析了攻擊者識別出一條匿名路徑的發(fā)起者的概率。WonGoo協議的分析表明了利用概率模型驗證技術分析安全協議的可行性。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. Communi