形式化分析工具AVISPA（四） SPAN工具简要介绍

参考：

参考资料：https://hal.inria.fr/hal-01213074v5

有多个版本的。也可关注公号：养两只猫。发送 “VISPA教程” 获取

安装增强功能

之前在安装增强功能时，有的小伙伴可能遇到需要密码的情况 ，密码为span

安装流程如下：

1. 点击设备，安装增强功能。会在桌面产生VBox_GAs这个文件。
2. 点开文件，点击右上角 open autorun prompt，下一步
3. 输入密码：span

1.点击设备，安装增强功能。会在桌面产生VBox_GAs这个文件。

前提：SPAN AVISPA教程

1. 按照前面的教程进行安装
2. 安装包和教程通过前面教程获取
3. 建议参照A Short SPAN A VISPA Tutorial.PDF 自己独立进行操作会有一个直观的体验和印象

SPAN工具简要介绍

1.点击桌面SPAN图标，主界面如下图。

完整的SPAN主图形界面

1.打开或者保存 HLPSL或者CAS 规范的文件

2.OFMC、ATSE、SATMC、TA4SP是四种证明工具

3.protocol、intruder、attack simulation是三种模拟形式。分别是协协议仿真、入侵者仿真、攻击仿真

2.三种仿真模式演示

2.1 protocol simulation

protocol simulation

modes选项

modes选项1

modes选项2

variables monitoring

变量监控1

变量监控2

2.2 intruder simulation

入侵者仿真

2.3 attack simulation

与intruder simulation雷同

总结：

1.modes选 sender pattern 这个选项，看起来相对直观、一致。如下图

2.通过查看intruder knowledge,可以直观的发现哪些信息不安全。如下图的nonce-2等。

3.比较有序的操作流程（纯个人总结）

1. 先查看协议仿真（protocol simulation），改模式，查看是否能够完全复现所编写的协议。
2. 选择证明工具进行证明。（若不进行第一步检查，证明结果会直接显示安全。因为协议本身不完整，没有输入进来。）
3. 根据需要进行调试（根据哪些信息不安全进行，进行安全调试）