毕业论文

打赏
当前位置: 毕业论文 > 计算机论文 >

基于Spin的安全攻击仿真设计(3)

时间:2018-07-08 16:38来源:毕业论文
安全协议[4],亦可称作密码协议,是以密码学为基础的消息交换协议,它的目的是在网络环境中提供各种满足完整性、私密性、认证性、不可否认性的安全


    安全协议[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工具集。 基于Spin的安全攻击仿真设计(3):http://www.751com.cn/jisuanji/lunwen_19221.html
------分隔线----------------------------
推荐内容