《匿名协议WonGoo的概率模型验证分析》由会员分享，可在线阅读，更多相关《匿名协议WonGoo的概率模型验证分析（9页珍藏版）》请在金锄头文库上搜索。
1、匿名协议WonGoo的概率模型验证分析陆天波，方滨兴，孙毓忠，郭丽（中国科学院计算技术研究所软件研究室 北京 100080）（中国科学院研究生院 北京 100039）（）摘 要Internet隐私的一个主要问题是缺乏匿名保护。近年来，人们已经针对这一问题做了很多工作。然而，如何利用已有的形式化方法分析匿名技术却是一个极具挑战的问题。对P2P匿名通信协议WonGoo进行了形式化分析。利用离散时间Markov链模型化节点和攻击者的行为。系统的匿名性质采用时序逻辑PCTL进行描述。利用概率模型验证器PRISM对WonGoo系统的匿名性进行了自动验证。结果表明WonGoo的匿名性随着系统规模的增加而增
2、加；但却随着攻击者观察到的源自同一个发送者的路径的增加而降低。另外，匿名路径越长，系统的匿名性越强。关键词匿名；点对点；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)(Gradu
3、ate 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
4、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
5、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.Key words anonymity,
6、Peer-to-Peer, WonGoo, Probabilistic Model Checking 1引言Internet的一个缺陷是不提供匿名保护，攻击者可以根据通信流之间的关系对发送者和接收者进行追踪。随着Internet的快速发展并被人们广为接受，以及搜索引擎和数据挖掘等技术的发展，人们已经开始关注Internet上的隐私和匿名。隐私不仅意味着信息的机密性，而且意味着信息发布者身份的机密性。匿名技术是Internet上保护用户隐私的一种有效手段，它通过一定的方法将通信流中的通信关系加以隐藏，使攻击者无法获知双方的通信关系或通信的一方。用户在通信过程中，通过隐藏自己的IP地址来保护自己的
7、隐私。例如，用户访问了某个网站，但是由于用户使用了匿名技术，使得该访问活动无法与用户身份信息（指IP地址）关联起来，这在一定程度上保护了用户的隐私。加密技术可以保护通信的内容，但是攻击者可以通过通信流分析(Traffic analysis)手段观察出谁和谁在通信，通信的时间以及通信流的多少等。因此，加密技术并不能保证通信的安全，尤其是在一个大的开放的环境中，保护通信者的身份就显得更加困难。本文中通信者的身份是指其IP地址，因此发送者是指发送者的IP地址，同样，接收者是指接收者的IP地址。我们所提出的WonGoo协议1是一个综合了Mix2和Crowds3的优点的可扩展点对点协议，提供三种形式的匿
8、名保护：发送方匿名（sender anonymity），即消息无法被关联到其发送者；接收方匿名（receiver anonymity），即消息无法被关联到其接收者；关系匿名（relationship anonymity），即消息的发送方和接收方是不可关联的（unlinkability）4。WonGoo克服了Mix效率低和Crowds抗攻击性差的缺点，通过分层加密和随机转发取得了强匿名和高效率。我们在文献1中分析了WonGoo的效率和匿名性介于Crowds 和Mix之间，是Crowds和Mix的折中。模型验证（Model Checking）技术是安全协议形式化分析的一项重要技术，它最早应用于硬件
9、的性能验证中。随着信息安全技术的不断发展，被逐渐应用于安全协议的形式化分析中。本文利用概率模型验证（Probabilistic Model Checking）技术分析了WonGoo系统的匿名性。我们把WonGoo系统形式化为一个离散时间Markov链（discrete-time Markov chains，DTMCs）模型，利用时序逻辑PCTL（Probabilistic Computational Tree Logic）5来描述WonGoo系统的匿名性质，并用概率模型验证器PRISM6进行验证。我们所考虑的问题是攻击者是否能够确定谁是一条匿名路径的发起者。我们假定攻击者可以观察部分网络通信流
10、，可以运行自己的WonGoo节点，可以控制其他的部分WonGoo节点。但是，攻击者不能破坏系统所采用的加密技术。2概率模型验证技术模型验证是一种验证有限状态系统的自动化分析技术。系统被模型化为一个状态转化图，系统的性质用时序逻辑描述。它通过一个有效的搜索过程来验证状态转化图是否满足某种性质。我们可以把模型验证抽象的描述为：给定一个模型M和逻辑描述的性质P，检查MP，即在模型M中性质P是否成立。模型验证的最大优点在于验证过程是全自动化的，并且如果一个性质不满足，它能给出反例说明这个性质不满足的理由。概率模型验证是模型验证技术的扩充，主要用于自动验证具有随机行为的系统中某些事件发生的概率。例如在系
11、统运行过程中验证事件“停机的概率不超过0.1”和“视频帧在5毫秒内到达的概率不低于0.9”等。概率模型验证中系统的形式化模型被赋予了概率信息，典型的情况是模型的每一个状态转化都标记有一个概率，用于说明状态转化的可能性。我们在本文中用到的模型是离散时间Markov链（DTMCs），其他两个常用的模型是连续时间Markov链（continuous-time Markov chains，CTMCs）和Markov决策过程（Markov decision processes，MDPs）。2.1离散时间Markov链（DTMCs）一个带标记函数的离散时间Markov链D是一个四元组 ，其中l 是一个有限
12、状态的集合；l 是初始状态；l 是一个转移概率矩阵，满足 ，对任意的；l 是一个标记函数，表示原子命题在状态s成立，其中AP是一个原子命题集合。转移概率矩阵的元素给出了从状态到状态的转移概率。系统的一次执行可用一条通过DTMCs的路径表示。本文中WonGoo系统的一次执行是指一条WonGoo路径的建立过程。一条通过DTMCs的路径是一个有穷（或者无穷）的状态序列，其中对任意的，有。我们把始于状态的路径的集合记为。2.2 DTMCs上的PCTL模型验证PCTL是对时序逻辑CTL（Computational Tree Logic）7的扩充和发展。它在CTL基础之上增加了概率算子，其中，。PCTL的
13、语法如下：其中是原子命题，是一个整数，是一个状态公式，是一个路径公式。概率算子的意思是，如果一条路径源于状态且满足路径公式的概率满足条件，则认为公式在状态是满足的。可以表示成下列公式： 其中。文献8对这一概率的计算过程进行了讨论。PRISM支持三种类型的路径公式：，和。路径满足路径公式，记为。下面给出PCTL在DTMCs上的语义描述。对于一条路径： （的第二个状态满足公式） （的前个状态中的某个满足，同时该状态以前的所有状态都满足） 对于一个状态: for all 对于公式来说，常用的形式是。如果一个状态s满足性质，则从状态到达满足公式的状态的概率满足条件。2.3 PRISM模型验证器PRIS
14、M6是由英国伯明翰大学开发的一个概率模型验证器。它支持三种模型，DTMCs，CTMCs和MDPs。在PRISM中，系统的行为用PRISM语言进行描述。一个系统被构建成几个模块，这些模块之间利用标准的进程代数运算进行交互。一个模块包括一些变量，用于表示系统的状态。系统的行为用一些监视命令（guarded command）表示。监视命令的格式如下： - ;其中，guard是系统变量上的断言，command描述状态转移，其转移的条件是guard为真。如果状态转移是不确定的，则command的形式为： : + + : PRISM根据对系统的描述进行建模并确定可达状态的集合。待验证的系统性质用时序逻辑P
15、CTL或CTL进行描述。对于本文用到的DTMCs来说，我们是用PCTL进行描述的。3 WonGoo协议设Alice与Bob进行通信，Alice首先选择一些WonGoo节点，我们称之为固定接收点。固定接收点的功能与Chaum描述的Mix节点的功能相似。Alice利用这些固定接收点的公钥对要发送的消息进行分层加密，构造出WonGoo数据包，然后以概率转发给一个随机选定的节点，称为概率接收点，以概率转发给下一个固定接收点。随后的每个节点（包括固定接收点和概率接收点）都进行类似的操作。当WonGoo数据包到达接收者Bob以后，就形成了一条WonGoo路径。随后的所有消息以及从Bob返回到Alice的消息都沿着这条路径进行传递。我们在文献1中分析了攻击者不能分辨出一条路径上的固定接收点和概率接收点。在一个大的点对点匿名通信系统中，由于节点只拥有局部的拓扑信息，因此，在进行下一跳选择时，可能会选择到已经在路径上出现过的节点，即节点可能会在路径上重复出现。为了提高系统的匿名性，必须尽量减少重复节点出现的概率。WonGoo在路径构造过程中，由发送者Alice确定的固定节点不允许重复。而且，每一个节点在进行概率转发时，所选择的下一跳节点不能与该节点本身以及上一跳
