参考：

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

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

安装增强功能

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

安装流程如下：

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

前提：SPAN+AVISPA教程

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

SPAN工具简要介绍

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

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

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

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

2.三种仿真模式演示

2.1 protocol simulation

modes选项

variables monitoring

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. 根据需要进行调试（根据哪些信息不安全进行，进行安全调试）