Formal Analysis of Anonymity Based on Strand Space Model

摘要：

Anonymous communication protocols can be used in ubiquitous environments to preserve the identity of users. To verify the correctness of the protocol, a formal framework for the analysis of anonymity property of anonymous communication protocols in terms of strand space model was proposed. The key ingredient is the notions of equivalent bundles and extremum pair, which are used to define anonymity. Then we illustrate our approach by proving sender anonymity and unlinkability for two well-known anonymous communication protocols, Crowds and Onion Routing and show how the framework is capable of verifying the correctness of protocols or capturing the flaws. The result shows that sender anonymity will fail in Crowds if there exist a global attacker and relation anonymity will fail in Onion Routing if the attacker knows the onion router’s private key. Furthermore, to analyze the particular version of Onion Routing proposed in 1, it can also find the flaw in the protocol.

关键词： Strand Space Model equivalent bundles extremum pair Anonymity Formal Methods Ubiquitous Computing

作者: Lu Zhang Junzhou Luo

作者单位: School of Computer Science and Engineering,Southeast University,Nanjing,P.R.China

会议类型: 国际会议

会议名称: The First IEEE International Conference on Ubi-Media Coputing and Workshops(第一届泛媒体处理国际会议)

会议地点: 兰州

会议语种:英文

在线出版日期: 2008-07-15（万方平台首次上网日期，不代表论文的发表时间）