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

匿名协议WonGoo的概率模型验证分析摘 要Internet隐私的一个主要问题是缺乏匿名保护。近年来，人们已经针对这一问题做了很多工作。然而，如何利用已有的形式化方法分析匿名技术却是一个极具挑战的问题。对P2P匿名通信协议WonGoo进行了形式化分析。利用离散时间Markov链模型化节点和攻击者的行为。系统的匿名性质采用时序逻辑PCTL进行描述。利用概率模型验证器PRISM对WonGoo系统的匿名性进行了自动验证。结果表明WonGoo的匿名性随着系统规模的增加而增加；但却随着攻击者观察到的源自同一个发送者的路径的增加而降低。另外，匿名路径越长，系统的匿名性越强。关键词匿名；点对点；WonGoo；概率模型验证Analysis of Anonymity Protocol WonGoo with Probabilistic Model CheckingAbtract 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 path length.Key words anonymity, Peer-to-Peer, WonGoo, Probabilistic Model Checking 1引言Internet的一个缺陷是不提供匿名保护，攻击者可以根据通信流之间的关系对发送者和接收者进行追踪。随着Internet的快速发展并被人们广为接受，以及搜索引擎和数据挖掘等技术的发展，人们已经开始关注Internet上的隐私和匿名。隐私不仅意味着信息的机密性，而且意味着信息发布者身份的机密性。匿名技术是Internet上保护用户隐私的一种有效手段，它通过一定的方法将通信流中的通信关系加以隐藏，使攻击者无法获知双方的通信关系或通信的一方。用户在通信过程中，通过隐藏自己的IP地址来保护自己的隐私。例如，用户访问了某个网站，但是由于用户使用了匿名技术，使得该访问活动无法与用户身份信息（指IP地址）关联起来，这在一定程度上保护了用户的隐私。加密技术可以保护通信的内容，但是攻击者可以通过通信流分析(Traffic analysis)手段观察出谁和谁在通信，通信的时间以及通信流的多少等。因此，加密技术并不能保证通信的安全，尤其是在一个大的开放的环境中，保护通信者的身份就显得更加困难。本文中通信者的身份是指其IP地址，因此发送者是指发送者的IP地址，同样，接收者是指接收者的IP地址。我们所提出的WonGoo协议1是一个综合了Mix2和Crowds3的优点的可扩展点对点协议，提供三种形式的匿名保护：发送方匿名（sender anonymity），即消息无法被关联到其发送者；接收方匿名（receiver anonymity），即消息无法被关联到其接收者；关系匿名（relationship anonymity），即消息的发送方和接收方是不可关联的（unlinkability）4。WonGoo克服了Mix效率低和Crowds抗攻击性差的缺点，通过分层加密和随机转发取得了强匿名和高效率。我们在文献1中分析了WonGoo的效率和匿名性介于Crowds 和Mix之间，是Crowds和Mix的折中。模型验证（Model Checking）技术是安全协议形式化分析的一项重要技术，它最早应用于硬件的性能验证中。随着信息安全技术的不断发展，被逐渐应用于安全协议的形式化分析中。本文利用概率模型验证（Probabilistic Model Checking）技术分析了WonGoo系统的匿名性。我们把WonGoo系统形式化为一个离散时间Markov链（discrete-time Markov chains，DTMCs）模型，利用时序逻辑PCTL（Probabilistic Computational Tree Logic）5来描述WonGoo系统的匿名性质，并用概率模型验证器PRISM6进行验证。我们所考虑的问题是攻击者是否能够确定谁是一条匿名路径的发起者。我们假定攻击者可以观察部分网络通信流，可以运行自己的WonGoo节点，可以控制其他的部分WonGoo节点。但是，攻击者不能破坏系统所采用的加密技术。2概率模型验证技术模型验证是一种验证有限状态系统的自动化分析技术。系统被模型化为一个状态转化图，系统的性质用时序逻辑描述。它通过一个有效的搜索过程来验证状态转化图是否满足某种性质。我们可以把模型验证抽象的描述为：给定一个模型M和逻辑描述的性质P，检查MP，即在模型M中性质P是否成立。模型验证的最大优点在于验证过程是全自动化的，并且如果一个性质不满足，它能给出反例说明这个性质不满足的理由。概率模型验证是模型验证技术的扩充，主要用于自动验证具有随机行为的系统中某些事件发生的概率。例如在系统运行过程中验证事件“停机的概率不超过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 是一个有限状态的集合；l 是初始状态；l 是一个转移概率矩阵，满足 ，对任意的；l 是一个标记函数，表示原子命题在状态s成立，其中AP是一个原子命题集合。转移概率矩阵的元素给出了从状态到状态的转移概率。系统的一次执行可用一条通过DTMCs的路径表示。本文中WonGoo系统的一次执行是指一条WonGoo路径的建立过程。一条通过DTMCs的路径是一个有穷（或者无穷）的状态序列，其中对任意的，有。我们把始于状态的路径的集合记为。2.2 DTMCs上的PCTL模型验证PCTL是对时序逻辑CTL（Computational Tree Logic）7的扩充和发展。它在CTL基础之上增加了概率算子，其中，。PCTL的语法如下：其中是原子命题，是一个整数，是一个状态公式，是一个路径公式。概率算子的意思是，如果一条路径源于状态且满足路径公式的概率满足条件，则认为公式在状态是满足的。可以表示成下列公式： 其中。文献8对这一概率的计算过程进行了讨论。PRISM支持三种类型的路径公式：，和。路径满足路径公式，记为。下面给出PCTL在DTMCs上的语义描述。对于一条路径： （的第二个状态满足公式） （的前个状态中的某个满足，同时该状态以前的所有状态都满足） 对于一个状态: for all 对于公式来说，常用的形式是。如果一个状态s满足性质，则从状态到达满足公式的状态的概率满足条件。2.3 PRISM模型验证器PRISM6是由英国伯明翰大学开发的一个概率模型验证器。它支持三种模型，DTMCs，CTMCs和MDPs。在PRISM中，系统的行为用PRISM语言进行描述。一个系统被构建成几个模块，这些模块之间利用标准的进程代数运算进行交互。一个模块包括一些变量，用于表示系统的状态。系统的行为用一些监视命令（guarded command）表示。监视命令的格式如下： <guard> -> <command>其中，guard是系统变量上的断言，command描述状态转移，其转移的条件是guard为真。如果状态转移是不确定的，则command的形式为： <prob> : <command> + ··· + <prob> : <command>PRISM根据对系统的描述进行建模并确定可达状态的集合。待验证的系统性质用时序逻辑PCTL或CTL进行描述。对于本文用到的DTMCs来说，我们是用PCTL进行描述的。3 WonGoo协议设Alice与Bob进行通信，Alice首先选择一些WonGoo节点，我们称之为固定接收点。固定接收点的功能与Chaum描述的Mix节点的功能相似。Alice利用这些固定接收点的公钥对要发送的消息进行分层加密，构造出WonGoo数据包，然后以概率转发给一个随机选定的节点，称为概率接收点，以概率转发给下一个固定接收点。随后的每个节点（包括固定接收点和概率接收点）都进行类似的操作。当WonGoo数据包到达接收者Bob以后，就形成了一条WonGoo路径。随后的所有消息以及从Bob返回到Alice的消息都沿着这条路径进行传递。我们在文献1中分析了攻击者不能分辨出一条路径上的固定接收点和概率接收点。在一个大的点对点匿名通信系统中，由于节点只拥有局部的拓扑信息，因此，在进行下一跳选择时，可能会选择到已经在路径上出现过的节点，即节点可能会在路径上重复出现。为了提高系统的匿名性，必须尽量减少重复节点出现的概率。WonGoo在路径构造过程中，由发送者Alice确定的固定节点不允许重复。而且，每一个节点在进行概率转发时，所选择的下一跳节点不能与该节点本身以及上一跳节点相同。为了使分析变得简单，本文假定节点可在WonGoo路径上的任何位置重复出现。因此，WonGoo系统的匿名性实际上比本文分析的要高。为了后面叙述方便，我们定义固定路径和变化路径两个概念。由一个固定接收点直接到达另一个固定接收点的一条路称为固定路径（发送者和接收者也被看成是固定接收点）。两个固定接收点之间依据概率转发所形成的路径称为变化路径。显然，当变化路径长度为1时，则成为固定路径。4 WonGoo的模型构造我们仅仅对WonGoo的路径建立过程进行模型验证，而对路径建立完成以后的通信没有进行模型验证，原因是路径一旦建立，那么路径上的每一个转发节点都是从固定的上一个节点接收消息，而且通信的内容是不会泄漏发送者的身份信息的。因此攻击者不会从随后的通信中获得更多的关于发送者的信息。我们的Markov链模型中的状态代表匿名路径建立过程中系统所处的状态。一个状态完全由模型中的状态变量所确定，见表1。表1 状态变量Table 1 State variablesrunCountNumber of paths constructed so far (<=TotalRuns).goodThe selected forwarder is honest.badThe selected forwarder is bad.lastSeenIdentity of the preceding forwarder on the path. observei Number of times corrupt members observed member i.newReady to construct another path.startBeginning of new path construction.runContinue path construction.deliverTerminate the path.recordLastRecord the identity of the preceding forwarder.badObserveHave a corrupt member record its observations.fixedNodeNumNumber of fixed WonGoo nodes in a path.FwLengthForward path length between two fixed WonGoo nodes.我们假定攻击者除了有能力运行自己的WonGoo节点之外，还能控制部分其他的节点。我们把攻击者自己的节点及被其控制的其他节点统称为泄密节点，也叫泄密者；把没有被攻击者控制的节点，即非泄密者，称为诚实的节点。诚实的节点不会为攻击者提供任何信息。假设个成员的WonGoo网络中有个泄密者，发送者Alice已经利用节点选择算法1选定了个固定接收点。我们所考虑的问题是攻击者是否能够确定一条路径的发送者是谁。对接收者的分析与对发送者的类似。如果发送者本身是一个泄密者，则对攻击者来说，系统已经被攻破。我们考虑由非泄密节点发起的一条路径。在这条路径上，泄密节点占据了一个位置。泄密者的目的是确定谁是该路径的发起者。由于我们采用了加密技术，因此通信的内容是不会暴露发起者的身份的。所以，攻击者有理由相信第一个泄密者的前驱节点比其他节点更像是发起者。这种假设是合理的，因为从攻击者来看第一个泄密者的前者最有可能是发起者。后面的叙述中假设WonGoo网络中诚实节点数为10。4.1 协议的开始我们要求每一次会话都是由同一个发送者(observe0)发起的。这是通过在协议开始时设置变量lastSeen的值为零来实现的。同时，我们还要设置分别用于表示固定节点数和变化路径长度的变量fixedNodeNum和FwLength的值。/ Set up a new protocol instance new & (runCount > 0) -> (runCount' = runCount-1) & new' = false & start' = true & fixedNodeNum' = MaxfixedNodeNum & FwLength' = MaxFwLength;/ Start the protocol start -> lastSeen'=0 & run'=true & deliver'=false & start'=false;4.2 转发节点的选择发送者随机的从个节点中选择第一个概率接收点。假定个节点被选中的概率是相等的。我们把转发节点的选择模型化为两次状态转移，一次确定所选择的转发节点是否是诚实的，另外一次确定转发节点的身份。随机选择的转发节点是恶意节点的概率为badC=C/N，是诚实节点的概率为goodC=1-badC。/ Good or bad WonGoo member (!good & !bad & !deliver & run) -> goodC: (good'=true) & (recordLast'=true) & (run'=false) +badC: bad'=true & badObserve'=true & run'=false;如果转发节点是诚实的，则它可能为N-C个诚实节点中的任意一个。转发者的身份记录在lastSeen变量中。记录转发者的身份是为了模拟以下行为：如果该转发节点的下一个节点是恶意节点，则该恶意节点可以记录下该转发节点的IP地址。/ Record the last WonGoo member who touched the message, all good members may appear with equal / probability recordLast & WonGooSize=10 ->0.1: (lastSeen'=0) & (recordLast'=false) & (run'=true) + 0.1: (lastSeen'=9) & (recordLast'=false) & (run'=true);WonGoo协议中，每一个节点（包括恶意节点）都必须确定下一跳。转发者以概率将数据转发给随机选定的概率接收点，以概率转发给已经选好的下一个固定接收点。/ Good members, forward to a random selected node with probability PF, else deliver to the next fixed node. (good & !deliver & run & FwLength > 0) -> PF: (good'=false) & (FwLength'=FwLength-1) + notPF: (good'=false) & (fixedNodeNum'=fixedNodeNum-1) & (FwLength'=MaxFwLength); 4.3 恶意节点的模型化显然，匿名路径上的节点是知道它前一跳的地址的。如果是恶意节点，则它将记录下其上一跳的IP地址。这是通过读取lastSeen变量的值并纪录在observei中而实现的。/ Bad members, remember from whom the message was received and terminate the protocol lastSeen=0 & badObserve -> (observe0' = observe0 + 1) & deliver'=true & run'=true & badObserve'=false; lastSeen=9 & badObserve -> (observe9' = observe9 + 1) & deliver'=true & run'=true & badObserve'=false;对每一次路径建立过程来说，计数器observei并不清零，而是进行累加。这使得攻击者可以将对源自同一个发起者的多条路径的观察信息进行累加。我们假定攻击者可以验证出两条路经是否源自同一个发送者。4.4 协议的结束当遇到攻击者时我们就结束路径建立过程，这是因为一旦碰到了恶意节点，则随后的建立过程不会提供更多的关于发送者的信息给攻击者，攻击者所能获知的就是上一跳的地址。这一点与Shmatikov9用PRISM分析Crowds协议时所采用的方法相同。但是如果在路径建立过程没有碰到恶意节点，Shmatikov的方法在理论上会产生死锁状态，原因是Shmatikov没有对匿名路径的长度进行限制。我们用fixedNodeNum表示固定接收点数，FwLength表示变化路径长度，而且我们认为接收者也是一个固定接收点。这样，如果在路径建立过程中没有碰到恶意节点，则当fixedNodeNum的值为零时，路径建立结束，避免了死锁。/ If all members in a path are honest, terminate the path set up when its length increases to the max length. (!good & !deliver & run & FwLength = 0) -> (fixedNodeNum' = fixedNodeNum-1) & (FwLength' = MaxFwLength); fixedNodeNum=0 -> deliver'=true;/ Terminate the protocol待添加的隐藏文字内容3 deliver & run -> done'=true & deliver'=false & run'=false & good'=false & bad'=false; / Start a new instance done -> new'=true & done'=false & run'=false;5 匿名性质的形式化与对Crowds的分析39类似，我们假定攻击者能够把源自同一个发送者的几条路经关联起来。在攻击者看来，如果某一个节点比其他节点更像是发送者，则他有理由认为该节点就是真正的发送者。我们要回答的问题就是攻击者猜测出发送者的概率有多大。我们将在表示WonGoo系统的Markov链上构造PCTL公式对这个问题进行讨论。我们用表示攻击者观察到WonGoo成员的次数。其意思是在由同一发送者发起的多条路径中，经过节点并且的下一跳是恶意节点的路径有条。用表示发送者被观察到的次数。这包括两种情况，一是恶意节点被选为第一个转发者；二是发送者本身被选为一个中转节点，其下一跳是一个恶意节点。我们采用Shmatikov在文献9中提出的方法来验证WonGoo成员。如果一个成员被观察到的次数比其他成员的都多，即，则我们认为该成员是发送者。为此，定义以下事件：，（发起者被观察到次数大于其他任何成员的）。于是我们要验证的概率为： （猜测到真正的发起者）。上述匿名性质用PCTL描述如下：/Detection P = ? true U (new & runCount = 0 & observe0 > observe1 & & observe0 > observe9)6 验证结果我们利用PRISM模型验证器对WonGoo系统的不同配置进行概率模型验证。表2描述了不同规模下的状态空间，其中，固定节点数fixedNodeNum=3，变化路径长度FwLength=3。从表中可知，与其他的模型验证一样，随着系统规模的增大，状态空间增长很快，这使得分析大规模WonGoo系统变得困难。如何解决模型验证中状态空间爆炸问题是该领域的一个难题。表2 状态空间Table 2 Size of state spaceWonGoo源自同一发送者的路径数（TotalRuns）345610 honest membersstates112,890524,0261,955,8526,232,410transitions308,7701,439,3065,391,23217,232,49015 honest membersstates332,9002,099,87610,460,61243,785,236transitions1,126,5957,130,77135,631,407149,556,43120 honest membersstates734,9605,860,62636,518,022189,355,322transitions2,964,72023,708,786148,121,382769,919,48225 honest membersstates1,373,82013,244,27699,077,582612,790,418transitions6,434,77062,186,726466,274,6572,890,100,243表3计算了不同路径数下的验证概率，从中可以看出以下两点：l 随着攻击者所观察到的源自同一发送者的路径的增多，系统的匿名性降低。因此，在WonGoo中，一次会话（发送者和接收者之间的一次通信）只通过一条路径完成，而不像Peekabooty所建议的那样，一次会话通过多条路径完成，既所谓的多路径路由。l 在恶意节点比例（badC=0.167）不变时，验证概率随着系统规模的增大而减小。这说明系统的匿名性随着规模的增加而增加。 表3 不同路径数下的验证概率（PF=0.3, fixedNodeNum=3, FwLength=3）。 Table 3 Probabilities of detecting the initiator increase with increasing TotalRuns WonGoo源自同一发送者的路径数（TotalRuns）345610 honest, 1 corruptPr(%)17.2917.8618.5119.1215 honest, 2 corruptPr(%)17.4718.0019.3219.8910 honest, 2 corruptPr(%)21.8524.2528.0932.2115 honest, 3 corruptPr(%)19.9322.0725.8728.4320 honest, 4 corruptPr(%)18.9620.9723.5125.3725 honest, 5 corruptPr(%)18.3919.9822.8324.78Yong Guan等人10研究指出，通常情况下，匿名性随着匿名路径长度的增加而增加。WonGoo正是在保证足够匿名的前提下，通过延长匿名路径，从而进一步提高了系统的匿名性。表4和表5分别描述了WonGoo的匿名性随路径长度的变化关系。表4通过调整转发概率Pf的大小来调整路径长度。表5通过调整固定节点数fixedNodeNum来调整路径长度。可以看出，随着匿名路径的增长，验证概率降低，从而系统的匿名性得到了提高。表4 不同转发概率下的验证概率（fixedNodeNum=4, FwLength=5, Totalrun=3）Table 4 Probabilities of detecting the initiator decrease with increasing forward probabilitiesWonGooPF 0.10.20.30.40.50.60.70.80.910 honest, 1 corruptPr(%)17.9417.1016.0614.6712.7910.397.735.403.8715 honest, 2 corruptPr(%)17.7216.5415.2013.6311.799.747.736.094.9710 honest, 2 corruptPr(%)21.8420.5819.2617.8816.4415.0113.6612.4411.2815 honest, 3 corruptPr(%)19.7818.4617.0815.6614.2012.7711.4910.419.4620 honest, 4 corruptPr(%)18.7517.4016.0014.5513.0911.6810.439.428.5725 honest, 5 corruptPr(%)18.1516.7915.3813.9212.4511.059.838.858.07表5 不同固定节点数下的验证概率（PF=0.3, FwLength=5, Totalrun=3）Table 5 Probabilities of detecting the initiator decrease with increasing fixed node numbersWonGoofixedNodeNum2468101210 honest, 1 corruptPr(%)20.6216.0612.8010.709.468.7815 honest, 2 corruptPr(%)22.1815.2011.439.538.648.2610 honest, 2 corruptPr(%)27.7019.2616.2115.3215.1815.1615 honest, 3 corruptPr(%)26.0017.0813.8212.7612.4912.4720 honest, 4 corruptPr(%)25.1316.0012.6511.5211.1811.1225 honest, 5 corruptPr(%)24.6215.3811.9810.8110.4410.357 结论形式化方法是对安全协议进行验证的一种有力工具。如何利用已有的形式化方法对匿名协议进行分析是一个极具挑战的问题。概率模型验证是一种十分有效的协议形式化分析工具。本文利用PRISM模型验证器对匿名通信协议WonGoo进行了分析。WonGoo通过随机转发和分层加密建立匿名通信路径。因此，我们把WonGoo的路径建立过程模型化为一个离散时间Markov链，并在攻击者可以识别出两条链路是否源自同一发送者的假设下，分析了攻击者识别出一条匿名路径的发起者的概率。WonGoo协议的分析表明了利用概率模型验证技术分析安全协议的可行性。References:1 T. Lu, B. Fang, Y. Sun, X. Cheng. WonGoo: A Peer-to-Peer Protocol for Anonymous Communication, In Proceedings of the 2004 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA04), June 2004: 1102-1106.2 D. Chaum. Untraceable electronic mail, return addresses and digital pseudonyms. Communications of the ACM, February 1981, 24(2): 84-88. 3 M. K. Reiter and A. D. Rubin. Crowds: Anonymity for Web Transactions. ACM Transactions on Information and System Security, November 1998, 1(1): 66-92.4 A. Pfitzmann and M. Köhntopp. Anonymity, Unobservability, and Pseudonymity A Proposal for Terminology, Draft v0.14. Anon_Terminology_v0.14.pdf, May 2003.5 H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 1994, 6(5): 512-535. 6 http:/www.cs.bham.ac.uk/dxp/prism7 E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. on Programming Languages and Systems, 1986, 8(2): 244-263.8 D.Parker. Implementation of Symbolic Model Checking for Probabilistic Systems. Ph.D. Thesis, University of Birmingham, August 2002.9 V. Shmatikov. Probabilistic Analysis of Anonymity. In Proc. 15th IEEE Computer Security Foundations Workshop (CSFW'02), June 2002: 119-128.10 Y. Guan, X. Fu, R. Bettati, and W. Zhao, "An Optimal Strategy for Anonymous Communication Protocols," in Proceedings of the 22nd IEEE International Conference on Distributed Computing Systems (ICDCS 2002), July 2002: 257-266.