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

--if

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

--of if

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

--noexec

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

--typed | --untyped

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

--out file.atk

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

--nb max it nb

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

--short

寻找步数最短的攻击。

--ns

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