使用avispa进行nspk协议安全性分析

《使用avispa进行nspk协议安全性分析》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、基于AVISPA工具进行NSPK协议分析―、AVISPA工具介绍AVISPA分析工具的结构图如图1所示。HLPSL是一种丰富的、模块化的、基于角色的形式语言，提供了一套包括控制流模式、数据结构、可选择入侵者模式、复杂的安全目标以及不同的密码初始值和代数性质的说明。这些特性能够使HLPSL很好的描述现代的、工业化规模的协议。而且，HLPSL不仅支持基于时间片段的逻辑行为的公开语义，还支持基于重写的中间形式化语言IF。HLPSL2IF自动将HLPSL语言翻译成IF语言，并将它们依次反馈给测试后端。AVISPA使用了4种后端分析工具來解

2、决安企协议的确认问题：(1)OFMC(On-the-flyModel-Checker)：基于IF语言需求驱使的描述，通过探测系统的变迁，OFMC能够完成协议的篡改和有限制的确认。OFMC支持密码操作的代数性质的规范，以及各种协议模型。(2)CL-AtSe(Constraint-Logic-basedAttackSearcher)：CL-AtSe通过强大的简化探测法和冗余排除技术來执行协议。它建立在模型化的方式上，并且是对密码操作的代数性质的延伸。CL-AtSe支持输入缺陷探测和处理消息串联。(3)SATMC(SAT-basedMo

3、del-Checker)：SATMC建立在通过IF语言描述的，有限域上变迁关系的编码的公式，初始状态和状态集合的说明代表了整个协议的安全特性。此公式将反馈给SAT状态推导机，并且建立的任何一个模型都将转化为一个攻击事件。(4)TA4SP(TreeAutomatabasedonAutomaticApproximationsfortheAnalysisofSecurityProtocols):TA4SP通过树形语言和重写机制估计入侵者的知识。根据不同的保密特性,TA4SP能够判断一个协议是否有缺陷，或者是儿个会合的对话后是否安全。1▼

4、T▼~1▼1▼OFMC分W终姝CL-AtSc分桁终维SATMC分析终播TA4SP分析终播11111_111阁1AVISPA工具结构二、AVISPA工具安装AVISPA工具在AVISPA官方网站上可以下载，运行在Linux操作系统环境下。首先,下载并安装AVISPAvl.l版本(本文使用AVISPA1.0版本为例)，解压安装包到对应目录：其次，需要设置工具集的环境变量，将AV1SPA_PACKAGE关联到安装包的绝对路径；最后将avispa脚本语言设置在命令行解释器的执行H录中。例如：用户想安装AVISPA工具集在/opt路径下，命

5、令如下［51:cd/opttar-xzf/home/xyz/avispa-package-X.Y_Linux-i686.tgzexportAVISPA_PACKAGE=/opt/avispa-X.YexportPATH=$PATH:$AVISPA_PACKAGE三、XEmacs模式的使用(1)XEmacs工具的安装。AVISPA提供和XEmacs工具的用户友好接门(XEmacs工具是Linux操作系统下的一种编辑器)，它们之间支持川户和AVISPA工具集之间的简单交互。首先，Linux操作系统需要安装XEmacs编辑器；其次，需要

6、对AVISPA进行没置，使其支持XEmacs模式，命令如下：cd/opt/otherstar-xzvfavispa-mode.tgzcdtemporary-avispamakeinstall(2)XEmacs工具按钮。AVISPAXEmacs模式提供了一套完整而直观的编译环境对安全协议进行说明和分析。最常用的分析山发点是通过hlpsl文件开始。在AVISPA模式下，当XEmacs工具自动侦测出后缀名为“.hlpsl”的文件时，会在XEmacs工具栏上出现对应的AVISPA按钮。AVISPA按钮的大致功能如下：AVISPA：提供选项

7、、模式的定制和改变后端分析工具等功能；《和＞〉:提供在同一个协议不同的分析文件(例如“.if”，“.atk”等)之间进行导航;Processfile：导入编译器对中间文件进行编译和分析，得出结论；Update:当一个工具被XEmacs异步导入时，一旦此工具被巾断，此按钮将刷新当前的缓存区。NSPK协议分析(1)NSPK协议简介非对称密码体制NSPK协议，协议双方身份认证部分为：1)A—B：{N：,A}KA首先生成临时值M,加上自己的身份，用B的公开密钥KB加密后发送给B。2)B—A：(N：,N6}K.B生成临时值N6,加上A的临吋

8、值Nn,用A的公开密钥KA加密后发送给A。3)A—B：{M}KoAIMB发送经过KB加密的Nj.整个协议采用公幵密钥系统，K4,K8分别是A和B的公开密钥.N口，N6是A和B发布的具有新鲜性的临时值(nonce)。(2)NSPK分析实验使川AVIS