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

收稿日期：2004-11基金项目:国家自然科学基金(60273016)，国家“八六三”高技术研究发展计划基金（2001AA142110）及中国科学院计算技术研究所基金(20016250)资助。作者简介:陆天波，博士研究生，主要研究方向为网络信息安全、分布式计算；方滨兴，研究员，博士生导师，主要研究方向为网络信息安全、并行计算；孙毓忠：研究员，博士生导师，主要研究方向为计算机系统结构；郭丽，副研究员，硕士生导师，主要研究方向为网络信息安全。匿名协议WonGoo的概率模型验证分析陆天波，方滨兴，孙毓忠，郭丽（中国科学院计算技术研究所软件研究室北京100080）（中国科学院研究生院北京100039）（[e-mail]）摘要Internet隐私的一个主要问题是缺乏匿名保护。近年来，人们已经针对这一问题做了很多工作。然而，如何利用已有的形式化方法分析匿名技术却是一个极具挑战的问题。对P2P匿名通信协议WonGoo进行了形式化分析。利用离散时间Markov链模型化节点和攻击者的行为。系统的匿名性质采用时序逻辑PCTL进行描述。利用概率模型验证器PRISM对WonGoo系统的匿名性进行了自动验证。结果表明WonGoo的匿名性随着系统规模的增加而增加；但却随着攻击者观察到的源自同一个发送者的路径的增加而降低。另外，匿名路径越长，系统的匿名性越强。关键词匿名；点对点；WonGoo；概率模型验证中图法分类号TP393AnalysisofAnonymityProtocolWonGoowithProbabilisticModelCheckingLUTian-bo,FANGBin-xing,SUNYu-zhong,GUOLi(InstituteofComputingTechnology,ChineseAcademyofSciences,Beijing,P.R.China,100080)(GraduateSchooloftheChineseAcademyofSciences,Beijing,P.R.China,100039)AbtractOneofthemainprivacyproblemsinInternetislackofanonymity.Muchworkhasbeendoneonthisprobleminrecentyears.However,itisachallengetoanalyzeanonymityprotocolformally.Thispaperpresentsformalanalysisofpeer-to-peeranonymouscommunicationprotocolWonGoo.Thebehaviorofgroupmembersandtheadversaryismodeledasadiscrete-timeMarkovchain,andsecuritypropertiesareexpressedasPCTLformulas.UsingtheprobabilisticmodelcheckerPRISM,itanalyzestheanonymityguaranteestheprotocolisintendedtoprovide.Asaresult,itnotonlyfindsthatanonymityprovidedbyWonGooincreaseswiththeincreaseingroupsizeanddegradeswiththeincreaseinthenumberofrandomroutingpaths,butitalsoshowstherelationshipbetweenanonymityandpathlength.Keywordsanonymity,Peer-to-Peer,WonGoo,ProbabilisticModelChecking1引言Internet的一个缺陷是不提供匿名保护，攻击者可以根据通信流之间的关系对发送者和接收者进行追踪。随着Internet的快速发展并被人们广为接受，以及搜索引擎和数据挖掘等技术的发展，人们已经开始关注Internet上的隐私和匿名。隐私不仅意味着信息的机密性，而且意味着信息发布者身份的机密性。匿名技术是Internet上保护用户隐私的一种有效手段，它通过一定的方法将通信流中的通信关系加以隐藏，使攻击者无法获知双方的通信关系或通信的一方。用户在通信过程中，通过隐藏自己的IP地址来保护自己的隐私。例如，用户访问了某个网站，但是由于用户使用了匿名技术，使得该访问活动无法与用户身份信息（指IP地址）关联起来，这在一定程度上保护了用户的隐私。加密技术可以保护通信的内容，但是攻击者可以通过通信流分析(Trafficanalysis)手段观察出谁和谁在通信，通信的时间以及通信流的多少等。因此，加密技术并不能保证通信的安全，尤其是在一个大的开放的环境中，保护通信者的身份就显得更加困难。本文中通信者的身份是指其IP地址，因此发送者是指发送者的IP地址，同样，接收者是指接收者的IP地址。我们所提出的WonGoo协议[1]是一个综合了Mix[2]和Crowds[3]的优点的可扩展点对点协议，提供三种形式的匿名保护：发送方匿名（senderanonymity），即消息无法被关联到其发送者；接收方匿名（receiveranonymity），即消息无法被关联到其接收者；关系匿名（relationshipanonymity），即消息的发送方和接收方是不可关联的（unlinkability）[4]。WonGoo克服了Mix效率低和Crowds抗攻击性差的缺点，通过分层加密和随机转发取得了强匿名和高效率。我们在文献[1]中分析了WonGoo的效率和匿名性介于Crowds和Mix之间，是Crowds和Mix的折中。模型验证（ModelChecking）技术是安全协议形式化分析的一项重要技术，它最早应用于硬件的性能验证中。随着信息安全技术的不断发展，被逐渐应用于安全协议的形式化分析中。本文利用概率模型验证（ProbabilisticModelChecking）技术分析了WonGoo系统的匿名性。我们把WonGoo系统形式化为一个离散时间Markov链（discrete-timeMarkovchains，DTMCs）模型，利用时序逻辑PCTL（ProbabilisticComputationalTreeLogic）[5]来描述WonGoo系统的匿名性质，并用概率模型验证器PRISM[6]进行验证。我们所考虑的问题是攻击者是否能够确定谁是一条匿名路径的发起者。我们假定攻击者可以观察部分网络通信流，可以运行自己的WonGoo节点，可以控制其他的部分WonGoo节点。但是，攻击者不能破坏系统所采用的加密技术。2概率模型验证技术模型验证是一种验证有限状态系统的自动化分析技术。系统被模型化为一个状态转化图，系统的性质用时序逻辑描述。它通过一个有效的搜索过程来验证状态转化图是否满足某种性质。我们可以把模型验证抽象的描述为：给定一个模型M和逻辑描述的性质P，检查M╞P，即在模型M中性质P是否成立。模型验证的最大优点在于验证过程是全自动化的，并且如果一个性质不满足，它能给出反例说明这个性质不满足的理由。概率模型验证是模型验证技术的扩充，主要用于自动验证具有随机行为的系统中某些事件发生的概率。例如在系统运行过程中验证事件“停机的概率不超过0.1”和“视频帧在5毫秒内到达的概率不低于0.9”等。概率模型验证中系统的形式化模型被赋予了概率信息，典型的情况是模型的每一个状态转化都标记有一个概率，用于说明状态转化的可能性。我们在本文中用到的模型是离散时间Markov链（DTMCs），其他两个常用的模型是连续时间Markov链（continuous-timeMarkovchains，CTMCs）和Markov决策过程（Markovdecisionprocesses，MDPs）。2.1离散时间Markov链（DTMCs）一个带标记函数的离散时间Markov链D是一个四元组),,,(LPsS，其中S是一个有限状态的集合；Ss是初始状态；]1,0[:SSP是一个转移概率矩阵，满足SsssP'1)',(，对任意的Ss；APSL2:是一个标记函数，表示原子命题在状态s成立，其中AP是一个原子命题集合。转移概率矩阵的元素)',(ssP给出了从状态s到状态's的转移概率。系统的一次执行可用一条通过DTMCs的路径表示。本文中WonGoo系统的一次执行是指一条WonGoo路径的建立过程。一条通过DTMCs的路径是一个有穷（或者无穷）的状态序列...210sss，其中对任意的0i，有0),(1iissP。我们把始于状态s的路径的集合记为sPath。2.2DTMCs上的PCTL模型验证PCTL是对时序逻辑CTL（ComputationalTreeLogic）[7]的扩充和发展。它在CTL基础之上增加了概率算子)(~pP，其中]1,0[p，},,,{~。PCTL的语法如下：)(||||::~pPtrue||::kX其中是原子命题，k是一个整数，是一个状态公式，是一个路径公式。概率算子)(~pP的意思是，如果一条路径源于状态s且满足路径公式的概率满足条件p~，则认为公式)(~pP在状态s是满足的。可以表示成下列公式：s╞)(~pPpPs~)(其中}||{)(sssPathPP。文献[8]对这一概率的计算过程进行了讨论。PRISM支持三种类型的路径公式：X，21k和21。路径满足路径公式，记为╞。下面给出PCTL在DTMCs上的语义描述。对于一条路径：|)1(|X（的第二个状态满足公式）),|)(|)(.(|1221ijjikik（的前k个状态中的某个满足2，同时该状态以前的所有状态都满足1）2121|.0|kk对于一个状态Ss:trues|forallSs)(|sLs2121|||sss||ssppPssp~)()(|~对于公式21来说，常用的形式是true1。如果一个状态s满足性质)(~truePp，则从状态s到达满足公式的状态的概率满足条件p~。2.3PRISM模型验证器PRISM[6]是由英国伯明翰大学开发的一个概率模型验证器。它支持三种模型，DTMCs，CTMCs和MDPs。在PRISM中，系统的行为用PRISM语言进行描述。一个系统被构建成几个模块，这些模块之间利用标准的进程代数运算进行交互。一个模块包括一些变量，用于表示系统的状态。系统的行为用一些监视命令（guardedcommand）表示。监视命令的格式如下：[]guard-command;其中，guard是系统变量上的断言，command描述状态转移，其转移的条件是guard为真。如果状态转移是不确定的，则command的形式为：prob:command+···+prob:commandPRISM根据对系统的描述进行建模并确定可达状态的集合。待验证的系统性质用时序逻辑PCTL或CTL进行描述。对于本文用到的DTMCs来说，我们是用PCTL进行描述的。3WonGoo协议设Alice与Bob进行通信，Alice首先选择一些WonGoo节点，我们称之为固定接收点。固定接收点的功能与Chaum描述的Mix节点的功能相似。Alice利用这些固定接收点的公钥对要发送的消息进行分层加密，构造出WonGoo数据包，然后以概率fp转发给一个随机选定的节点，称为概率接收点，以概率fp1转发给下一个固定接收点。随后的每个节点（包括固定接收点和概率接收点）都进行类似的操作。当WonGoo数据包到达接收者Bob以后，就形成了一条WonGoo