形式化分析工具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 文件。这将允许分别分析每个安全属性。

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

工具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	默认情况下，攻击的跟踪可能会简化，某些步骤可能会丢失；此选项允许避免这种情况并显示完整的跟踪。