基于概率进程演算的安全协议自动化分析技术研究-邵飞.pdf

《基于概率进程演算的安全协议自动化分析技术研究-邵飞.pdf》由会员分享，可在线阅读，更多相关《基于概率进程演算的安全协议自动化分析技术研究-邵飞.pdf（57页珍藏版）》请在得力文库 - 分享文档赚钱的网站上搜索。

1、中南民族大学 硕士学位论文 基于概率进程演算的安全协议自动化分析技术研究 姓名：邵飞 申请学位级别：硕士 专业：计算机应用技术 指导教师：孟博 2011-05-03中南民族大学硕士学位论文 I 摘 要 安全协议的设计与验证是信息安全领域中非常重要的内容。 形式化 方法是安全协议验证的一个强有力的工具。 借助自动化工具， 应用形式 化方法来分析安全协议， 是当今重要的研究课题。 形式化方法分为： 符 号方法和计算方法， 符号方法把密码原语看作完美的黑盒， 易于获得自 动化工具的支持， 但是不能够建立密码学可靠性； 计算方法基于计算复 杂性和概率理论， 可以建立密码学可靠的证明， 但是不易获得自动

2、化工 具的支持。 可否认认证协议是安全协议中的一类重要的协议， 广泛应用于电子 政务中。 传统的对可否认性的证明是基于符号方法的， 且手工的， 容易 产生错误， 没有建立密码学可靠性。 本文引入一种基于计算模型的概率 进程演算： Blanchet 演算， 对可否认认证协议中的可否认性进行了分析 与证明。主要工作如下： (1) 对安全协议的形式化涉及到的技术做了一个比较完整的概 述。重点介绍了安全协议的相关理论和分析技术。 (2) 首先对计算模型，Blanchet 演算和 CryptoVerif 工具进行了详 细的介绍， 包括语法和非形式化语义、 类型系统、 形式化语义、 观察等 价，Game

3、转换， 并给出简单的示例。 然后基于 Blanchet 演算， 提出一 个支持 CryptoVerif 的可否认性证明模型。采用此模型，对 Fan 等人提 出的可否认认证协议的可否认性进行了分析和证明。 (3) 基于椭圆曲线的离散对数困难问题，提出一个非交互式可否 认认证协议。并且基于提出的可否认性证明模型，应用 Blanchet 概率 演算和 CryptoVerif 工具对其可否认性进行了分析和验证。 关键词：安全协议；形式化分析；计算模型；可否认性 基于概率进程演算的安全协议自动化分析技术研究 II ABSTRACT The design and verification of secur

4、ity protocols play important roles in information security field. Formal verification of security protocols with automated tools is a powerful technology. The research in the methods of formal analysis for security protocols is a hot topic today. Formal methods place into two categories: symbolic me

5、thod and computational method. In symbolic method, the cryptographic primitives serve as perfect black boxes. Computational method is based on computational complexity and probability theory; it can create a reliable proof of cryptography. Deniable authentication protocol is a kind of security proto

6、col which is widely used in e-government. The traditional proof of deniability based on symbolic method, it is manual and prone to error, and it cannot establish cryptography reliability. This paper introduces a probability model based on a kind of probabilistic polynomial-time process calculus: Bla

7、nchet calculus. Analyze and prove the deniability of deniable authentication protocol using this process calculus. Main works are as follows: (1) A complete overview on technology of the formal methods. Focus on the theory of security protocols and analysis techniques. (2) Firstly introduce computat

8、ional method, Blanchet calculus and CryptoVerif in detail, including syntax and non-formal semantics, type systems, formal semantics, observation equivalence, Game conversion, and give a simple example. Then proposed a deniable model based on Blanchet calculus. Apply this model to the proof of Fan e

9、t al deniable authentication protocol. (3) Based on elliptic curve discrete logarithm problem; present a non-interactive deniable authentication protocol. Analyze and prove the deniability of this protocol using the proposed deniable model, Blanchet calculus and CryptoVerif. KEY WORDS: security prot

10、ocol ；formal analysis ；computational model ； deniability 中南民族大学 学位论文原创性声明 本人郑重声明： 所呈交的论文是本人 在导师的指导下独立进行研究所取 得的研究成果。 除了文中特别加以标 注引用的内容外， 本论文不包含任何 其 他个人或集体已经发表或撰写的成果作品。 对本文的研究做出重要贡献的个 人和集体， 均已在文中以明确方式标明。 本人完全意识到本声明的法律后 果 由本人承担。 作者签名： 日期： 年 月 日 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、 使用学位论文的规定， 同意学 校保留并向国家有关部门或机

11、构送交 论文的复印件和电子版， 允许论文被查 阅和借阅。 本人授权中南民族大学可以将本学位 论文的全部或部分内容编入 有关数据库进行检索， 可以采用影印、 缩印或扫描等复制手段保存和汇编 本 学位论文。 本学位论文属于 1 、保密 ，在_年解密后适用本授权书。 2 、不保密 。 （请在以上相应方框内打“ ” ） 作者签名： 日期： 年 月 日 导师签名： 日期： 年 月 日 中南民族大学硕士学位论文 1 第 1章 绪 论 随着信息技术的发展，网络以惊人的速度向各个领域渗透，信息的地位与作 用因计算机网络技术的快速发展而急剧上升，信息化发展改变了我们每一个人的 生产和生活方式。人们在享受网络带来

12、便捷的同时，信息安全问题同样因此而日 显突出，网络上的诈骗、赌博、传销手段日益更新，网上银行资产安全问题使人 胆战心惊，而网络协议安全是通信安全和数据安全的一个重要保障，研究者们曾 提出了大量安全协议，但是由于协议应用环境的复杂性，以及设计协议的目的侧 重多样性，这些安全协议在后来的应用中多数出现了这样或者那样的安全漏洞， 存在漏洞的安全协议可能在网络入侵者的多种攻击下无法保证信息的安全。确保 通信协议的安全需要从两方面着手：一是在协议的设计过程中加以指导，力求协 议不出现漏洞；二是在协议设计完成后对其进行安全性分析。因此，如何验证一 个设计出来的安全协议是否安全成为安全协议研究领域的重点。

13、由于网络环境的复杂性，并且协议会话多重交互，参与的角色千变万化，非 法入侵者可能会是其中的参与主体，安全协议的漏洞很难由人工方法来发现和鉴 别，同时在设计安全协议的时候，过于理想化的推导过程和主观性的假设往往会 影响分析的结果的准确性，验证安全协议的安全性必须借助形式化的分析方法或 验证工具来完成，因此十分有必要对安全协议自动化分析技术进行深入的研究。 1.1 国内外研究现状 安全协议形式化分析方法分为两类，符号方法和计算方法，符号方法把密码 原语看作完美的黑盒，计算方法是基于计算模型的形式化方法，这种方法把密码 原语内的算法看作协议的一部分，并与其它部分一起进行建模和分析。Needham 和

14、 Schroeder 1 第一次提出对安全协议进行形式化分析的 思想，他们分别建立了 基 于对称密钥和公钥的认证协议。Dolev 和 Yao 在 1983 年提出了著名的 Dolev-Yao 模型 2 ， 开创了安全协议形式化验证的新阶段， 为形式化分析的发展做了突出贡献。 1989 年，Burrows ，Abadi 和 Needham 首次提出了一种基于知识和信念的 BAN 逻 辑 3 ， 用 来描述和验证安全协议，BAN 逻辑简洁直观， 易于使用， 因而应用广泛。 1996 年， Gavin Lowe 4 使用 CSP(Communicating Sequential Processes)

15、 和模型检测技 术对密码协议进行分析，他首次采用 CSP 模型和 CSP 模型检测工具 FDR 分析了 NSPK 协议，并找到了一个从未发现的安全漏洞。从 1978 年 NSPK 协议问世，到 Lowe 发现安全缺陷，已经过去了大约 17 年之久，可见分析验证安全协议的复杂 性和重要性。Paulson 5,6 利用高阶逻辑描述公式，使用基于归纳的定理证明方法，基于概率进程演算的安全协议自动化分析技术研究 2 设计出了定理证明器 Isabelle ，这个方法更着重于证明协议的正确性。至此，安全 协议的形式化分析方法发展到了理论证明阶段。 1993 年，Bellare-Rogaway 7 模型的提

16、出开启了对计算模型形式化方法的研究， 基本思想是将协议 P 的安全性规约为问题 Q 的安全性， 通过证明问题 Q 的安全性来 说明协议 P 的安全性， 其中规约过程具有概率属性和时间属性。 Shoup 提出了更为 抽象的模拟模型 8,9 ， 而 Bellare-Rogaway 模型和 Shoup 提出的模拟模型不具有通用 性， 不同的协议的安全性证明不能重用。1998 年，Bellare 、Canetti 和 Krawczyk 10 利用模拟的思想重新设计了模式方法，Canetti 和 Krawczyk 11 在 2001 年进一步用 不可区分思想改进了此模型方法，Blanchet 12 在

17、2006 年提出了一种基于进程概率 演算的计算模型形式化方法，并实现了证明过程自动化工具 CryptoVerif ，对安全 协议的分析的证明产生了重要的影响。 本文介绍 Blanchet 演算的及其自动化工具 CryptoVerif，利 用 CryptoVerif 分别 对非交互式和交互式可否认认证协议的可否认性进行自动化分析和证明。 1.2 论文结构安排 本文共分为五章，第一章为绪论，主要概述安全协议形式化分析方法的研究 背景； 第二章主要介绍安全协议的基本概念、 分类及其性质及其形式化分析方法； 第三章详细介绍了基于计算模型的 Blanchet 演算及自动化验证工具 CryptoVerif

18、 ； 第四章对可否认认证协议进行了简要的介绍，提出的一个基于椭圆曲线的非交互 式可否认认证协议，使用 Blanchet 演算和 CryptoVerif 工具分别对提出的基于椭圆 曲线的非交互式可否认认证协议和 Fan 交互式协议下可否认性进行了证明；第五 章为总结。 中南民族大学硕士学位论文 3 第 2章 安全协议形式化分析方法 2.1 安全协议介绍 安全协议，也称作密码协议，是以密码学为基础的消息交换协议，其目的是 在网络环境中提供各种安全服务。密码学是网络安全的基础，但是网络安全又不 能仅仅依靠密码算法，安全协议是网络安全的一个重要组成部分，它运行在计算 机通信网或分布式系统中，借助密码算

19、法来达到密钥分配和身份认证等目的。 安全协议的安全目标是多种多样的，但是基本目标是实现通信主体的身份认 证并为后续的通信过程安全地分配密钥或其他各种秘密，所以身份认证和密钥保 密是安全协议最基本的安全属性， 也是安全协议形式化分析主要研究的两个属性； 在通信的过程中，通信各方交换的信息可能存在涉及个人隐私、不想被他人知道 或篡改的秘密，因此安全协议应该具有保密性和完整性；另外，如果通信的任一 方违反了协议的规则，参与通信的其余各方能够搜集证据，防止抵赖。 按照安全协议功能，可以将其分成以下几类： (1) 密钥协商协议 该类协议用于完成参与者之间会话密钥的建立，通常是在参与协议的两个或 者多个参

20、与者之间建立共享的密钥。例如一次通信中使用的会话密钥，协议中可 以采用对称密钥密码体制，也可以采用非对称密钥密码体制。对称密钥下加解密 过程比非对称密钥下加解密过程要快很多，因此使用对称密钥策略可以处理更多 信息。然而在每两个通信实体之间都保存一个只有这两个实体才知道的对称密钥 是不现实的。针对这个问题，可以使用公钥密码体制为每次通信过程新生成一个 新的对称密钥， 即会话密钥， 为分配会话密钥而设计的协议被称为密钥协商协议。 例如 Diffie-Hellman 密钥协商协议 13 。 通常这类协议需要一个可信的第三方服务器 负责生成和管理会话密钥。 (2) 身份认证协议 身份认证是指证实主体的

21、真实身份与其所声称的身份是否相符的过程。该类 协议的目的是验证参与协议的一方或者若干方确实是这些参与者自己所声称的身 份。身份认证协议依赖参与者所特有的一些特征，比如密钥或密码，通过输入密 码来登录系统也算是一种简单的身份认证协议。根据是否依赖第三方可把身份认 证协议分为基于可信第三方的认证协议和双方认证协议；根据认证使用的密码体 制分为基于对称密钥的认证协议和基于公钥密码体制的认证协议；根据认证实体 的个数分为单向认证协议和双向认证协议。著名的身份认证协议有 N-S 协议 1 。 (3) 认证密钥交换协议 认证密钥交换协议将身份认证协议和密钥交换协议结合在一起，是网络通信基于概率进程演算的安

22、全协议自动化分析技术研究 4 中应用最普遍的安全协议，该协议可分为身份认证和密钥协商两个阶段，先对通 信主体的身份进行认证，通信主体只有通过身份认证，才能获得安全通信过程的 会话密钥。常见的认证密钥交换协议是 Kerberos 协议 14 。 (4) 电子商务协议 电子商务协议往往比较复杂，会运用更多的安全技术，而且协议的参与者代 表了交易的双方， 因为交易双方的利益目标不一致， 甚至根本就是矛盾的， 所以， 电子商务协议最关注的是公平性，即协议必须保证交易的双方都不能通过损害对 方的利益来得到它不应该得到的利益。电子商务协议中，除了需要满足上面已提 到的安全属性，如认证性，保密性等等，还要要

23、求具有原子性、匿名性和不可否 认性。常用的电子商务协议是 SET 协议。 2.2 基于符号模型的安全协议形式化分析方法 符号方法，也称为基于 Dolev-Yao 模型的方法，是形式化分析方法研究的主 流，起步较早，发展较成熟，自动化程度较高。符号方法是将安全协议本身与其 所使用的密码系统隔离，把密码系统看作是一个完美，没有任何漏洞且独立的黑 盒子，并在此基础上对安全协议进行分析和验证，然而实际情况下，密码系统的 正确性难以保证。目前存在多种基于符号模型的形式化方法用于分析和验证，主 要包括信念逻辑方法（基于推理的结构性方法）、模型检测方法（基于攻击的结 构性方法）和定理证明方法（基于证明的结构

24、性方法）。 2.2.1 信念逻辑方法 信念逻辑方法是基于知识集合和信念集合的，由命题和推理规则组成一个完 整的逻辑系统，命题表示主体对消息的知识或信念，推理规则表示知识和信念的 转换法则，可以从已知的知识和信念推导出新的知识和信念。通过一系列的推理 过程来验证协议的安全性。 在众多基于信念逻辑的形式化分析方法中，最著名的是 1989 年 Burrows 等人 提出的 BAN 逻辑，随后使用 BAN 逻辑对 N-S 协议、Kerberos 协议进行了分析， 成功的找出了其中已知或未知的漏洞，使得人们对于这种分析和验证方法产生了 极大的兴趣， 但它也存在很多缺陷 15 ， 首先，BAN 逻辑的抽象

25、层次较高， 语义模 糊；其次，它应用范围较小，只能对安全协议中的认证性进行分析，不支持其它 一些重要的安全属性，如保密性；再者，当逻辑分析发现协议中的错误时，每个 人都相信那确实是协议有问题，而当逻辑分析一个协议是安全时，却没有人敢相 信它的正确性， 即该方法具有非形式化性质的理想化假设。 针对 BAN 逻辑存在的 缺陷， 在 BAN 逻辑基础上又出现了 GNY 逻辑 16 、 AT 逻辑 17 、 VO 逻辑 18 、 Kailar中南民族大学硕士学位论文 5 逻辑 19 、CS 逻辑 20 、KG 逻辑 21 和 Nonmonnotomic 逻辑 21 等。 2.2.2 模型检测方法 早期

26、的模型检测技术是一种分析和模拟硬件工作过程的形式方法，后来逐渐 用于分析软件和模拟通信协议， 近年来已发展成为安全协议分析的一个重要手段。 其基本思想类似于图灵机，主要关注协议的状态及其转换，将协议表示成一个状 态集合和一个状态转移集合，并对攻击者和参与者在协议所有可能的路径进行穷 举搜索，检测协议的安全性是否在每条路径上都被满足。模型检测有两种搜索方 式：一种是前向搜索，从某个初始状态出发，随着协议的执行，看是否能到达一 个不安全的状态；另一种是后向搜索，先确定一个不安全的状态，看是否有一条 能到达合法的初始状态的路径。 模型检测方法是非常有效的安全协议的分析方法，这种方法的验证过程是由 计

27、算机自动完成，验证过程中不需要用户参与，因此其自动化程度高。如果发现 协议有漏洞，还能够自动输出反例，但是模型检测方法容易产生状态空间爆炸问 题，不适用于比较复杂的协议；需要指定附加的运行参数，比如主体的数量。需 要注意的是，使用模型检测方法即使没有发现协议的漏洞，也并不能保证协议一 定是安全的。 模型检测方法需要借助于自动化工具，按照适用范围不同可把它们分成三类 21 ： (1) 通用的，不是专为安全协议形式化分析而设计的工具，是基于一阶逻辑、 Mur 、通信顺序进程 CSP 等验证语言的，这类方法仅仅是验证协议的正确性， 而忽略了安全属性。其中比较著名的是 Gavin Lowe 在 199

28、6 年使用基于 CSP 的模 型检测工具 FDR 对 Needham-Schroeder 协议进行了分析，并发现了一个以前没有 发现的漏洞。 (2) 基于安全协议代数重写性质的一类单一代数理论模型， 这种方法主要侧重 于研究协议状态的可获性。 Dolev 和 Yao 首次给出了该模型， 此后 Bellovn 和 Merritt 、 Meadows 、Woo 和 Lam 、Genet 和 Klay 都在该领域进行了卓有意义的研究。 (3) 为特定安全目标设计的工具， 这种方法对协议的分析能力有限， 可以找出 已知攻击，但无法找出未知的攻击。如 Interrogator 和 NRL 协议分析器。

29、2.2.3 定理证明方法 模型检测方法是从安全协议的反向寻找协议中存在的漏洞，定理证明方法是 从正向说明安全协议的安全性， 定理证明方法是用数学的手段证明协议的正确性， 这点与基于信念逻辑方法相似，但它不是使用命题和推理规则的手段，而是借助基于概率进程演算的安全协议自动化分析技术研究 6 语义更明确、规则更完善的数学方法，可以分析任意大小的协议，不限制主体参 与协议运行的回合数。 定理证明方法是一种有效验证协议的正确性的方法，但它难以发现协议的缺 陷，且证明过程是手工或半自动化的。 Kemmerer 等学者设计的 Ina Jo 和 ITO 是定理证明方法的典型代表 21 ， 另一项 重要的方法

30、是 Paulson 的基于归纳的定理证明方法 23 ，Paulson 设计的定理证明器 Isabelle 可以使用归纳方法分析安全协议，此后 Thayer 、Herzog 、Guttman 基于 Paulson 方法提了著名的串空间模型 24 。 Proverif 25 工具是近年来较为成功的形式化 工具， 由 Blanchet 设计和开发， 输入语言为扩展 pi 演算或 horn 子句， 核心处理部 分负责对安全属性进行逻辑推导证明，最终把结论以用户可读的形式给出。 2.3 基于计算模型的安全协议形式化分析方法 相对于符号方法，基于计算模型的安全协议分析方法更接近协议的实际运行 情况，它把密

31、码原语内的计算部分也作为协议的一部分进行建模和分析，假定密 码原语是不完美的，即攻击者可以对密码原语进行攻击。改善了形式化证明和协 议实际运行情况之间的隔阂。基于计算模型的形式化分析方法的理论基础是概率 和计算复杂性，设计过程中还参考了最新的密码学成果。 对计算模型形式化方法的研究始于 Bellare-Rogaway 模型 7 ，基本思想是将协 议 P 的安全性规约为问题 Q 的安全性， 通过证明问题 Q 的安全性来说明协议 P 的安 全性， 其中规约过程具有概率属性和时间属性。 Shoup 8,9 提出了更为抽象的模拟模 型， 而 Bellare-Rogaway 模型和 Shoup 提出的模

32、拟模型不具有通用性， 不同的协议 的安全性证明不能重用。1998 年，Bellare 、Canetti 和 Krawczyk 10 利用模拟的思想 重新设计了模式方法，Canetti 和 Krawczyk 11 在 2001 年进一步用不可区分思想改 进了此模型方法，另外 Abadi 和 Rogaway 16 在提出一种具有计算合理性 (Computational Soundness) 的符号模型，试图连接起符号 模型和计算模型，分别基 于符号模型和计算模型对私钥加密算法进行了建模，证明了在符号模型下的保密 性在计算模型下同样存在，给出了一种符号模型下加密算法的计算性证明方法。 在文献16 中

33、，Abadi 等人对安全协议形式化分析中的符号模型和计算模型进行了 权威和详细的综述。Blanchet 12 在 2006 年提出了一种基于进程概率演算的计算模 型形式方法并实现了证明过程自动化工具 CryptoVerif ，对安全协议的分析的证明 产生了重要的影响。计算模型下的形式化方法证明协议安全性的过程通常包括三 个基本步骤： (1) 对协议参与方和运行环境进行建模，对攻击者行为进行建模。 (2) 定义安全目标，即将要证明的协议的安全属性。 中南民族大学硕士学位论文 7 (3) 证明安全目标， 使用变换规则， 对所建立起来的模型进行不断规约， 若在 概率多项式时间内能够证明安全目标，则协

34、议具有相应的安全属性。 基于概率进程演算的安全协议自动化分析技术研究 8 第 3章 Blanchet演算和 CryptoVerif 工具 3.1介绍 3.1.1 概要 在计算模型中，消息是位串，攻击者是一个概率多项式时间图灵机，这种模 型接近于协议实际的运行情况，但当前典型的基于该方法的论证过程往往是人工 的和不规范的。相比之下，在符号模型即形式化的 Dolev-Yao 模型中，密码原语 被当作完美的黑盒子，它们通过已建立的代数系统中的函数符号来表示，如项， 可能还会有一些等式。分析协议时可以直接调用这些黑盒子，而不用考虑其内部 实现细节。基于这种具有较高抽象性的模型，可以建立自动化验证工具，

35、但是通 常基于符号模型的安全性论证没有计算模型下准确。 自从 Abadi 和 Rogaway 26 发表了开创性的论文后，如何关联两种模型的问题 便引起研究者的强烈关注。通常，它们先是表明 Dolev-Yao 模型符合计算模型这 种观点的合理性，并进而获取基于符号模型的协议自动化论证来间接说明在计算 模型下的协议正确性。然而，这种方式依然具有很大局限性，因为计算模型和符 号模型并不是严格等价的，需要附加的假设去保证它们等价关系的正当性（对密 码原语要有专门的安全性约束 27 ）。 在计算模型下， Blanchet 提出了一种新的协议自动化证明方法， 并且已经实现 了一个直接依赖计算模型的自动化

36、证明工具 CryptoVerif ，已经证明在存在主动攻 击和并发会话的环境下，该工具的证明结果同样有效。该方法的证明过程通过 Game 序列 8,9,28 的形式表现， 类似的表现方法已经使用在一些密码学研究中， 在一 个 Game 序列中， 初始 Game 代表将要进行分析和证明的协议， 以 Blanchet 演算的 形式给出，证明的最终结果是特定安全属性的被攻击成功的概率，序列中其它每 一个 Game 都是对其前一个 Game 进行特定的转换而获得的， 并且上下文可区分相 邻 Game 间差别的可能性很小， 即在外部看来相邻 Game 之间是等价的， 差别基本 上是可忽略的， 若最后一个

37、 Game 可以证明安全目标， 即攻击者获胜的可能性为 0， 综上所述，可以得出初始 Game 攻击者获胜的可能性是可忽略的。 这里使用一种新的概率进程演算，称为 Blanchet 演算，Blanchet 演算基于 pi 演算和其他几种演算 29,30,31,32 的思想。 在这种演算中， 消息是位串， 密码原语可看 作是位串到位串的函数的序列。这种演算具有概率学语义，并且所有的进程的运 行都是多项式时间的。观察等价是证明安全属性过程中使用到的主要技术，其基 本思想是：若攻击者能够区分进程 Q 和 Q 的可能性是可忽略的，就表示 Q 观察等 价于 Q ，即 QQ 。 在上面提到的几种演算的基础

38、上，Blanchet 演算增加了一种新中南民族大学硕士学位论文 9 的功能，进程执行过程中所有的变量的值都存储在数组中，这也是协议验证过程 自动化的关键， 比如，xi 表示进程索引编号为 i 中的 x 变量的值。 数组代替链表， 经常用在协议的人工论证时。例如，考虑 MAC 安全性的定义。通常，这些安全性 定义了攻击者伪造 MAC 成功概率是可忽略的，也就是说，所有的正确的 MACs 都 是经过调用 MAC 生成算法获得的。 因此， 在密码学证明中， 有一个链表保存 MAC 算法中处理过的参数， 当要证明消息 m 的 MAC 时， 可以另外检查消息 m 是否在链 表中。在 Blanchet 演

39、算中， MAC 生成算法使用过的参数都保存在数组中，可以通 过遍历这个数组的方法来寻找消息 m。因为数组一直存在于演算中，因此它 的使 用更便于实现自动化论证，相对于人工论证中的链表，数组不需要对插入其中的 值进行附加的说明。正是这样，消除了许多细微但是很难自动化的语法转换，并 且可以更方便的通过等式来表示数组元素之间的关系，还可能涉及在数组索引上 的计算。 CryptoVerif 工具证明过程其实就是一系列的 Game 转换过程，为了把初始 Game 经过若干次转换而变成一个满足安全属性的最终 Game ，其中重要的一类转 换需要应用密码原语安全性定义。关于这一类转换将在 3.3.2 小节详

40、细介绍， Blanchet 用观察等价LR 作为每个密码原语的安全性定义， L 和 R 是一系列的 函 数（输入为函数的参数，输出为运行结果），LR 表示可以把调用 L 的进程 Q 转 换为调用 R 的进程 Q 。Blanchet 已经用观察等价LR 的形式对若干密码原语的安 全性进行了定义，如私钥加密算法，公钥加密算法，数字签名算法，摘要算法。 除此之外，其它类型的转换都可看作是语法转换，语法转换是为了更好地应用密 码原语的安全定义，密码原语安全性定义转换和语法转换相结合实现 Game 转换。 为了证明协议安全性，CryptoVerif 使用启发式证明策略执行 Game 转换：当 应用一个语

41、法或密码原语安全性转换失败后，工具会检查该转换必须的前提是否 全部满足，若有的条件不满足，会先对该条件施行转换，直到所有的条件都已满 足， 这种策略使得协议证明过程可以完全的自动化。CryptoVerif 还提供交互模式， 也就是说，可以人工指定要应用的转换，通过密码原语函数和相关的密钥来指定 要使用的特定密码原语的安全假设，使用启发式策略来推断中间可能要使用到的 语法转换。这种交互模式对于某些基于公钥密码机制的安全协议十分有用，因为 在有的情况下，可能同时有几个密码原语的安全定义可以使用，但只有其中的一 个能够引出正确的证明。CryptoVerif 是可靠的，无论用户给出任何指示，如果该 工

42、具能够证明出某协议的一个安全属性，那么在密码原语安全定义正确前提下， 该安全属性一定满足。 CryptoVerif 工具是使用 Objective Caml 语言开发出来的。 基于概率进程演算的安全协议自动化分析技术研究 10 3.1.2 标记 我们先简要的介绍一下基本的标记， 其中 1122 / , / ,., / mm M xM x M x 表示用项 j M 替换 j x ,其中jm ， 集合 S 的阶用符号| S 来表示。 如果 S 是一个有限集， R x S 表示在集合 S 中随机选择一个元素且把它的值赋给 x。如果 A 是一个概率算法，那 么 () 1 , m x Ax x L 表示

43、随机选择项 r ， 且在 r 下运行 ( ) 1 , m Ax x L 的结果赋给 x ， 另外， x M 表示一个简单的赋值操作。 Blanchet 演算中使用到的其他一些标记和解释如表 3.1 所示： 表3.1 标记和语法 i 编号 1 , m xM M L 变量 项 M,N:= 1 , m fMM L 函数 0 空 QQ 并行 ! in Q 复制 n 次 1 , m cM M L 通道 输入进程 Q:= ( ) 111 , :, : ; lk k cMLM xi TLx i T P %输入 11 c, ,; lk M MN NQ LL 输出 1 new , , :; m xiiT P L

44、 随机数 1 let , , : m xiiTM i n P = L 赋值 () 1 if defined , then else l M MMPP L 条件 输出进程 P:= () 11 1 , , suchthat find else defined , , then jj m j j jm jm j jlj j j uuin P MMMP = % L L查询 3.2 Blanchet演算 3.2.1 语法和非形式化语义 本节将对 Blanchet 演算中标记的语法和语义进行更加详细的解释， 在表 3.1 中 所列举出标记的表示方法参考了 pi 演算和其他一些演算 29,30,31,32

45、。 Blanchet 演算定义包含通道名的可数集 c ，存在一个从通道到整数的映射 maxlen ， () maxlen c 表示通道 c 上发送的消息的最大长度， 表示一个提前指定的 安全参数， 大于 () maxlen c 长度的消息会被自动分段后再发送出去， 对任一通道 c ， () maxlen c 是 的多项式表示（这是所有进程运 行在多项式时间内的一个重要的保 证）。 中南民族大学硕士学位论文 11 Blanchet 演算还使用参数 n， () In 表示在给定的一个安全参数 下对整数变量 n 的变换， () In 是一个函数， 输入为 n， 输出为一整数， 该函数在以 为参数的多

46、 项式时间内运行。 该演算还使用到类型符号 T ， 对于安全参数 的每一个实际值， 每种类型 T 对 应于一个元素集合 () IT ，bitstring 是所有位串的全集， 表示空位串， 集合 () IT 是 在多项式时间下可识别的，也就是说，存在一个多项式时间复杂度算法用于判断 一个元素是否在集合 () IT 内，fixed length 属性的类型表示该类型的变量具有相同 的长度。 large 属性表示集合 () IT 集合内的元素数量极多，即1/ | ( ) | IT 小到可以忽 略不计，Blanchet 演算已经定义了几种常用的类型， bool 类型的变量可取值集合 (), I boo

47、l true false = ，false 是 0 ，true 是 1 ， 其它还有() I bitstring Bitstring = ， (1, ) 1, ( ) InIn = 。 Blanchet 演算中， f 表示函数符号，一个函数符号意味着一个类型转换 1 : . m fTTT 。每个 f 对应于 1 ( ) . ( ) m IT IT 到T 中的函数集合 () If 中的一个 函数， 且其中任一函数 1 ( )( ,., ) m Ifx x 是多项式时间可计算的。Blanchet 演算已经定 义了一些特定函数关系， M N = 用于判断是否等价， M N 用于判断是否不等价， M

48、N 表示逻辑或， M N 表示逻辑与， M 表示逻辑非。 在该演算中， 项表示位串或在之上的计算。 索引 i 是一个整数， 在并发环境下 用于区分同一个进程的不同拷贝，变量 1 ,., m xMM 表示 m 维数组 x 中的索引为 1,., m M M 的变量的值。 函数应用 1 ( ,., ) m fMM 返回输入为 1,., m M M 的函数 f 的输出结 果。 演算包含两种进程： 输入进程 Q 和输出进程 P ， 输入进程 Q 负责在一个通道接 收消息。 输出进程 P 负责内部计算和在一个通道上发送消息， 输入进程 0 什么也不 做， QQ 是两个进程的并行组合；! in Q 表示进程的 n 个拷贝并行运行，且每个进 程对应一个不同的索引 1, in ; ; newChannel c Q 新建一个私有通道 c 然后执行进程 Q ， 关于输入进程的语法 ( ) 1