基于Casper的安全攻击仿真(3)
本文主要使用形式化验证工具Casper/FDR对NSPK协议进行验证，发现攻击漏洞并改进，并对其进行再次验证分析。
1.3论文结构安排
本次课题是通过基于Casper安全攻击仿真的研究，总结分析出安全协议的相关概念，以及基于Casper安全攻击仿真实现的方法。并通过对。。协议的安全分析，达到熟练掌握使用Casper/FDR工具进行仿真的目的。根据本人的工作，本论文分四章，具体内容安排如下：
第一章：引言。首先对课题背景进行了概述，随后简要介绍了国内外的研究现状及安全协议研究发展的几个阶段，最后对本文的组织结构进行了说明。
第二章：安全协议及协议分析方法概述。本章介绍了安全协议的基本概念，安全协议的常见攻击方法，安全协议的设计规范以及安全协议的分析方法等相关背景知识。并对安全协议形式化分析所用到的模型检测工具进行了简要介绍。
第三章：Casper/FDR工具分析。本章首先分析了Casper/FDR工具的由来及发展，其后讲解了Casper的语法规范，并举例说明。其后截图说明了Casper/FDR工具的安装，安装过程中需要注意环境变量的设置。最后，对软件主界面进行了简要介绍。
第四章：协议安全攻击仿真的实现。本章通过Casper/FDR工具实现了对NSPK协议以及NSPK协议的改进协议NSL协议的安全仿真攻击，并通过对NSPK协议攻击漏洞的分析得出改进方案NSL协议，再现了当年Lowe发现NSPK协议漏洞并改进得到NSL协议的全过程。同时也进一步用实例说明了Casper/FDR工具的使用。
1.4本章小结
首先对课题背景进行了概述，随后简要介绍了国内外的研究现状及安全协议研究发展的几个阶段，最后对本文的组织结构进行了说明
2.安全协议及协议分析方法概述
2.1安全协议概述
2.1.1安全协议的基本概念
协议[7]即参与各方要遵守的规范和约定，是两个或者两个以上的参与者为完成某项特定的任务而采取的一系列动作的集合。协议还具有如下特点：（1）协议中每个参与的实体都必须足够了解协议，并且预先了解自身所要完成的所有动作；（2）协议中的每个可信实体都必须同意并遵循协议要求；（3）协议的描述必须要足够清晰，每一步都必须有明确定义并且不会引起误解；（4）协议必须是完整的，对每种可能出现的情况必须规定出相应具体的动作。
安全协议[8]，也可称作密码协议，其是以密码学为基础的消息交换协议，它的目的是在网络环境中提供各种满足完整性、私密性、认证性、不可否认性的安全服务。
2.1.2安全协议分类
安全协议的分类方式有很多，现根据协议完成的功能进行划分，可以分成4类：
1. 密钥交换协议（Key Exchange Protocol）
通常用于在参与协议的多个实体间建立共享密钥，一般情况下适用于单次通信中所使用的会话密钥，协议可使用对称密码机制，也可使用非对称密码体制。由于使用对称密钥加密解密比使用非对称密钥加密解密的过程要快很多，所以使用对称密钥可以处理大量通信信息。然而在每对通信实体之间都保存一个保密的对称密钥是不现实的，因此一般是用公钥密钥体制为每次通信过程生成一个新的对称密钥（又称为会话密钥）。分配这个对称密钥的协议就被称为密钥交换协议。这种协议一般需要一个由可信第三方服务器生成的会话密钥（可信的）。例如Diffie-Hellman密钥交换协议。
2. 认证协议（Authentication Protocol）