基于Casper的安全攻击仿真
本毕业论文主要应用Casper/FDR（Communication Sequential Process/ Failure Divergence Refinement）工具，来验证安全协议的安全性。主要的研究成果如下：
（1） 介绍了对安全协议和安全协议检测方法的概念
（2） 分析了Casper/FDR工具的安装使用
（3） 研究并分析了Casper语言及语法
（4） 利用Casper/FDR工具研究NSPK协议的安全性，并对发现的攻击漏洞进行分析，得到改进方案即NSL协议，并对之进行分析。
关键词 安全协议 安全攻击仿真 形式化分析方法 模型检测 Casper/FDR
毕业设计说明书（论文）外文摘要
Title Security attack simulation based on Casper
Abstract
Along with the development of computer networks, network technology has brought a lot of convenience to our work and life. But enjoy the convenience that network bring to us, network security issues become increasingly prominent attendant.Information security is the most important thing of the network security system.The security protocols which is an important part of modern information security, provides a wide variety of security services in networks and distributed systems and occupies an important position in the information systems security. Therefore, the security analysis of security protocols are important.
This paper studies on the application Casper/FDR (Communication Sequential Process/Failure Divergence Refinement)tool,to verify the security of safety protocols. The main results are as follows:
(1)Introduce the conception of the security protocols and security protocols detection methods.
(2)Analyze the installation and use of Casper/FDR tool.
(3)Introduce the language and grammar for Casper.
(4)Use Casper / FDR tool to analyze NSPK protocol,and discover the flaw of protocol,then improve it（NSL） and get corresponding analysis results.
Keywords Security Protocol Safety Simulation Formal analysis method Model Checking Casper/FDR
目 次
1引言 1
1.1课题背景 1
1.2国内外研究现状及我的工作 1
1.3论文结构安排 2
1.4本章小结 2
2.安全协议及协议分析方法概述 3
2.1安全协议概述 3
2.1.1安全协议的基本概念 3
2.1.2安全协议分类 3
2.1.3常见的安全协议攻击 4
2.1.4设计安全协议的原则 4
2.2安全协议分析方法概述 5
2.2.1非形式化分析方法 5
2.2.2形式化分析方法 5
2.3常用模型检测工具概述 6
2.3.1 Casper/FDR工具 6
2.3.2 Murphi工具 6
2.3.3 SMV工具 7
2.3.4 NRL协议分析器 7
2.3.5 Interrogator工具 7
2.3.6 AVISPA工具 7
2.4本章小结 8
3. CASPER/FDR工具分析 9
3.1 CASPER/FDR工具简介 9