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

匿名协议 WonGoo 的概率模型验证分析陆天波，方滨兴，孙毓忠，郭丽（中国科学院计算技术研究所软件研究室 北京 100080）（中国科学院研究生院 北京 100039）（lutianbo@software.ict.ac.cn）摘 要Internet 隐私的一个主要问题是缺乏匿名保护。近年来，人们已经针对这一问题做了很多工作。然而，如何利用已有的形式化方法分析匿名技术却是一个极具挑战的问题。对 P2P 匿名通信协议 WonGoo 进行了形式化分析。利用离散时间 Markov 链模型化节点和攻击者的行为。系统的匿名性质采用时序逻辑 PCTL 进行描述。利用概率模型验证器 PRISM 对WonGoo 系统的匿名性进行了自动验证。结果表明 WonGoo 的匿名性随着系统规模的增加而增加；但却随着攻击者观察到的源自同一个发送者的路径的增加而降低。另外，匿名路径越长，系统的匿名性越强。关键词匿名；点对点；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 ...