基于Spin的安全攻击仿真设计(2)
4.5 本章小结 29
结 论 30
致 谢 31
参考文献32
1 绪论
1.1 课题背景
随着社会及计算机技术的不断发展、飞速革新，人们的学习、生活等发生着日新月异的变化。随着程序规模的不断加大，系统亦越来越复杂，因此对安全协议的要求也就越来越高，潜在的细微错误都有可能引起灾难性的后果。如何从源头上解决这一问题，在设计时就能证明系统正确，在设计时就能发现潜在错误？模型检测技术正是这样一种自动化的验证技术。
1.2 模型检测的基本原理
模型检测[1](model checking)是一种十分重要的自动验证技术。它最早于1981年由Clarke和Emerson以及Quielle和Sifakis分别提出的。模型检测主要是通过显式状态搜索验证有穷状态、并发系统的模态以及命题性质的。虽然被限制在有穷系统上是它的缺点,但是模型检测可以应用于许多非常重要的系统。因此，一般情况下我们可以把模型检测和抽象、归纳原则等检测方法结合起来验证非有穷状态系统。
模型检测的基本思想[2]是用状态迁移系统表示系统的行为。设定期望的性质，系统是否具有所期望的性质？对存在争议的问题进行建模，于是问题就转化为用该模型是否具有所期望的性质。就有穷状态系统来看，这样的问题是可以被判定的，也就是说可以用程序在有限的时间内自动判断。
模型检测的分类有两套标准，如图1.1,1.2。
图1.1模型检测以技术分类
图1.2 模型检测以对象分类
1.3 模型检测器的工作原理
图1.3表示的是模型检测器的工作原理，从输出中可以看到模型检测器检测协议状态是否满足系统条件，有着自动化和提供反例等众多优点。
图1.3 模型检测器工作原理图
1.4 章节安排
本次课题是通过基于Spin进行安全攻击仿真的研究，总结分析出安全协议的相关概念，以及基于Spin进行安全攻击仿真的方法。并通过对NSPK协议的安全分析，达到熟练掌握使用Spin工具进行仿真的目的。根据本人的工作，本论文分四章，具体内容安排如下：
第一章：绪论。首先对课题背景进行概述，随后简要介绍了模型检测的基本原理以及模型检测器的工作原理，最后对本文的组织结构进行了说明，并进行章节小结。
第二章：理论背景。本章介绍了模型检测工具Spin，以及安全协议形式化分析方法的理论基础，并且对近来安全协议形式化分析用到的主要模型检测工具进行了简要介绍。
第三章：Spin工具分析。本章主要进行Spin的安装说明、安装过程中遇到问题的解决方法、Promela语言以及软件主界面的简要介绍。
第四章：协议安全攻击仿真的实现。本章通过Spin工具实现了对NSPK协议的安全仿真攻击，并对NSPK协议攻击漏洞进行分析。同时也进一步用实例说明了Spin工具的使用。
1.5 本章小结
首先对课题背景进行了概述，并对模型检测的基本原理及发展状况进行介绍，随后对模型检测器的基本原理进行介绍，最后对本文的组织结构进行了介绍。
2 安全协议及分析方法概述
2.1 安全协议概述
2.1.1 安全协议的基本概念
协议[3]即参与各方要遵守的规范和约定，是两个或者两个以上的参与者为完成某项特定任务而采取的一系列动作的集合。
协议的特点：每个协议中的实体必须了解该协议，并知道自己的职责；协议中的每个可信实体必须同意并遵循它；协议语意必须明确；协议必须对每种可能出现的情况都进行规定。