基于Spin的安全攻击仿真设计
本文主要应用SPIN（Simple Promela Interpreter）工具，来验证安全协议的安全性。主要的研究成果如下：
（1） 介绍了对安全协议和安全协议检测方法的概念
（2） 分析了Spin工具的安装使用
（3） 研究并分析了Spin语言及语法
（4） 利用Spin工具研究NSPK（Needham-Schroeder Public-Key Protocol）协议的安全性，并对发现的攻击漏洞进行分析，得到改进方案。
关键词 安全协议 安全攻击仿真 模型检测 Spin
毕业论文设计说明书外文摘要
Title Security attack simulation based on Spin
Abstract
Along with the development of computer networks, network technology has brought us a lot of convenience,but enjoying the convenience that network brings to us, network security issues will become increasingly prominent attendant. Network security situation is increasingly grim. Among these problems, information security is a top priority. Therefore security analysis of security protocols also has become very important. This paper studies on the application of Spin (Simple Promela Interpreter) tool, to verify the secure of safety protocols. The main results are as follows:
(1)Introduce the conception of the security protocols and the detection of security protocols.
(2)Analyze the installation and use of Spin tool.
(3)Introduce the language and grammar for Spin.
(4)Use Spin tool to analyze NSPK protocol, and discover the flaw of protocol, get corresponding analysis results.
Keywords Security Protocol Safety Simulation Model Checking Spin
目 次
1 绪论 1
1.1 课题背景 1
1.2 模型检测的基本原理 1
1.3 模型检测器的工作原理 2
1.4 章节安排 2
1.5 本章小结 3
2 安全协议及分析方法概述 4
2.1 安全协议概述 4
2.1.1 安全协议的基本概念 4
2.1.2 安全协议分类 4
2.2 安全协议分析方法概述 5
2.2.1 非形式化分析方法 5
2.2.2 形式化分析方法 5
2.3 常用的模型检测工具 5
2.3.1 Casper/FDR工具 6
2.3.2 AVISPA工具 6
2.4 本章小结 6
3 SPIN工具分析 7
3.1 Spin工具简介 7
3.2 Promela语言 8
3.2.1 Promela语法简介 9
3.2.2 Promela语言的具体使用 11
3.3 Spin安装 13
3.3.1 安装Cygwin 13
3.3.2 在Cygwin中安装yacc和SPIN 17
3.3.3 安装SPIN 的图形界面工具ispin 18
3.4 iSpin界面介绍 20
3.5互斥协议仿真结果 21
3.6 本章小结 23
4 协议安全攻击仿真的实现 24
4.1 协议步骤 24
4.2 协议的Spin语言表示 25
4.3 安全仿真攻击结果分析 26
4.4 漏洞分析 28