- 上一篇：php+mysql项目需求管理系统设计
- 下一篇：面向WEB服务的测试执行自动化技术框架设计与实现
本文主要使用形式化验证工具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）
-
基于MATLAB的图像增强算法设计
-
jsp+sqlserver高校二手商品交...
-
基于Kinect的手势跟踪与识别算法设计
-
JAVA基于安卓平台的医疗护工管理系统设计
-
java+mysql设备监控记录的大...
-
基于核独立元分析的非线...
-
基于Hadoop的制造过程大数据存储平台构建
十二层带中心支撑钢结构...
乳业同业并购式全产业链...
酸性水汽提装置总汽提塔设计+CAD图纸
java+mysql车辆管理系统的设计+源代码
杂拟谷盗体内共生菌沃尔...
河岸冲刷和泥沙淤积的监测国内外研究现状
大众媒体对公共政策制定的影响
当代大学生慈善意识研究+文献综述
中考体育项目与体育教学合理结合的研究
电站锅炉暖风器设计任务书