基于Casper的安全攻击仿真(2)
3.2 CASPER语言 9
3.3 CASPER中的特殊字符 13
3.4 CASPER/FDR安装及使用分析 13
3.4.1 Casper/FDR安装 13
3.4.2 Casper/FDR界面介绍 15
3.5本章小结 16
4.协议安全攻击仿真的实现 17
4.1验证NSPK协议 17
4.1.1协议步骤 17
4.1.2协议过程描述 17
4.1.3协议的Casper语言表示 18
4.1.4安全仿真攻击结果分析 19
4.1.5漏洞分析 21
4.2验证NSL协议 22
4.2.1协议步骤 22
4.2.2协议过程描述 22
4.2.3协议的Casper语言表示 22
4.2.4安全仿真攻击结果分析 24
4.3本章小结 26
结 论 27
致 谢 28
参考文献 29
1引言
1.1课题背景
随着计算机技术的不断发展，网络技术的不断革新，人们的生活发生了日新月异的变化。以电子商务为代表的网络应用发展迅速，网络逐渐成为了人们工作生活中不可或缺的一部分。随着人们对网络的依赖加深，使用网络所带来的信息安全问题也日益凸出。
协议的安全性是信息安全的一个重要保障，自协议概念提出以来，很多研究者相继提出了大量的安全协议，来确保网络通信的安全。但是，由于协议的复杂应用环境，以及设计协议时侧重点的不同，导致这些安全协议大都存在一些或大或小的安全漏洞。而存在漏洞的安全协议可能会导致包括用户隐私信息泄露等问题在内的各种信息安全问题。确保协议安全一般应该从两个方面入手：一是在协议设计过程中足够严谨，每一步都进行努力推敲，力求协议不出现或少漏洞；二是在协议设计完成以后对协议进行安全性分析。所以，如何验证一个协议的安全性成为安全协议研究方面的重点。
由于安全协议存在的漏洞很难由人工方法来发现和鉴别，且由于协议运行及设计过程中的各方面复杂性，协议实际运行环境是非常复杂的。因此，安全协议的安全性验证必须通过形式化分析方法或验证工具来进行。
1.2国内外研究现状及我的工作
我国研究学者冯登国[1]提出，安全协议形式化分析的发展过程可以分为4个比较有代表性的阶段：
（1）早期阶段；
（2）形式化分析初期阶段；
（3）转折阶段；
（4）理论证明阶段；
Needham和Schroeder最早提出安全协议的形式化分析思想，他们两人创建了关于共享和公钥认证系统的安全协议[2]。其后，1983年Dolev和Yao提出了著名的Dolev-Yao模型[3]，为形式化分析研究做出了突出贡献。1989年，Burrows，Needham等人率先以逻辑形式方法提出了一种用来描述和验证密码协议的BAN逻辑[4]，BAN逻辑简洁直观，易于掌握使用，因而应用广泛。Gavin Lowe于1996年使用CSP（通信顺序进程）和模型检测技术对密码协议进行分析[5]，他首次使用CSP模型和CSP模型检测工具FDR分析NSPK协议，并成功发现一个新的攻击。Paulson利用高阶逻辑描述公式，使用基于归纳的定理证明方法，并开发出定理证明器Isabelle，这个方法更注重于验证协议的正确性[6]。
基于定理证明的分析方法也有其不足之处，其证明过程必须全程有人工参与，且需要更加深入的数学理论基础，参与者通常是专家级学者，这限制了其的普遍应用。相对的，模型检测法验证安全协议自动化程度高，过程中不需要用户参与。