文 献 综 述
信息化席卷全球，信息化技术的应用也日益广泛，因此信息的安全已成为互联网络中十分重要的问题。而安全协议作为信息安全的基础，其自身的安全性问题已成为了安全研究的重要内容[1][13]。安全协议已广泛地应用到身份认证、接入控制、密钥分配、电子商务等多个领域，其安全性的需求也越来越迫切。自安全协议出现以来，人们一直对它进行分析设计研究。但由于安全协议总是运行在复杂的、不安全的网络环境中，许多攻击方法产生的错误用人工检测很难识别，从而保证对协议安全性分析的准确性[1]。许多安全协议如“Needham-SchroedeiJ”[2]就是在发布和使用了很长一段时间才发现其漏洞的。所以必须采用形式化的方法和工具来分析和验证网络安全协议的安全性，通过有效的程序来分析系统及其条件来确定在系统满足条件下的证明是否正确。
安全协议（Security Protocol）也称作密码协议（Cryptography Protocol）[2][3]，安全协议形式化分析理论与应用研究是一种以密码学为基础的协议，它运行在计算机网络或分布式系统中，借助于密码算法来达到密钥分配、身份认证等目标。安全协议与密码算法的关系可以这样来理解，密码算法为网络上的消息提供加解密等操作（如Hash函数等），而安全协议则是在密码算法基础上为各种安全服务提供实现方案，是基于密码算法的更高一层的算法[4]。基于前文协议与算法的关系，可以简单地说，安全协议就是在消息处理环节采用了若干密码算法的协议。
然而，安全协议未必是安全的，它的安全性分析一直是一个复杂而困难的问题，对安全协议的研究已成为世界上信息与网络安全方面的一个重要研究方向[5]。实践证明，形式化方法是安全协议安全性分析更为可靠和有效的途径。
安全协议的形式化分析是采用一种正规的、标准的方法对协议进行分析，以检查协议是否满足其安全目标[6]。实践证明，形式化方法是安全协议安全性分析较为可靠和有效的途径。自二十世纪八十年代末，Burrow、Abadi和Needham提出了BAN逻辑[7]以来，用形式化的方法分析密码协议的安全性已成为密码学研究的热点之一。安全协议形式化描述一般针对安全协议诚实角色和安全协议攻击者建模，描述安全协议角色进行消息交互、处理的步骤，以及描述安全协议运行的前提假设。形式化描述语言基于数学模型，克服了非形式化描述的不精确性和二义性[5]；使用程序语言概念，具有形式化的语法和语义，可以描述安全协议的并发性、不确定性；它是进行形式化描述的一种规范，抽象于具体的实现环境，因此可作为标准的描述语言，有利于通过相应的分析工具对协议的安全目标进行自动化分析，也有利于使用自动化工具建立安全协议开发环境[8]。安全协议安全性分析是一项紧迫且意义重大的工作，它不仅能够找出协议中存在的漏洞，而且对协议的设计过程也具有指导作用。
通常将安全协议形式化分析方法分成三大类：基于推理的模态逻辑方法、基于模型检测的形式化方法和基于定理证明的形式化方法。[9]
模态逻辑方法是分析安全协议最直观、最简单的一种方法，它们描述了一个逻辑公理集合，由一些命题和推理规则组成。在推理过程中将安全协议的安全属性定义成一些可进行运算的特殊符号的集合，并且在假设的定理下运用协议公理对通信实体掌握的知识和信仰进行推导，进而得到关于安全协议属性的新知识和信仰[9]。模态逻辑方法中最具代表的是BAN逻辑，它是由Burrows等人1989 年提出来的[9][10]，主要研究可信主体在协议执行过程中所持信念的演化。
模型检测方法侧重使用状态搜索来检查协议属性，把安全协议的状态用路径安全协议形式化分析理论与应用研究的方式呈现出来，可分为前向搜索和后向搜索。模型检测方法对协议进行分析时一般可借助于自动化分析工具，同时存在形式化语言能够将把协议转化为自动工具能识别的形式[10]。自动化分析工具有一般目的的模型检测工具FDR和MurPhi;以及专为安全协议分析开发的NRL协议分析器和Interrogator等工具。比较著名的模型检测方法是CSP与 FDR相结合的方法[6][11]。
基于定理证明的分析方法侧重使用定理证明的方式给出关于协议安全属性的论证。安全协议的安全属性表示成需要证明的定理，将判断安全协议是否满足安全属性转化为证明公理系统中的目标定理是否成立。最具代表性的有重写逼近法、Schneider阶函数、Paulson归纳证明法和 Thayer Fabrega，Herzog 和 Guttman 等人[7]提出的串空间模型（strand space）。定理证明的方法可以通过定理证明器协助完成证明过程。常见的定理证明器有：Isabelle、HOL、Paradox、ACL2、PVS 和 ProVerif[8][15]。
ProVerif是BFuno Blanchet开发的基于Dolev-Yao模型的形式化自动验证密码学协议工具，是用Prolog语言实现的系统[1][4][8][13]。它能够描述各种密码学原语，包括：共享密钥密码学和公钥密钥密码学(加密和数字签名)，Hash函数和Deffie-Hellman密钥交换协议，并指定了重写规则和方程式。ProVerif能处理一个无穷会话并发协议和无穷消息空间，克服了状态空间爆炸]的问题。
以上是毕业论文文献综述，课题毕业论文、任务书、外文翻译、程序设计、图纸设计等资料可联系客服协助查找。
