基于概率Applied Pi的匿名度分析.doc

上海交通大学硕士学位论文基于概率Applied Pi的匿名度分析姓名：谢思敏申请学位级别：硕士专业：指导教师：傅育熙20090201上海交通大学工学硕士学位论文 摘要 第 II 页 匿名度。最后文章分析了经典的密码学家就餐问题，用概率applied pi对其建模，计算匿名度并对实验结果进行对比和分析，验证了本文的基本思想。 关键词：概率进程演算, 匿名度, 互模拟, 匿名协议, 密码学家就餐问题 上海交通大学工学硕士学位论文 ABSTRACT 第 III 页 Measuring Anonymous System with Probabilistic Applied Pi Calculus ABSTRACT As the development and wildly use of electronic business, people began to pay attention to the personal information and privacy involved in all kinds of internet activities. However, nowadays nearly all transactions, information exchange, and clients actions and so on, can be observed and recorded in network. In this way, it s very possible that the private data belonging to client will be not properly used and analyzed, leading to all kinds of information leak. At present, there are many formalized ways to study anonymity, we can divide them into two classes: Process calculus combined with bisimulation, Logic and Model checking. Based on these ways, many researchers have shown results for studying the anonymity of some anonymous communication systems. However，increasing people realize that something always happened with probability in the real network. So we neglected this probability to analyze anonymity while modeling network with traditional formal ways. Obviously it cannot satisfy the practical needs, then some researchers proposed some probabilistic anonymous communication systems. They take probability in the realistic network into consideration, and introduce probability activity into anonymous communication systems. This is more close to the real network. As probabilistic anonymous systems are proposed in the literature, it cannot say whether a system is anonymous absolutely. To analyze such kind of anonymous systems, traditional process calculus cannot work. First, the calculus is not expressive enough to model the system with probabilities, so we should use probabilistic process calculi. Second, to get a degree of anonymity, bisimulation is not enough because it only compares two processes and give an answer“yes” or “no” to tell if they operate similarly, so we need another relation which is more refined than bisimilarity. we chose the probabilistic applied pi calculus (PAPi forshort), which extends the 上海交通大学工学硕士学位论文 ABSTRACT 第 IV 页 applied pi calculus with introducing non-dterministic and probabilistic choic operators. This paper studied the anonymity in the model of Probabilistic Applied Pi (PAPi for short). Main contributions of this paper can be summarized as follows: First, a metric was defined on PAPi Processes to measure the similarity between processes. This metric was then shown to be well-defined since it turns out to be 0 when two processes are weakly bisimilar. Upon metric, the formal definition of anonymity degree was given. Finally, as an illustrating example, the anonymity of probabilistic Dining Cryptographer Problem (DCP for short) was analyzed in our framework. Key Words: probabilistic process calculus, degree of anonymity, bisimulation, anonymous system, DCP 上海交通大学 学位论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究工作所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本文的研究做出重要贡献的个人和集体，均已在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。 学位论文作者签名： 日期： 年 月 日 上海交通大学 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅。本人授权上海交通大学可以将本学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。 保密，在 年解密后适用本授权书。 本学位论文属于 不保密。 （请在以上方框内打“”） 学位论文作者签名： 指导教师签名： 日期： 年 月 日 日期： 上海交通大学工学硕士学位论文 第一章 绪论 第 1 页 第一章 绪论 1.1研究背景与意义随着计算机科学技术的发展和个人电脑的普及，整个世界通过计算机网络连接在一起，人们的生活也越来越离不开网络。在网络上大家可以进行各项活动，如联系好友，收发信件，浏览新闻，商业活动等。最近几年随着电子商务的兴起与广泛应用，大家也开始关注在进行各种网络活动中涉及到的个人信息隐私问题。然而，在当今的网络世界中，几乎所有的交易、信息交换、用户的行为等都可能被观测到，并且被记录下来。这样很有可能造成原本属于用户的隐私性的数据被不恰当的进行使用和分析，造成各种信息的泄露，于是越来越多的人开始关注和研究网络行为的匿名性。 最近几年里也有不少人提出了实现各种匿名网络通信的系统，如FOO电子投票协议1，不可跟踪电子现金协议2等等。研究匿名性有很多种方法，因为形式化方法分析有助于更准确的描述安全协议的行为和定义匿名性，所以用形式化的方法来分析安全协议的匿名性成了最近几年比较热门的研究课题之一，目前国外在该领域比较活跃的主要是欧美的一些国家，国内对安全协议的形式化研究也引起了重视。安全协议形式化分析技术可使协议设计者通过系统分析将注意力集中于接口、系统环境的假设、在不同条件下系统的状态、条件不满足时出现的情况以及系统不变的属性，并通过系统验证，提供协议必要的安全保证3。因此用形式化的方法来研究匿名通信系统的匿名属性在准确性方面有着明显的优势，而之前很多研究者在研究过程中也给匿名性提供了各种各样更加精确的定义。其中Pfitzmannd在4里，提出了三种匿名属性：发送者匿名性，接收者匿名性，发送者与接收者的不可连接性。在分析安全协议的匿名性时可以就这三种属性进行分析。 进程演算(process calculus)作为形式化方法的一种为进程之间的通信和交互提供了高层的描述。它是一种强有力的并发系统建模工具。基于进程演算的安全协议分析和验证，既可以利用进程演算的操作语义采用状态搜索的方法，又可以借鉴进程演算作为代数模型的等价系统采用测试等价的理论与方法，还可以使用进程演算作为抽象程序设计语言的程序分析方法。而且进程演算用于安全协议验证已有十多年的历史，最早用于安全协议分析的进程演算是CSP（Communicating Sequential Processes）5，随后，CCS（Calculus of Communication System）、pi上海交通大学工学硕士学位论文 第一章 绪论 第 2 页 演算等都被用于安全协议和安全系统的分析。Abadi等人对pi演算6进行了扩充，增加了加密、解密等操作原语，形成了spi演算7。随后Abadi又在pi的基础上进行扩展增加了传值、函数原语和等式系统理论等提出了applied pi8，而且它已经用于对安全协议的建模Just Fast Keying9和验证10。这个演算无需为特定的密码系统操作构造新的原语，因此有很好的通用性，也就能表达和分析相当复杂的协议（混合了多个密码学原语的协议，如加密、解密、Hash函数、签名等操作原语）。由此可见，用进程演算的方法来研究匿名性也有着不短的历史，并且在分析某些具体的通信系统时取得了不错的成果。 而前面所提到的FOO电子投票协议1，不可跟踪电子现金协议2等它们都是非概率的匿名系统，即不考虑动作的随机性，因此可以用传统的形式化方法来分析其匿名性，比如用pi演算和弱互模拟来分析MUTE匿名文件共享系统11，用类pi演算来验证电子支付协议的认证性和匿名性12，在新的安全模型下定义和分析匿名性13。但是现实的世界当中某些事件的发生是具备一定的随机性的，往往一个系统中某些动作是以一定的概率发生的。而我们用传统的方法对它们建模时却忽略掉了随机性，显然是不符合现实世界的规律的。于是又有一部分学者开始考虑在原来的匿名系统中增加了概率，认为某些动作是以一定的概率发生的，如Crowds14和DCP(密码学家就餐问题)15的变种。 加入了概率后，用传统的进程演算来分析其匿名性不再可行。首先传统的演算表达能力不够强，无法对带概率的通信协议中的一些概率动作进行建模。其次，为了得到匿名度，仅有互模拟是不够的，因为，互模拟只能对他们是否相似简单地回答“是”或者“否”，所以我们需要使用带概率的形式化方法以及一种比互模拟更加丰富的关系来分析这种匿名系统。 1.2国内外研究现状目前，国内外形式化研究安全协议主要有基于知识与信念推理的模态逻辑方法，基于定理证明的方法和基于进程演算的方法三种。其中，进程演算对于协议的描述几乎接近协议的本身含义，可以很精确地刻画协议的运行过程。使用进程演算对安全协议分析和验证时，协议的每一个主体都被建模为一个单独的进程，这些子进程并发运行，并使用进程之间的共享通道进行同步通信，这样得到的并发系统将作为安全协议的基本模型。利用进程演算对安全协议进行分析和验证时，既借鉴了进程演算作为代数模型的基本验证理论与方法，又使用了进程演算作为抽象程序设计语言的程序分析方法。因此，基于进程演算的安全协议验证技术可上海交通大学工学硕士学位论文 第一章 绪论 第 3 页 分为模型检测技术、互模拟验证技术和程序分析技术三种。 而目前已经完成的研究工作可以分为：非概率框架下使用逻辑再结合model checking验证、在非概率框架下用进程演算建模再结合互模拟验证、对带概率的匿名协议使用逻辑再结合model checking验证和香农的熵理论这几个方法。 1.2.1非概率框架下使用逻辑再结合model checking验证 这种方法是使用逻辑来描述匿名性然后用model checking进行验证。目前已经实现的工作有： Syverson和Halpern等人在16里使用模型逻辑定义了各种各样的匿名性。在17里使用工具集CRL自动验证FOO协议（电子投票协议）和DCP（密码学家就餐问题）。 另外Garcia也提出用认知逻辑（Epistemic Logic）来刻画和分析协议的匿名性，并给出了一系列不同匿名性质在认知逻辑（Epistemic Logic）中的形式化刻画18。这种研究方法能清楚准确的刻画出协议所需要的满足的性质。 然而这几种研究方法都必须建模成攻击者模型，在攻击者复杂的情况下是很困难而且容易出错的。 1.2.2在非概率框架下用进程演算建模再结合互模拟验证 用进程演算表达的匿名性协议可以用互模拟来描述其匿名性。其中有： Schneider和Sidiropoulos在使用CSP（Communicating Sequential Processes）对匿名性进行分析中使用了一个偏序关系来表示某个进程是否满足其规范说明（specification）。文章19对于如何分析给定协议的匿名性给出了如下方法：首先应描述满足匿名性定义的协议的规范说明（specification），然后将协议使用CSP描述出来，最后验证两者是否满足上述偏序关系，即能验证给定协议是否满足相关匿名性质。 另外还有很多，比如：11通过pi演算和弱互模拟来分析MUTE匿名文件共享系统，20和21都是使用applied pi演算和labelled bisimulation分析安全协议的。 通过进程演算我们不需要给出攻击者模型，因为进程已经可以表达攻击者的攻击能力，但是它的缺点是，除非我们将进程限制到有限个状态，否则将很难对互模拟进行验证。 上海交通大学工学硕士学位论文 第一章 绪论 第 4 页 1.2.3对带概率的匿名协议使用逻辑再结合model checking验证 22使用PCTL（Probabilistic Computation Tree Logic）对Crowds系统建模，然后运用PRISM(Probabilistic model checker)自动验证匿名性。PCTL用于对概率有限状态空间的带概率的属性进行推理。它可以表达“在任意进程的调度下，事件E发生的概率至少为p”这种形式的属性。用此建模后，再利用PRISM验证。PRISM是一个用Markov chain描述的系统23，它能计算到达每一个可达状态的概率。 此外，16也用概率的方式给出了匿名性的定义。并且对一些概率匿名系统的匿名性进行分析。 1.2.4香农的熵理论 24运用香农的熵的定义对匿名性给出了一个测量系统,它也可以对带有概率的匿名性协议进行分析。然而，这种方法要求攻击者的能力是有限制的，另外由于比较复杂，通常这种分析很难自动化。 1.3研究内容既然传统的进程演算不再可行，所以我们需要使用概率的进程演算，以及一种比互模拟更加丰富的关系。这篇文章里我们选择了概率applied pi演算。它是由Jean Goubault-Larrecq等人2007年在25中提出，它与applied pi类似，不仅有传值、函数原语和等式系统理论，还增加了概率加和不确定加操作，很适合用来分析安全协议，特别是带概率的安全协议。而且目前用PAPi的形式化验证技术已经应用到很多的领域，但是还从未有用PAPi对匿名性进行分析的研究工作和结果。因此这篇文章主要是用PAPi对概率匿名通信系统进行研究，我们的主要研究工作集中于： 1) 我们选择了概率applied pi演算（简写为PAPi）25，它在applied pi的基础上增加了概率选择和不确定选择操作。并且我们在一对PAPi进程上定义metric，它是一个0到1之间的值，可以对两个进程的相似度进行量化，当两个进程弱互模拟时等于0，当两个进程完全不相似时metric等于1，并且证明弱互模拟与metric之间的对应关系。 2) 根据metric，我们由强到弱定义了三个匿名度：beyond suspicion，probable innocence和possible innocence，可以根据metric的值来计算系统中的匿名概率，上海交通大学工学硕士学位论文 第一章 绪论 第 5 页 从而得到匿名度。 3) 我们用PAPi对经典的DCP匿名系统建模，分为两种情况讨论，这里考虑的是四个密码学家就餐问题，并且计算其匿名度，并对结果进行简单的对比与分析。 1.4论文的结构接下来，文章是这样组织的：第二章介绍了我们所需要的有关PAPi的基础知识；第三章定义metric，并证明了它与互模拟的关系，还给出了如何计算metric的方法；第四节给出了匿名度的形式化定义；第五节我们分析实例DCP。最后一节总结了我们所做的工作。 上海交通大学工学硕士学位论文 第二章 PAPi 第 6 页 第二章 PAPi 2001年，Abadi等学者参照了演算26到applied 演算的扩展，将pi演算扩展成applied pi演算8。applied pi 演算继承了pi演算的通信和并发构造，增加了函数和等式原语。消息不仅仅是原子名，还有通过名和函数构成的值。这个演算能很容易地处理标准数据类型，而且可以更加清楚的形式化描述安全协议。譬如，用新名表示新的通道、随机值和密钥，用函数表示密码学原语。相对于Spi演算，这个演算不需要为特定的密码系统操作构造新的原语，从而有很好的通用性，也就能表达和分析相当复杂的协议（混合了多个密码学原语的协议，如加密、解密、Hash函数、签名等操作原语）。applied pi演算8提出了观察等价和静态等价两种等价关系，使之更好的描述和验证具体的安全协议。 因为越来越多的用户希望自己在网络上的行为是匿名的，所以很多的网络通信协议也越来越注重匿名性，尤其是电子商务协议。而我们用传统的进程演算比如applied pi来分析匿名系统，我们只能对它是否满足匿名性简单的回答yes或者no，然而现实的网络世界是千变万化的，在这种不确定的网络中，这种简单的回答显然是令人不满意的。于是最近的研究热点就集中在模拟那些带有定量信息的系统上，这些系统都会涉及到一些定量的信息，网络中的某些行为却是以一定的概率发生的，比如Crowds系统和DCP问题等。这些协议无法用传统的进程演算来建模，于是我们选择了PAPi。 Jean Goubault-Larrecq在applied pi的基础上提出了概率applied pi演算（PAPi） 25。它继承applied pi的优点，同时增加了概率操作，从而可以对带概率的安全协议进行分析。 本章当中，我们介绍下我们研究过程中将要用的有关PAPi的一些定义，具体可以参考25。 2.1语法PAPi的语义和applied pi演算相似，在applied pi定义的普通进程（plain process）上增加了概率加（）和不确定加（+）。给定一个,其中函数符号表示函数名，表示参数的数目。项(term),普通进程(plain process),扩展进程(extend process)由下面语法定义： 上海交通大学工学硕士学位论文 第二章 PAPi 第 7 页 项： , , , 普通进程： ,0 . . | ! . 扩展进程： , . . |/ 在项中，,是名；,是变量；,则表示满足,的函数。 对普通进程来说，0表示什么也不做；.在通道上输出项，然后执行进程；而.则在通道上先接收一个项，然后将输入代替中的x执行进程；不确定性选择表示接下来执行的可能是或者；而概率加表示以c的概率执行、以111的概率执行；|表示和并发执行；!表示无限个并行执行； .限制P中的自由名。 扩展进程在普通进程中加入主动替换/，所以|/类似于 | （严格上来说 .|/与它等价）。直观上我们可以将主动替换/理解为协议中的每一个参与者都知道的一些静态信息，或者是环境得到了项M但是却无法获得M中的一些原子名。并行替换/|/可以写为/,/。如果我们用表示某个替换，那么将替换应用到变量x上海交通大学工学硕士学位论文 第二章 PAPi 第 8 页 可以写成，将替换应用到项T中的自由变量可以写成。 2.2其他的概念限制和输入操作划定了变量和名的作用范围。通常我们用和表示进程A的自由变量和自由名，和表示进程的受限名和受限变量。 如果一个进程中的每个变量要么是受限要么是被定义成一个主动替换，那么我们说这个进程是封闭的，并用表示所有封闭进程的集合，用 表示不重复的受限序列 . . 。 直观上，我们可以讲扩展进程理解为一个普通进程加了上下文来解释它们的变量。通常一个上下文（evaluation context）是一个带有一个空洞的表达式（扩展进程）。从语法上 _ 的定义如下： _ . _ . _ | _ _ | 其中A是一个扩展进程，如果是封闭的，那么上下文 _ 封闭了A。 帧(frame)是一个由0进程和主动替换建立起来的扩展进程。一个扩展进程A的帧可以写成如下的形式： ./ ，其中。如果是空集，那么 0；如果,而且,，那么 ./ | / | | /。由此可见，我们可以将帧看作是进程A泄露给环境的一些静态的知识，每一个扩展进程都对应着一个帧。我们用来表示帧的域，它是一个出现在的主动替换中但是又没有被限制的变量的集合。我们说一个扩展进程的域就是指它的帧的域。 在扩展进程的定义时我们用到，它表示两个项之间的等价。对每一个，我们定义一个等式理论系统E，我们用MMEN来表示M和N在等式系统E下是等价的，简写为。例如给出如下的等式系统E：fsttpair,， snddpair,我们可以得到项fsttpair,和项snddpair,是等价的。 PAPi在表达带有概率选择操作的概率协议时更加的方便。我们可以用表上海交通大学工学硕士学位论文 第二章 PAPi 第 9 页 示在上的点分布，并将.111写成 2.3语义在PAPi中，操作语义由标号转移系统（Labeled Transition System, LTS）和结构等价(Structure Congruence)构成。 定义： 结构等价(Structure Congruence)是定义在扩展进程上的最小的等价关系，它在名和变量的-换元以及上下文的应用下是封闭的。结构等价的定义如下： PAR0 | 0 PARA | | | | PARC | | PEPL ! | ! NEW0 .00 NEWC . . .0 NEWPAR | | . ALIAS ./0 SUBJEST / | / | / REWRITE / E 并发操作和受限操作是标准的。ALIAS是一个任意的主动替换，SUBJEST描述的是一个主动替换应用到与它有关的进程，REWRITE则是相等的项的替换。那么根据这些等价关系我们可以得到|/ ./ | ，。 定义： 内部概率规约关系（internal probabilistic reduction）是在结构等价和上下文中封闭的最小关系，它描述的是一个进程A到一个概率分布的变换，并满足下面的关系： ID 上海交通大学工学硕士学位论文 第二章 PAPi 第 10 页 COMM . | .| NDBRAN PRBRAN THEN if then else ELSE if then else for E EVCON 既然规约规则在上下文应用下必须是封闭的，那么如果 ，我们需要定义满足 。于是我们对的定义为。 下面的这个例子可以帮助我们理解PAPi的内部概率规约： 例1：给出进程，那么有和。而且对任意进程B，都满足 | 和 | 。 where ,| , | 其中与|的一个内部规约见图2-1和2-2. 图 2-1 进程A 的概率规约 Fig.2-1 The internal probabilistic reduction from process A : :,11:,111:上海交通大学工学硕士学位论文 第二章 PAPi 第 11 页 图 2-2 进程A|B 的概率规约 Fig.2-2 The internal probabilistic reduction from process A | B 2.5执行序列如果并且0，那么从进程A到进程B需要经过一步骤，记为。 进程A的一个执行 (execution)是一个有限或者无限的步骤序列，其中,，/。我们用来表示可以从进程A开始的所有的执行的集合。对一个有限的执行，我们定义和|。对于任意|，我们用表示步骤序列。 例2：如果例1当中。那么有： | |0， | | 因为不确定选择的存在，所以扩展进程可能按不同的方式执行。直观上我们可以理解一个进程进行一步骤时，有一个调度者(scheduler)来决定下一步如何走，但这个决定是不能确定的。给一个进程A，我们用behave(A)表示A可能进行的动作，如|，调度者可以是一个函数F，它给有限的执行e分派一个分布。如果有一个调度者F，和一个进程A，和一个进程集合H，有限的执行，我们给出了下面的定义： ：为从A开始由调度者F调度执行的集合: |,0 ：。 | | | 上海交通大学工学硕士学位论文 第二章 PAPi 第 12 页 ：|（这里的比较为前缀比较），那么它的概率度量。 :表示从A开始并且经过H中某个进程的执行的集合即： | ,for some :从A开始由F调度能够到达H中某个进程的概率： 例3：如果有进程P见图2-3： 图 2-3 进程A 的概率规约 Fig.2-3 The internal probabilistic reduction from process A 其中的一个执行为 那么有1,e2,，其中1，2， 0.75，0.75。 1 0.75 0.2 0.6 0.4 2 上海交通大学工学硕士学位论文 第二章 PAPi 第 13 页 2.6等价关系与一般进程演算不同， applied pi演算更加强调对已经泄露给环境的知识(Knowledge)进行比较，从而有静态等价（static equivalence）(记为)的概念。PAPi继承了这一概念，用来建立封闭扩展进程上的等价关系，它描述的是两个进程的帧的不可区分性。直观地说，两个进程静态等价当且仅当环境无法从他们的帧中看出区别。比如 .,/与 .,/是静态等价的，因为在不知道密钥的情况下，环境无法区分这两个密文。 弱互模拟（记为）是定义在LTS下的。两个封闭扩展进程是弱互模拟的就意味着他们能执行的操作是相似的，并且它们同时是静态等价的。 Goubault-Larrecq在23里证明了弱互模拟等同观测等价。在使用进程演算分析安全协议时，我们通常使用的是观测等价，这最符合安全上的直观，即对于任意观测者来说两个进程不可区分。但是观测等价在进程演算中是非常难以证明的，因为需要考察无限多的上下文。而弱互模拟的证明却是比较方便，因此这二者的等价对安全协议验证非常有意义。静态等价和弱互模拟的详细定义请参见11。 静态等价（static equivalence）是建立在封闭扩展进程上的等价关系，它描述的是两个进程的结构的不可区分性。 这些等价关系的定义可以参考如下： 定义1：当且仅当存在某些 和替换 满足： .，而且 ， 那么我们认为两个项和在结构下是等价的，并写为 定义2：如果并满足对任意项和都有： 成立，当且仅当 也成立 那么我们说两个封闭的结构和是等价的，并且记为。 定义3（静态等价）：当两个封闭扩展进程它们的结构（frame）是静态等价时，那么这两个进程也是静态等价的，可以记为。 弱互模拟是定义在标号规则下的。两个封闭扩展进程是弱互模拟的就意味着他们能执行的操作是相似的。在11里证明了弱互模拟等同观测等价（对于任意上海交通大学工学硕士学位论文 第二章 PAPi 第 14 页 观测者来说两个进程不相同的可能性）。 定义4（弱互模拟）：是满足下面条件的封闭扩展进程间对称关系中最大的一个二元关系。如果，那么有： ； ，/，那么有且； ， ，/，那么有满足 ,，其中并且； 定义5（观测等价）：是满足下面条件的封闭扩展进程间对称关系中最大的一个二元关系。如果，那么有： ，有，那么存在且； ，/，那么有且； 对所有封闭上下文满足 CCBB。 上海交通大学工学硕士学位论文 第三章 进程之间的度量 第 15 页 第三章 进程之间的度量 上一章里我们对PAPi做了详细的介绍，我们可以看到观察等价和静态等价可以用来描述安全协议的一些性质。