专栏首页认证协议的形式化分析形式化分析工具AVISPA(三)2.学习User micro-manual of AVISPA
原创

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

工具:

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

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

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

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

我来说两句

0 条评论
登录 后参与评论

相关文章

  • SPAN: a Security Protocol ANimator for A VISPA

    Protocol Simulation:模拟协议并建立对应于HLPSL规范的特定MSC(Message Sequence Charts,消息序列图);

    春风大魔王
  • SPAN+A VISPA for Verifying Cryptographic Protocols

    春风大魔王
  • 形式化分析工具(六):HLPSL Tutorial(Example 4,other)

    默认情况下,CL-AtSe打印的攻击痕迹可能不是最小的。实际上,这是CL-Atse的首次攻击。但是,可以使用-short选项要求CL-Atse输出最小的攻击之一...

    春风大魔王
  • php学习笔记之require()和include()

    include()在执行文件时每次都要进行读取和评估,如果每次执行代码时是读取不同的文件,或者通过一组文件迭代循环,就使用include();

    solate
  • 完美!Kubernetes 集群的零停机服务器更新

    来源 | https://vflong.github.io/sre/k8s/2020/02/16/zero-downtime-server-updates-fo...

    java进阶架构师
  • 配置tomcat限制指定IP地址访问后端应用

    1. 场景 后端存在N个tomcat实例,前端通过nginx反向代理和负载均衡。 tomcat1 tomcatN | ...

    2Simple
  • 谈喻凯:4.16比特币冲高回落 维持在5000关口拉锯

      调整何时都会出现,只要是金融市场,就不要期待会出现每日收盘价上涨的情况发生。关键的问题是,调整以什么级别出现。调整力度如何以及调整的时间怎样。BTC由熊市向...

    谈喻凯
  • 短视频软件开发结合美颜SDK打造短视频源码经典

    为什么短视频软件这么火呢?因为它符合了用户碎片化时间的需求,既娱乐了大众,又不会浪费用户太多时间。

    用户4551288
  • 音频工具分析实例

    AI之禅
  • ZooKeeper故障节点替换过程详解

    一、环境描述 我的生产环境ZooKeeper 版本3.4.6,5个节点组成的ZooKeeper集群。ZooKeeper集群为一套8个节点的Hadoop集群和HB...

    CSDN技术头条

扫码关注云+社区

领取腾讯云代金券