《基于概率进程演算的安全协议自动化分析技术研究》由会员分享，可在线阅读，更多相关《基于概率进程演算的安全协议自动化分析技术研究（57页珍藏版）》请在金锄头文库上搜索。
1、中南民族大学 硕士学位论文 基于概率进程演算的安全协议自动化分析技术研究 姓名：邵飞 申请学位级别：硕士 专业：计算机应用技术 指导教师：孟博 2011-05-03 中南民族大学硕士学位论文 I 摘 要 安全协议的设计与验证是信息安全领域中非常重要的内容。 形式化 方法是安全协议验证的一个强有力的工具。借助自动化工具，应用形式 化方法来分析安全协议，是当今重要的研究课题。形式化方法分为：符 号方法和计算方法，符号方法把密码原语看作完美的黑盒，易于获得自 动化工具的支持，但是不能够建立密码学可靠性；计算方法基于计算复 杂性和概率理论，可以建立密码学可靠的证明，但是不易获得自动化工 具的支持。 可
2、否认认证协议是安全协议中的一类重要的协议， 广泛应用于电子 政务中。传统的对可否认性的证明是基于符号方法的，且手工的，容易 产生错误，没有建立密码学可靠性。本文引入一种基于计算模型的概率 进程演算：Blanchet 演算，对可否认认证协议中的可否认性进行了分析 与证明。主要工作如下： (1) 对安全协议的形式化涉及到的技术做了一个比较完整的概 述。重点介绍了安全协议的相关理论和分析技术。 (2) 首先对计算模型，Blanchet 演算和 CryptoVerif 工具进行了详 细的介绍，包括语法和非形式化语义、类型系统、形式化语义、观察等 价，Game 转换，并给出简单的示例。然后基于 Blan
3、chet 演算，提出一 个支持 CryptoVerif 的可否认性证明模型。采用此模型，对 Fan 等人提 出的可否认认证协议的可否认性进行了分析和证明。 (3) 基于椭圆曲线的离散对数困难问题，提出一个非交互式可否 认认证协议。并且基于提出的可否认性证明模型，应用 Blanchet 概率 演算和 CryptoVerif 工具对其可否认性进行了分析和验证。 关键词：安全协议；形式化分析；计算模型；可否认性 基于概率进程演算的安全协议自动化分析技术研究 II ABSTRACT The design and verification of security protocols play impor
4、tant 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 method and computational m
5、ethod. 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 protocol which is widely used
6、 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: Blanchet calculus. Analyze
7、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 computational method, Blanchet c
8、alculus 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 et al deniable authentica
9、tion 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 protocol；formal analysis；com
10、putational model； deniability 中南民族大学中南民族大学 学位论文原创性声明学位论文原创性声明 本人郑重声明：所呈交的论文是本人在导师的指导下独立进行研究所取 得的研究成果。除了文中特别加以标注引用的内容外，本论文不包含任何其 他个人或集体已经发表或撰写的成果作品。 对本文的研究做出重要贡献的个 人和集体，均已在文中以明确方式标明。本人完全意识到本声明的法律后果 由本人承担。 作者签名： 日期： 年 月 日 学位论文版权使用授权书学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学 校保留并向国家有关部门或机构送交论文的复印件和电子
11、版， 允许论文被查 阅和借阅。 本人授权中南民族大学可以将本学位论文的全部或部分内容编入 有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编本 学位论文。 本学位论文属于 1、保密，在_年解密后适用本授权书。 2、不保密。 （请在以上相应方框内打“”） 作者签名： 日期： 年 月 日 导师签名： 日期： 年 月 日 中南民族大学硕士学位论文 1 第 1 章 绪 论 随着信息技术的发展，网络以惊人的速度向各个领域渗透，信息的地位与作 用因计算机网络技术的快速发展而急剧上升，信息化发展改变了我们每一个人的 生产和生活方式。人们在享受网络带来便捷的同时，信息安全问题同样因此而日 显突出
12、，网络上的诈骗、赌博、传销手段日益更新，网上银行资产安全问题使人 胆战心惊，而网络协议安全是通信安全和数据安全的一个重要保障，研究者们曾 提出了大量安全协议，但是由于协议应用环境的复杂性，以及设计协议的目的侧 重多样性，这些安全协议在后来的应用中多数出现了这样或者那样的安全漏洞， 存在漏洞的安全协议可能在网络入侵者的多种攻击下无法保证信息的安全。确保 通信协议的安全需要从两方面着手：一是在协议的设计过程中加以指导，力求协 议不出现漏洞；二是在协议设计完成后对其进行安全性分析。因此，如何验证一 个设计出来的安全协议是否安全成为安全协议研究领域的重点。 由于网络环境的复杂性，并且协议会话多重交互，
13、参与的角色千变万化，非 法入侵者可能会是其中的参与主体，安全协议的漏洞很难由人工方法来发现和鉴 别，同时在设计安全协议的时候，过于理想化的推导过程和主观性的假设往往会 影响分析的结果的准确性，验证安全协议的安全性必须借助形式化的分析方法或 验证工具来完成，因此十分有必要对安全协议自动化分析技术进行深入的研究。 1.1 国内外研究现状 安全协议形式化分析方法分为两类，符号方法和计算方法，符号方法把密码 原语看作完美的黑盒，计算方法是基于计算模型的形式化方法，这种方法把密码 原语内的算法看作协议的一部分，并与其它部分一起进行建模和分析。Needham 和 Schroeder1第一次提出对安全协议进
14、行形式化分析的思想，他们分别建立了基 于对称密钥和公钥的认证协议。Dolev 和 Yao 在 1983 年提出了著名的 Dolev-Yao 模型2， 开创了安全协议形式化验证的新阶段， 为形式化分析的发展做了突出贡献。 1989 年，Burrows，Abadi 和 Needham 首次提出了一种基于知识和信念的 BAN 逻 辑3，用来描述和验证安全协议，BAN 逻辑简洁直观，易于使用，因而应用广泛。 1996 年， Gavin Lowe4使用 CSP(Communicating Sequential Processes)和模型检测技 术对密码协议进行分析，他首次采用 CSP 模型和 CSP 模
15、型检测工具 FDR 分析了 NSPK 协议，并找到了一个从未发现的安全漏洞。从 1978 年 NSPK 协议问世，到 Lowe 发现安全缺陷，已经过去了大约 17 年之久，可见分析验证安全协议的复杂 性和重要性。Paulson5,6利用高阶逻辑描述公式，使用基于归纳的定理证明方法， 基于概率进程演算的安全协议自动化分析技术研究 2 设计出了定理证明器 Isabelle，这个方法更着重于证明协议的正确性。至此，安全 协议的形式化分析方法发展到了理论证明阶段。 1993 年，Bellare-Rogaway7模型的提出开启了对计算模型形式化方法的研究， 基本思想是将协议P的安全性规约为问题Q的安全性
16、， 通过证明问题Q的安全性来 说明协议P的安全性，其中规约过程具有概率属性和时间属性。Shoup 提出了更为 抽象的模拟模型8,9， 而 Bellare-Rogaway 模型和 Shoup 提出的模拟模型不具有通用 性，不同的协议的安全性证明不能重用。1998 年，Bellare、Canetti 和 Krawczyk10 利用模拟的思想重新设计了模式方法，Canetti 和 Krawczyk11在 2001 年进一步用 不可区分思想改进了此模型方法，Blanchet12在 2006 年提出了一种基于进程概率 演算的计算模型形式化方法，并实现了证明过程自动化工具 CryptoVerif，对安全 协议的分析的证明产生了重要的影响。 本文介绍 Blanchet 演算的及其自动化工具 CryptoVerif，利用 CryptoVerif 分别 对非交互式和交互式可否认认证协议的可否认性
