形式化分析工具AVISPA(三)2.学习User micro-manual of AVISPA
时间:2022-07-22
本文章向大家介绍形式化分析工具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 |
默认情况下,攻击的跟踪可能会简化,某些步骤可能会丢失;此选项允许避免这种情况并显示完整的跟踪。 |
- JavaScript 教程
- JavaScript 编辑工具
- JavaScript 与HTML
- JavaScript 与Java
- JavaScript 数据结构
- JavaScript 基本数据类型
- JavaScript 特殊数据类型
- JavaScript 运算符
- JavaScript typeof 运算符
- JavaScript 表达式
- JavaScript 类型转换
- JavaScript 基本语法
- JavaScript 注释
- Javascript 基本处理流程
- Javascript 选择结构
- Javascript if 语句
- Javascript if 语句的嵌套
- Javascript switch 语句
- Javascript 循环结构
- Javascript 循环结构实例
- Javascript 跳转语句
- Javascript 控制语句总结
- Javascript 函数介绍
- Javascript 函数的定义
- Javascript 函数调用
- Javascript 几种特殊的函数
- JavaScript 内置函数简介
- Javascript eval() 函数
- Javascript isFinite() 函数
- Javascript isNaN() 函数
- parseInt() 与 parseFloat()
- escape() 与 unescape()
- Javascript 字符串介绍
- Javascript length属性
- javascript 字符串函数
- Javascript 日期对象简介
- Javascript 日期对象用途
- Date 对象属性和方法
- Javascript 数组是什么
- Javascript 创建数组
- Javascript 数组赋值与取值
- Javascript 数组属性和方法
- AkShare-中国宏观-央行货币当局资产负债
- AkShare-中国宏观-FR007利率互换曲线
- Github标星59.7k:用动画的形式呈现解LeetCode题目的思路
- 《爱情公寓》电影版,十年一瞬间(下)
- 实战:上亿数据如何秒查
- 《爱情公寓》电影版,十年一瞬间(上)
- Ajax爬取今日头条街拍美图
- 现在的房租有多高(杭州)?
- 英雄联盟皮肤大拼图
- Python爬虫-MongoDB
- Python爬虫-selenium
- 用Python识别图形验证码,实现自动登陆!
- 当Docker遇到Intellij IDEA,再次解放了生产力~
- 用Python爬取自主品牌汽车,看看国产汽车究竟长什么样?(上)
- 工具包 | 使用Python绘制Sci学术期刊配图