形式化分析工具AVISPA

在阅读论文的过程中发现了一个形式化分析工具（AVISPA）

现把使用过程记录如下：（重点记录遇到的问题）

一、有用的参考资料

1.(3条消息)AVISPA入门级教程_Summer Day-CSDN博客_avispa

2.(3条消息)AVISPA工具调研_Trust Bo-CSDN博客_avispa

3.(3条消息)AVISPA编译工具SPAN虚拟机的安装和简单使用教程_Summer Day-CSDN博客_span 工具

4.利用AVISPA证明D2D协议_Summer Day-CSDN博客_avispa时间戳

5.The AVISPA Project

二、安装使用

主要参考资料3，进行安装。

分为两部分：1.VirtualBox的安装。2.SPAN虚拟机的导入。

遇到问题一：虚拟机启动出故障

参考资料：(3条消息)Failed to instantiate CLSID_VirtualBox w/ IVirtualBox, but CLSID_VirtualBox w/ IUnknown works._kevin的博客-CSDN博客_failed to instantiate clsid_virtualbox w/ ivirtual

问题二：导入虚拟机出现问题。代码: E_INVALIDARG (0x80070057)

参考资料：https://www.cnblogs.com/pbblogs/p/10727429.html

但并没有用上。万能大法好（重装）我把第一次安装位置的虚拟机删了再重新装就没这个问题了。

原因自我推测应该是改路径的问题。

其它虚拟机导入问题方法：https://blog.csdn.net/mobileapps/article/details/4390084

问题三：不能为虚拟机打开一个新任务

解决方法：安装扩展包

通过安装“Oracle VM VirtualBox Extension Pack”扩展包解决问题

我们可以在VirtualBox官网的下载页面找到扩展包的下载方式，如图点击“All supported platforms”即可下载：

官网：https://www.virtualbox.org/wiki/Downloads

通过在VirtualBox中依次点击“管理->全局设定->扩展”，找到对应的扩展安装包，安装即可：

安装完成扩展包后，取消禁用USB控制器，之后开机，可以正常启动，问题解决。

红框显示已经正常启动了

其它问题可以参考：

https://blog.csdn.net/lijing198997/article/details/47027015