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

Internet隐私的一个主要问题是缺乏匿名保护．近年来，人们已经针对这一问题做了很多工作．然而．如何利用已有的形式化方法分析匿名技术却是一个极具挑战的问题．对P2P匿名通信协议WonGoo进行了形式化分析．利用离散时问Markov链模型化节点和攻击者的行为．系统的匿名性质采用时序逻辑PCTI，进行描述．利用概率模型验证器PRISM对WonGoo系统的匿名性进行了自动验证．结果表明WonGoo的匿名性随着系统规模的增加而增加；但却随着攻击者观察到的源自同一个发送者的路径的增加而降低．另外，匿名路径越长，系统的匿名性越强．

Analysis of Anonymity Protocol WonGoo with Probabilistic Model Checking

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-topeer anonymous communication protocol WonGoo. The behavior of group members and the adversary is modeled as a discretetime 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.