匿名协议WonGoo的概率模型验证分析

1、匿名协议WonGoo的概率模型验证分析陆天波，方滨兴，孙毓忠，郭丽（中国科学院计算技术研究所软件研究室 北京 100080）（中国科学院研究生院 北京 100039）（n）摘 要IInteerneet隐私私的一个个主要问问题是缺缺乏匿名名保护。近年来来，人们们已经针针对这一一问题做做了很多多工作。然而，如何利利用已有有的形式式化方法法分析匿匿名技术术却是一一个极具具挑战的的问题。对P22P匿名名通信协协议WoonGooo进行行了形式式化分析析。利用用离散时时间Maarkoov链模模型化节节点和攻攻击者的的行为。系统的的匿名性性质采用用时序逻逻辑PCCTL进进行描述述。利用用概率模模型验证证器P

2、RRISMM对WoonGooo系统统的匿名名性进行行了自动动验证。结果表表明WoonGooo的匿匿名性随随着系统统规模的的增加而而增加；但却随随着攻击击者观察察到的源源自同一一个发送送者的路路径的增增加而降降低。另另外，匿匿名路径径越长，系统的的匿名性性越强。关键词匿名；点对点点；WoonGooo；概概率模型型验证中图法分分类号TP3393Anallysiis oof AAnonnymiity Prootoccol WonnGooo wiith Proobabbiliistiic MModeel CChecckinngLU TTiann-boo, FFANGG Biin-xxingg, SSU

3、N Yu-zhoong, GUUO LLi(Insstittutee off Coompuutinng TTechhnollogyy, CChinnesee Accadeemy of Sciiencces, Beeijiing, P.R.CChinna, 10000800)(Graaduaate Schhooll off thhe CChinnesee Accadeemy of Sciiencces, Beeijiing, P.R.CChinna, 10000399)Abtrractt OOne of thee maain priivaccy pprobblemms iin IInteerne

4、et iis llackk off annonyymitty. Mucch wworkk haas bbeenn doone on thiis pprobblemm inn reecennt yyearrs. Howweveer, it is a cchalllennge to anaalyzze aanonnymiity prootoccol forrmallly. Thhis papper preesennts forrmall annalyysiss off peeer-to-peeer aanonnymoous commmunnicaatioon pprottocool WWonGGo

5、o. Thhe bbehaavioor oof ggrouup mmembberss annd tthe advverssaryy iss moodelled as a ddisccrette-ttimee Maarkoov cchaiin, andd seecurrityy prropeertiies aree exxpreesseed aas PPCTLL foormuulass. UUsinng tthe proobabbiliistiic mmodeel cchecckerr PRRISMM, iit aanallyzees tthe anoonymmityy guuaraanteee

6、s thee prrotoocoll iss inntenndedd too prroviide. Ass a ressultt, iit nnot onlly ffindds tthatt annonyymitty pprovvideed bby WWonGGoo inccreaasess wiith thee inncreeasee inn grroupp siize andd deegraadess wiith thee inncreeasee inn thhe nnumbber of ranndomm rooutiing patths, buut iit aalsoo shhowss

7、thhe rrelaatioonshhip bettweeen aanonnymiity andd paath lenngthh.Key worrds anoonymmityy, PPeerr-too-Peeer, WoonGooo, Proobabbiliistiic MModeel CChecckinng1引言言Inteerneet的一一个缺陷陷是不提提供匿名名保护，攻击者者可以根根据通信信流之间间的关系系对发送送者和接接收者进进行追踪踪。随着着Intternnet的的快速发发展并被被人们广广为接受受，以及及搜索引引擎和数数据挖掘掘等技术术的发展展，人们们已经开开始关注注Intternne

8、t上上的隐私私和匿名名。隐私私不仅意意味着信信息的机机密性，而且意意味着信信息发布布者身份份的机密密性。匿匿名技术术是Innterrnett上保护护用户隐隐私的一一种有效效手段，它通过过一定的的方法将将通信流流中的通通信关系系加以隐隐藏，使使攻击者者无法获获知双方方的通信信关系或或通信的的一方。用户在在通信过过程中，通过隐隐藏自己己的IPP地址来来保护自自己的隐隐私。例例如，用用户访问问了某个个网站，但是由由于用户户使用了了匿名技技术，使使得该访访问活动动无法与与用户身身份信息息（指IIP地址址）关联联起来，这在一一定程度度上保护护了用户户的隐私私。加密密技术可可以保护护通信的的内容，但是攻攻

9、击者可可以通过过通信流流分析(Traaffiic aanallysiis)手手段观察察出谁和和谁在通通信，通通信的时时间以及及通信流流的多少少等。因因此，加加密技术术并不能能保证通通信的安安全，尤尤其是在在一个大大的开放放的环境境中，保保护通信信者的身身份就显显得更加加困难。本文中中通信者者的身份份是指其其IP地地址，因因此发送送者是指指发送者者的IPP地址，同样，接收者者是指接接收者的的IP地地址。我们所提提出的WWonGGoo协协议11是一一个综合合了Miix22和CCrowwds3的的优点的的可扩展展点对点点协议，提供三三种形式式的匿名名保护：发送方方匿名（sennderr annony

10、ymitty），即消息息无法被被关联到到其发送送者；接接收方匿匿名（rreceeiveer aanonnymiity），即消消息无法法被关联联到其接接收者；关系匿匿名（rrelaatioonshhip anoonymmityy），即即消息的的发送方方和接收收方是不不可关联联的（uunliinkaabillityy）44。WWonGGoo克克服了MMix效效率低和和Croowdss抗攻击击性差的的缺点，通过分分层加密密和随机机转发取取得了强强匿名和和高效率率。我们们在文献献1中分析析了WoonGooo的效效率和匿匿名性介介于Crrowdds 和和Mixx之间，是Crrowdds和MMix的的折中

11、。模型验证证（Moodell Chheckkingg）技术术是安全全协议形形式化分分析的一一项重要要技术，它最早早应用于于硬件的的性能验验证中。随着信信息安全全技术的的不断发发展，被被逐渐应应用于安安全协议议的形式式化分析析中。本本文利用用概率模模型验证证（Prrobaabillisttic Moddel Cheeckiing）技术分分析了WWonGGoo系系统的匿匿名性。我们把把WonnGooo系统形形式化为为一个离离散时间间Marrkovv链（ddisccrette-ttimee Maarkoov cchaiins，DTMMCs）模型，利用时时序逻辑辑PCTTL（PProbbabiilis

12、sticc Coompuutattionnal Treee LLogiic）5来来描述WWonGGoo系系统的匿匿名性质质，并用用概率模模型验证证器PRRISMM6进行验验证。我我们所考考虑的问问题是攻攻击者是是否能够够确定谁谁是一条条匿名路路径的发发起者。我们假假定攻击击者可以以观察部部分网络络通信流流，可以以运行自自己的WWonGGoo节节点，可可以控制制其他的的部分WWonGGoo节节点。但但是，攻攻击者不不能破坏坏系统所所采用的的加密技技术。2概率模模型验证证技术模型验证证是一种种验证有有限状态态系统的的自动化化分析技技术。系系统被模模型化为为一个状状态转化化图，系系统的性性质用时时序

13、逻辑辑描述。它通过过一个有有效的搜搜索过程程来验证证状态转转化图是是否满足足某种性性质。我我们可以以把模型型验证抽抽象的描描述为：给定一一个模型型M和逻逻辑描述述的性质质P，检检查MP，即即在模型型M中性性质P是是否成立立。模型型验证的的最大优优点在于于验证过过程是全全自动化化的，并并且如果果一个性性质不满满足，它它能给出出反例说说明这个个性质不不满足的的理由。概率模型型验证是是模型验验证技术术的扩充充，主要要用于自自动验证证具有随随机行为为的系统统中某些些事件发发生的概概率。例例如在系系统运行行过程中中验证事事件“停机的的概率不不超过00.1”和“视频帧帧在5毫毫秒内到到达的概概率不低低于0

14、.9”等。概率模型型验证中中系统的的形式化化模型被被赋予了了概率信信息，典典型的情情况是模模型的每每一个状状态转化化都标记记有一个个概率，用于说说明状态态转化的的可能性性。我们们在本文文中用到到的模型型是离散散时间MMarkkov链链（DTTMCss），其其他两个个常用的的模型是是连续时时间Maarkoov链（conntinnuouus-ttimee Maarkoov cchaiins，CTMMCs）和Maarkoov决策策过程（Marrkovv deecissionn prroceessees，MMDPss）。2.1离离散时间间Marrkovv链（DDTMCCs）一个带标标记函数数的离散散时

15、间MMarkkov链链D是一个个四元组组，其中中是一个有有限状态态的集合合；是初始状状态；是一个转转移概率率矩阵，满足 ，对任任意的；是一个标标记函数数，表示示原子命命题在状状态s成立，其中AAP是一一个原子子命题集集合。转移概率率矩阵的的元素给给出了从从状态到到状态的的转移概概率。系系统的一一次执行行可用一一条通过过DTMMCs的的路径表表示。本本文中WWonGGoo系系统的一一次执行行是指一一条WoonGooo路径径的建立立过程。一条通通过DTTMCss的路径径是一个个有穷（或者无无穷）的的状态序序列，其其中对任任意的，有。我我们把始始于状态态的路径径的集合合记为。2.2 DTMMCs上上

16、的PCCTL模模型验证证PCTLL是对时时序逻辑辑CTLL（Coompuutattionnal Treee LLogiic）7的的扩充和和发展。它在CCTL基基础之上上增加了了概率算算子，其其中，。PCCTL的的语法如如下：其中是原原子命题题，是一一个整数数，是一一个状态态公式，是一个个路径公公式。概概率算子子的意思思是，如如果一条条路径源源于状态态且满足足路径公公式的概概率满足足条件，则认为为公式在在状态是是满足的的。可以以表示成成下列公公式： 其中。文文献88对这这一概率率的计算算过程进进行了讨讨论。PRISSM支持持三种类类型的路路径公式式：，和。路径径满足路路径公式式，记为为。下面面给

17、出PPCTLL在DTTMCss上的语语义描述述。对于一条条路径： （的的第二个个状态满满足公式式） （的的前个状状态中的的某个满满足，同同时该状状态以前前的所有有状态都都满足）对于一个个状态: ffor alll 对于公式式来说，常用的的形式是是。如果果一个状状态s满满足性质质，则从从状态到到达满足足公式的的状态的的概率满满足条件件。2.3 PRIISM模模型验证证器PRISSM66是由由英国伯伯明翰大大学开发发的一个个概率模模型验证证器。它它支持三三种模型型，DTTMCss，CTTMCss和MDDPs。在PRRISMM中，系系统的行行为用PPRISSM语言言进行描描述。一一个系统统被构建建成

18、几个个模块，这些模模块之间间利用标标准的进进程代数数运算进进行交互互。一个个模块包包括一些些变量，用于表表示系统统的状态态。系统统的行为为用一些些监视命命令（gguarrdedd coommaand）表示。监视命命令的格格式如下下： -;其中，gguarrd是系系统变量量上的断断言，ccommmandd描述状状态转移移，其转转移的条条件是gguarrd为真真。如果果状态转转移是不不确定的的，则ccommmandd的形式式为： : + + : PRISSM根据据对系统统的描述述进行建建模并确确定可达达状态的的集合。待验证证的系统统性质用用时序逻逻辑PCCTL或或CTLL进行描描述。对对于本文文用

19、到的的DTMMCs来来说，我我们是用用PCTTL进行行描述的的。3 WoonGooo协议议设Aliice与与Bobb进行通通信，AAlicce首先先选择一一些WoonGooo节点点，我们们称之为为固定接接收点。固定接接收点的的功能与与Chaaum描描述的MMix节节点的功功能相似似。Allicee利用这这些固定定接收点点的公钥钥对要发发送的消消息进行行分层加加密，构构造出WWonGGoo数数据包，然后以以概率转转发给一一个随机机选定的的节点，称为概概率接收收点，以以概率转转发给下下一个固固定接收收点。随随后的每每个节点点（包括括固定接接收点和和概率接接收点）都进行行类似的的操作。当WoonGo

20、oo数据据包到达达接收者者Bobb以后，就形成成了一条条WonnGooo路径。随后的的所有消消息以及及从Boob返回回到Allicee的消息息都沿着着这条路路径进行行传递。我们在在文献1中中分析了了攻击者者不能分分辨出一一条路径径上的固固定接收收点和概概率接收收点。在一个大大的点对对点匿名名通信系系统中，由于节节点只拥拥有局部部的拓扑扑信息，因此，在进行行下一跳跳选择时时，可能能会选择择到已经经在路径径上出现现过的节节点，即即节点可可能会在在路径上上重复出出现。为为了提高高系统的的匿名性性，必须须尽量减减少重复复节点出出现的概概率。WWonGGoo在在路径构构造过程程中，由由发送者者Aliic

21、e确确定的固固定节点点不允许许重复。而且，每一个个节点在在进行概概率转发发时，所所选择的的下一跳跳节点不不能与该该节点本本身以及及上一跳跳节点相相同。为为了使分分析变得得简单，本文假假定节点点可在WWonGGoo路路径上的的任何位位置重复复出现。因此，WonnGooo系统的的匿名性性实际上上比本文文分析的的要高。为了后后面叙述述方便，我们定定义固定定路径和和变化路路径两个个概念。由一个个固定接接收点直直接到达达另一个个固定接接收点的的一条路路称为固固定路径径（发送送者和接接收者也也被看成成是固定定接收点点）。两两个固定定接收点点之间依依据概率率转发所所形成的的路径称称为变化化路径。显然，当变化

22、化路径长长度为11时，则则成为固固定路径径。4 WoonGooo的模模型构造造我们仅仅仅对WoonGooo的路路径建立立过程进进行模型型验证，而对路路径建立立完成以以后的通通信没有有进行模模型验证证，原因因是路径径一旦建建立，那那么路径径上的每每一个转转发节点点都是从从固定的的上一个个节点接接收消息息，而且且通信的的内容是是不会泄泄漏发送送者的身身份信息息的。因因此攻击击者不会会从随后后的通信信中获得得更多的的关于发发送者的的信息。我们的的Marrkovv链模型型中的状状态代表表匿名路路径建立立过程中中系统所所处的状状态。一一个状态态完全由由模型中中的状态态变量所所确定，见表11。表1 状态变

23、量Table 1 State variablesrunCCounntNumbber of patths connstrructted so farr (0) - (runnCouunt=runnCouunt-1) & nnew=fallse & sstarrt=truue & fiixeddNoddeNuum = MaxxfixxedNNodeeNumm & FwLLenggth = MaxxFwLLenggth;/ SStarrt tthe prootoccol sstarrt - llasttSeeen=0 &runn=ttruee & delliveer=fallse & sstarrt

24、=fallse;4.2 转发节节点的选选择发送者随随机的从从个节点点中选择择第一个个概率接接收点。假定个个节点被被选中的的概率是是相等的的。我们们把转发发节点的的选择模模型化为为两次状状态转移移，一次次确定所所选择的的转发节节点是否否是诚实实的，另另外一次次确定转转发节点点的身份份。随机机选择的的转发节节点是恶恶意节点点的概率率为baadC=C/NN，是诚诚实节点点的概率率为gooodCC=1-baddC。/ GGoodd orr baad WWonGGoo memmberr (!goood & !badd & !deelivver & rrun)-gooodCC: (goood=truue)

25、 & (reccorddLasst=truue) & (runn=ffalsse) +badCC: bbad=trrue & bbadOObseervee=ttruee & runn=ffalsse;如果转发发节点是是诚实的的，则它它可能为为N-CC个诚实实节点中中的任意意一个。转发者者的身份份记录在在lasstSeeen变变量中。记录转转发者的的身份是是为了模模拟以下下行为：如果该该转发节节点的下下一个节节点是恶恶意节点点，则该该恶意节节点可以以记录下下该转发发节点的的IP地地址。/ RRecoord thee laast WonnGooo meembeer wwho touucheed t

26、the messsagge, alll goood memmberrs mmay apppearr wiith equual / pprobbabiilitty rrecoordLLastt & WonnGoooSizze=110 -0.1: (llasttSeeen=0) & (reccorddLasst=fallse) & (ruun=truue) +0.1: (laastSSeenn=99) & (rrecoordLLastt=ffalsse) & (runn=ttruee);WonGGoo协协议中，每一个个节点（包括恶恶意节点点）都必必须确定定下一跳跳。转发发者以概概率将数数据转发发给

27、随机机选定的的概率接接收点，以概率率转发给给已经选选好的下下一个固固定接收收点。/ GGoodd meembeers, foorwaard to a rranddom sellectted nodde wwithh prrobaabillityy PFF, eelsee deelivver to thee neext fixxed nodde. (goood & !ddeliiverr & runn & FwLLenggth 00) -PF: (ggoodd=ffalsse) & (FwLLenggth=FwwLenngthh-1) +notPPF: (goood=faalsee)& (fii

28、xeddNoddeNuum=fixxedNNodeeNumm-1) & (FwwLenngthh=MaaxFwwLenngthh);4.3 恶意节节点的模模型化显然，匿匿名路径径上的节节点是知知道它前前一跳的的地址的的。如果果是恶意意节点，则它将将记录下下其上一一跳的IIP地址址。这是是通过读读取laastSSeenn变量的的值并纪纪录在oobseerveei中而实实现的。/ BBad memmberrs, remmembber froom wwhomm thhe mmesssagee waas rreceeiveed aand terrminnatee thhe pprottocool ll

29、asttSeeen=00 & baddObsservve - (obsservve0 = obsservve0 + 11) & deelivver=trrue&runn=ttruee& bbadOObseervee=ffalsse; llasttSeeen=99 & baddObsservve - (obsservve9 = obbserrve99 + 1) & ddeliiverr=ttruee & runn=ttruee & baddObsservve=fallse;对每一一次路径径建立过过程来说说，计数数器obbserrveii并不清清零，而而是进行行累加。这使得得攻击者者可以将将对源自

30、自同一个个发起者者的多条条路径的的观察信信息进行行累加。我们假假定攻击击者可以以验证出出两条路路经是否否源自同同一个发发送者。4.4 协议的的结束当遇到攻攻击者时时我们就就结束路路径建立立过程，这是因因为一旦旦碰到了了恶意节节点，则则随后的的建立过过程不会会提供更更多的关关于发送送者的信信息给攻攻击者，攻击者者所能获获知的就就是上一一跳的地地址。这这一点与与Shmmatiikovv9用PRRISMM分析CCrowwds协协议时所所采用的的方法相相同。但但是如果果在路径径建立过过程没有有碰到恶恶意节点点，Shhmattikoov的方方法在理理论上会会产生死死锁状态态，原因因是Shhmattiko

31、ov没有有对匿名名路径的的长度进进行限制制。我们们用fiixeddNoddeNuum表示示固定接接收点数数，FwwLenngthh表示变变化路径径长度，而且我我们认为为接收者者也是一一个固定定接收点点。这样样，如果果在路径径建立过过程中没没有碰到到恶意节节点，则则当fiixeddNoddeNuum的值值为零时时，路径径建立结结束，避避免了死死锁。/ IIf aall memmberrs iin aa paath aree hoonesst, terrminnatee thhe ppathh seet uup wwhenn itts llenggth inccreaasess too thhe

32、mmax lenngthh. (!goood & !ddeliiverr & runn & FwLLenggth = 00) - (ffixeedNoodeNNum= fiixeddNoddeNuum-11) & (FFwLeengtth= MaaxFwwLenngthh); ffixeedNoodeNNum=0 - ddeliiverr=ttruee;/ TTermminaate thee prrotoocoll ddeliiverr & runn - doone=trrue & ddeliiverr=ffalsse & ruun=fallse &goood=faalsee & badd=f

33、falsse;/ SStarrt aa neew iinsttancce ddonee - neew=truue & doone=faalsee & runn=ffalsse;5 匿名名性质的的形式化化与对Crrowdds的分分析3399类似似，我们们假定攻攻击者能能够把源源自同一一个发送送者的几几条路经经关联起起来。在在攻击者者看来，如果某某一个节节点比其其他节点点更像是是发送者者，则他他有理由由认为该该节点就就是真正正的发送送者。我我们要回回答的问问题就是是攻击者者猜测出出发送者者的概率率有多大大。我们们将在表表示WoonGooo系统统的Maarkoov链上上构造PPCTLL公式对对这个问

34、问题进行行讨论。我们用表表示攻击击者观察察到WoonGooo成员员的次数数。其意意思是在在由同一一发送者者发起的的多条路路径中，经过节节点并且且的下一一跳是恶恶意节点点的路径径有条。用表示示发送者者被观察察到的次次数。这这包括两两种情况况，一是是恶意节节点被选选为第一一个转发发者；二二是发送送者本身身被选为为一个中中转节点点，其下下一跳是是一个恶恶意节点点。我们采用用Shmmatiikovv在文献献9中提出出的方法法来验证证WonnGooo成员。如果一一个成员员被观察察到的次次数比其其他成员员的都多多，即，则我我们认为为该成员员是发送送者。为为此，定定义以下下事件：，（发起起者被观观察到次次数

35、大于于其他任任何成员员的）。于是我们们要验证证的概率率为： （猜猜测到真真正的发发起者）。上述匿名名性质用用PCTTL描述述如下：/Deetecctioon P = ? truue UU (nnew & rrunCCounnt = 0 & oobseervee0 obbserrve11 & & obsservve0 oobseervee9)6 验证证结果我们利用用PRIISM模模型验证证器对WWonGGoo系系统的不不同配置置进行概概率模型型验证。表2描描述了不不同规模模下的状状态空间间，其中中，固定定节点数数fixxedNNodeeNumm=3，变化路路径长度度FwLLenggth=3。从从

36、表中可可知，与与其他的的模型验验证一样样，随着着系统规规模的增增大，状状态空间间增长很很快，这这使得分分析大规规模WoonGooo系统统变得困困难。如如何解决决模型验验证中状状态空间间爆炸问问题是该该领域的的一个难难题。表2 状态空间Table 2 Size of state spaceWonGGoo源自同一一发送者者的路径径数（TTotaalRuuns）345610 hhoneest memmberrsstattes112,8900524,02661,9555,88526,2332,4410trannsittionns308,77001,4339,33065,3991,223217,2232

37、,490015 hhoneest memmberrsstattes332,90002,0999,887610,4460,612243,7785,2366trannsittionns1,1226,55957,1330,777135,6631,4077149,5566,433120 hhoneest memmberrsstattes734,96005,8660,662636,5518,0222189,3555,3222trannsittionns2,9664,772023,7708,7866148,1211,3882769,9199,488225 hhoneest memmberrsstattes

38、1,3773,882013,2244,276699,0077,5822612,7900,4118trannsittionns6,4334,777062,1186,7266466,2744,65572,8990,1100,2433表3计算算了不同同路径数数下的验验证概率率，从中中可以看看出以下下两点：随着攻击击者所观观察到的的源自同同一发送送者的路路径的增增多，系系统的匿匿名性降降低。因因此，在在WonnGooo中，一一次会话话（发送送者和接接收者之之间的一一次通信信）只通通过一条条路径完完成，而而不像PPeekkaboootyy所建议议的那样样，一次次会话通通过多条条路径完完成，既既所谓的的多

39、路径径路由。在恶意节节点比例例（baadC=0.1167）不变时时，验证证概率随随着系统统规模的的增大而而减小。这说明明系统的的匿名性性随着规规模的增增加而增增加。 表3 不同路径数下的验证概率（PF=0.3, fixedNodeNum=3, FwLength=3）。Table 3 Probabilities of detecting the initiator increase with increasing TotalRunsWonGGoo源自同一一发送者者的路径径数（TTotaalRuuns）345610 hhoneest, 1 corrrupptPr(%)17.22917.88618.

40、55119.11215 hhoneest, 2 corrrupptPr(%)17.44718.00019.33219.88910 hhoneest, 2 corrrupptPr(%)21.88524.22528.00932.22115 hhoneest, 3 corrrupptPr(%)19.99322.00725.88728.44320 hhoneest, 4 corrrupptPr(%)18.99620.99723.55125.33725 hhoneest, 5 corrrupptPr(%)18.33919.99822.88324.778Yongg Guuan等等人110研研究指出出，通常

41、常情况下下，匿名名性随着着匿名路路径长度度的增加加而增加加。WoonGooo正是是在保证证足够匿匿名的前前提下，通过延延长匿名名路径，从而进进一步提提高了系系统的匿匿名性。表4和和表5分分别描述述了WoonGooo的匿匿名性随随路径长长度的变变化关系系。表44通过调调整转发发概率PPf的大大小来调调整路径径长度。表5通通过调整整固定节节点数ffixeedNoodeNNum来来调整路路径长度度。可以以看出，随着匿匿名路径径的增长长，验证证概率降降低，从从而系统统的匿名名性得到到了提高高。表4 不同转发概率下的验证概率（fixedNodeNum=4, FwLength=5, Totalrun=3）

42、Table 4 Probabilities of detecting the initiator decrease with increasing forward probabilitiesWonGGooPF 0.10.20.30.40.50.60.70.80.910 hhoneest, 1 corrrupptPr(%)17.99417.11016.00614.66712.77910.3397.7335.4003.87715 hhoneest, 2 corrrupptPr(%)17.77216.55415.22013.66311.7799.7447.7336.0994.97710 hhonee

43、st, 2 corrrupptPr(%)21.88420.55819.22617.88816.44415.00113.66612.44411.22815 hhoneest, 3 corrrupptPr(%)19.77818.44617.00815.66614.22012.77711.44910.4419.46620 hhoneest, 4 corrrupptPr(%)18.77517.44016.00014.55513.00911.66810.4439.4228.57725 hhoneest, 5 corrrupptPr(%)18.11516.77915.33813.99212.44511.0

44、059.8338.8558.077表5 不同固定节点数下的验证概率（PF=0.3, FwLength=5, Totalrun=3）Table 5 Probabilities of detecting the initiator decrease with increasing fixed node numbersWonGGoofixeedNoodeNNum2468101210 hhoneest, 1 corrrupptPr(%)20.66216.00612.88010.7709.4668.78815 hhoneest, 2 corrrupptPr(%)22.11815.22011.4439.5

45、338.6448.26610 hhoneest, 2 corrrupptPr(%)27.77019.22616.22115.33215.11815.11615 hhoneest, 3 corrrupptPr(%)26.00017.00813.88212.77612.44912.44720 hhoneest, 4 corrrupptPr(%)25.11316.00012.66511.55211.11811.11225 hhoneest, 5 corrrupptPr(%)24.66215.33811.99810.88110.44410.3357 结论论形式化方方法是对对安全协协议进行行验证的的一种

46、有有力工具具。如何何利用已已有的形形式化方方法对匿匿名协议议进行分分析是一一个极具具挑战的的问题。概率模模型验证证是一种种十分有有效的协协议形式式化分析析工具。本文利利用PRRISMM模型验验证器对对匿名通通信协议议WonnGooo进行了了分析。WonnGooo通过随随机转发发和分层层加密建建立匿名名通信路路径。因因此，我我们把WWonGGoo的的路径建建立过程程模型化化为一个个离散时时间Maarkoov链，并在攻攻击者可可以识别别出两条条链路是是否源自自同一发发送者的的假设下下，分析析了攻击击者识别别出一条条匿名路路径的发发起者的的概率。WonnGooo协议的的分析表表明了利利用概率率模型验

47、验证技术术分析安安全协议议的可行行性。Refeerenncess:T. LLu, B. Fanng, Y. Sunn, XX. CChenng. WonnGooo: AA Peeer-to-Peeer PProttocool ffor Anoonymmouss Coommuuniccatiion, Inn Prroceeediingss off thhe 220044 Innterrnattionnal Connferrencce oon PParaalleel aand Disstriibutted Proocesssinng TTechhniqquess annd AAppllicaatioons (PDDPTAA04), JJunee 20004: 11102-11006.D. CChauum. Un