网站大量收购闲置独家精品文档,联系QQ:2885784924

使用AVISPA进行NSPK协议安全性分析.pdfVIP

  1. 1、本文档共11页,可阅读全部内容。
  2. 2、有哪些信誉好的足球投注网站(book118)网站文档一经付费(服务费),不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
  3. 3、本站所有内容均由合作方或网友上传,本站不对文档的完整性、权威性及其观点立场正确性做任何保证或承诺!文档内容仅供研究参考,付费前请自行鉴别。如您付费,意味着您自己接受本站规则且自行承担风险,本站不退款、不进行额外附加服务;查看《如何避免下载的几个坑》。如果您已付费下载过本站文档,您可以点击 这里二次下载
  4. 4、如文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“版权申诉”(推荐),也可以打举报电话:400-050-0827(电话支持时间:9:00-18:30)。
  5. 5、该文档为VIP文档,如果想要下载,成为VIP会员后,下载免费。
  6. 6、成为VIP后,下载本文档将扣除1次下载权益。下载后,不支持退款、换文档。如有疑问请联系我们
  7. 7、成为VIP后,您将拥有八大权益,权益包括:VIP文档下载权益、阅读免打扰、文档格式转换、高级专利检索、专属身份标志、高级客服、多端互通、版权登记。
  8. 8、VIP文档为合作方或网友上传,每下载1次, 网站将根据用户上传文档的质量评分、类型等,对文档贡献者给予高额补贴、流量扶持。如果你也想贡献VIP文档。上传文档
查看更多

基于AVISPA工具进行NSPK协议分析

一、AVISPA工具介绍

AVISPA分析工具的结构图如图1所示。HLPSL是一种丰富的、模块化的、基于角色

的形式语言,提供了一套包括控制流模式、数据结构、可选择入侵者模式、复杂的安全目标

以及不同的密码初始值和代数性质的说明。这些特性能够使HLPSL很好的描述现代的、工

业化规模的协议。而且,HLPSL不仅支持基于时间片段的逻辑行为的公开语义,还支持基

于重写的中间形式化语言IF。

HLPSL2IF自动将HLPSL语言翻译成IF语言,并将它们依次反馈给测试后端。AVISPA

使用了4种后端分析工具来解决安全协议的确认问题:

(1)OFMC(On-the-flyModel-Checker):基于IF语言需求驱使的描述,通过探测系统

的变迁,OFMC能够完成协议的篡改和有限制的确认。OFMC支持密码操作的代数性质的

规范,以及各种协议模型。

(2)CL-AtSe(Constraint-Logic-basedAttackSearcher):CL-AtSe通过强大的简化探测

法和冗余排除技术来执行协议。它建立在模型化的方式上,并且是对密码操作的代数性质的

延伸。CL-AtSe支持输入缺陷探测和处理消息串联。

(3)SATMC(SAT-basedModel-Checker):SATMC建立在通过IF语言描述的,有限

域上变迁关系的编码的公式,初始状态和状态集合的说明代表了整个协议的安全特性。此公

式将反馈给SAT状态推导机,并且建立的任何一个模型都将转化为一个攻击事件。

(4)TA4SP(TreeAutomatabasedonAutomaticApproximationsfortheAnalysisofSecurity

Protocols):TA4SP通过树形语言和重写机制估计入侵者的知识。根据不同的必威体育官网网址特性,TA4SP

能够判断一个协议是否有缺陷,或者是几个会合的对话后是否安全。

图1AVISPA工具结构

二、AVISPA工具安装

1

AVISPA工具在AVISPA官方网站上可以下载,运行在Linux操作系统环境下。首先,

下载并安装AVISPAv1.1版本(本文使用AVISPA1.0版本为例),解压安装包到对应目

录;其次,需要设置工具集的环境变量,将

AVISPA_PACKAGE关联到安装包的绝对路径;最后将

avispa脚本语言设置在命令行解释器的执行目录中。例如:

用户想安装AVISPA工具集在/opt路径下,命令如下[5]:

cd/opt

tar-xzf/home/xyz/avispa-package-X.Y_Linux-i686.tgz

exportAVISPA_PACKAGE=/opt/avispa-X.Y

exportPATH=$PATH:$AVISPA_PACKAGE

三、XEmacs模式的使用

(1)XEmacs工具的安装。

AVISPA提供和XEmacs工具的用户友好接口(XEmacs工具是Linux操作系统下的一

种编辑器),它们之间支持用户和AVISPA工具集之间的简单交互。首先,Linux操作系统

需要安装XEmacs编辑器;其次,需要对AVISPA进行设置,使其支持XEmacs模式,命

令如下:

cd/opt/others

tar-xzvfavispa-mode.tgz

cdtemporary-avispa

makeinstall

(2)XEmacs工具按钮。

AVISPAXEmacs模式提供了一套完整而直观的编译环境对安全协议进行说明和

文档评论(0)

186****5732 + 关注
实名认证
文档贡献者

该用户很懒,什么也没介绍

1亿VIP精品文档

相关文档