基于Spin的安全攻击仿真设计(3)
安全协议[4]，亦可称作密码协议，是以密码学为基础的消息交换协议，它的目的是在网络环境中提供各种满足完整性、私密性、认证性、不可否认性的安全服务。
2.1.2 安全协议分类
安全协议的分类方式有很多，此处根据协议完成的功能进行划分，可以分成4类：
1. 密钥交换协议（Key Exchange Protocol）
密钥交换协议用于会话秘钥的建立，通常在该协议中的实体之间建立单次会话秘钥。这类协议需要一个可信第三方来产生会话秘钥，类似于服务器的功能，协议中可以采用公钥密码体质，亦可以采用私钥密码体制。
2. 认证协议（Authentication Protocol）
认证协议包括信息认证协议、身份认证协议、数据源认证协议和数据目的地认证协议等。这类协议一般通过实体所拥有的一些特征来识别身份，可用来防止假冒、篡改等攻击。
3. 认证密钥交换协议（Authenticated Key Exchange Protocol）
认证密钥交换协议是目前网络中使用使用最广泛的安全协议。它是将认证协议与交换密钥协议组合在一起产生的。协议首先对通信的主体进行身份认证，身份认证成功后进一步分配通信所需要的会话秘钥。
4.电子商务协议（Electronic Commerce Protocol）
由于协议的参与实体代表了交易的双方，因此公平性方面比一般协议考虑得多，也就是说不允许运行损人利己的事件。电子商务协议中还包括有原子性、匿名性、不可否认性等安全属性。
2.2 安全协议分析方法概述
迄今为止对安全协议的分析方法主要分为两种[6]，一种是非形式化分析方法，另一种是形式化分析方法。
2.2.1 非形式化分析方法
非形式化分析方法[7]也被称为攻击检验分析方法，是早期对安全协议的主要分析方法。这种方法就是使用各种已知的攻击方法对协议进行攻击，再查看攻击结果来分析协议的安全性。但在实际中已知的攻击方法通常会被高级的入侵者所避免，等再发现时或许已造成不可预估的损失，因此目前较少使用。
2.2.2 形式化分析方法
形式化方法[8]通过使用数学和逻辑方法对协议进行描述以及验证，其核心是为安全协议建立形式化模型，并探索其中是否存在不安全状态。
安全协议形式化分析方法通常分成三类：模态逻辑方法、模型检测方法与定理证明方法。
1.模态逻辑方法
模态逻辑方法[9]是迄今为止应用范围最为广泛的一种形式化分析方法，最具代表性的是BAN逻辑。其能够通过简单清晰的定义快速发现协议中的安全漏洞。通常BAN逻辑理想化过程将会使部分数据泄露、被修改或被伪造，因而使协议本身的安全性受到威胁。
2.模型检测方法
模型检测方法[10]又被称为状态空间搜索方法。基本思路为模拟一个相对大但有限的空间，设定最初状态，不限定攻击路径，检测其是否能够到达指定结点，以检测协议是否安全。由于模型检测方法假设的空间是有限的，所以只能限制协议中的主体数目，因此难以达到预期效果。因此这种方法难以证明协议正确与否。
3.定理证明方法
定理证明方法从用户接收和发送的信息出发，考虑所有可能的协议行为，通过一系列的推理证明它们是否满足一定的安全条件，该过程需要人为参与，难以自动化，在如今这样的信息社会中不再适用。
2.3 常用的模型检测工具
模型检测（Model Checking）[10]是一种用于验证有限状态并发系统的自动化技术。该技术已被用于软件分析和通信协议模拟等领域，到目前为止，已发展成对安全协议分析的重要方法。其基本思想是验证所希望的性质是否满足所建立的模型，如果不满足，则给出反例路径。模型检测对协议进行分析时需要借助自动化分析工具，例如Spin、Casper/FDR、AVISPA工具集等。下面简要介绍Casper/FDR以及AVISPA工具集。