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

匿名协议WonGoo的概率模型验证分析陆天波，方滨兴，孙毓忠，郭丽（中国科学院计算技术研究所软件研究室北京100080）（中国科学院研究生院北京100039）（lutianbo@software.ict.ac.cn）摘要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地第2页共9页编号：时间：2021年x月x日书山有路勤为径，学海无涯苦作舟页码：第2页共9页址。我们所提出的WonGoo协议[1]是一个综合了Mix[2]和Crowds[3]的优点的可扩展点对点协议，提供三种形式的匿名保护：发送方匿名（senderanonymity），即消息无法被关联到其发送者；接收方匿名（receiveranonymity），即消息无法被关联到其接收者；关系匿名（relationshipanonymity），即消息的发送方和接收方是不可关联的（unlinkability）[4]。WonGoo克服了Mix效率低和Crowds抗攻击性差的缺点，通过分层加密和随机转发取得了强匿名和高效率。我们在文献[1]中分析了WonGoo的效率和匿名性介于Crowds和Mix之间，是Crowds和Mix的折中。模型验证（ModelChecking）技术是安全协议形式化分析的一项重要技术，它最早应用于硬件的性能验证中。随着信息安全技术的不断发展，...