前往小程序,Get更优阅读体验!
立即前往
首页
学习
活动
专区
工具
TVP
发布
社区首页 >专栏 >形式化分析工具AVISPA(三)2.学习User micro-manual of AVISPA

形式化分析工具AVISPA(三)2.学习User micro-manual of AVISPA

原创
作者头像
春风大魔王
修改2020-07-20 10:18:56
1K0
修改2020-07-20 10:18:56
举报
文章被收录于专栏:认证协议的形式化分析

工具:

1.hlpsl2if

工具hlpsl2if编译扩展名为.hlpsl的文件中作为参数给定的协议的规范,并列出规范中发现的错误,或者生成一个名称相同但扩展名为 .if 的文件,该文件将在以后分析。

hlpsl2if [option] file.hlpsl

唯一有用的选项是--split。它允许为目标部分中指定的每个安全属性生成不同的 .IF 文件。这将允许分别分析每个安全属性。

请注意,此编译器无法找到规范中的所有错误,特别是一些必须使用分析工具检测到的语义错误。

2.cl-atse

工具cl-atse在IF文件给定的协议场景中查找攻击。如果没有发现攻击,这并不意味着安全属性总是有保证的,而只是在给定的场景中它们是有保证的。

cl-atse [options] file.if

可用的options

options

描述

--if

强制性的,意味着给定的文件是IF格式的规范。

--of if

推荐,表示显示器必须与IF格式兼容。

--noexec

不运行安全属性分析,但按理解显示执行方案;此选项对于识别语义错误非常有用,例如使用从未 初始化过的变量(由常量伪变量表示…),或使用变量的旧值而不是其新值(符号在HLPSL规范中 被遗忘)。

--typed | --untyped

允许精确分析是否在类型化模式(默认情况下)下执行;非类型化模式有时有助于根据类型的混淆查 找更多的攻击。

--out file.atk

在给定文件中保存找到的攻击(如果有)的跟踪。

--nb max it nb

如果规范允许应用多次相同的转换,默认情况下,此迭代次数限制为3次;此选项允许修改此最大迭 代次数。

--short

寻找步数最短的攻击。

--ns

默认情况下,攻击的跟踪可能会简化,某些步骤可能会丢失;此选项允许避免这种情况并显示完整的跟踪。

原创声明:本文系作者授权腾讯云开发者社区发表,未经许可,不得转载。

如有侵权,请联系 cloudcommunity@tencent.com 删除。

原创声明:本文系作者授权腾讯云开发者社区发表,未经许可,不得转载。

如有侵权,请联系 cloudcommunity@tencent.com 删除。

评论
登录后参与评论
0 条评论
热度
最新
推荐阅读
目录
  • 1.hlpsl2if
  • 2.cl-atse
领券
问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档