原创

形式化分析工具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

原创声明,本文系作者授权云+社区发表,未经许可,不得转载。

如有侵权,请联系 yunjia_community@tencent.com 删除。

我来说两句

0 条评论
登录 后参与评论

相关文章

  • 形式化分析工具(六):HLPSL Tutorial

    本文为阅读笔记。文章题目为: HLPSL Tutorial A Beginner’s Guide to Modelling and Analysing Inte...

    春风大魔王
  • 形式化分析工具AVISPA(四) SPAN工具简要介绍

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

    春风大魔王
  • SPAN: a Security Protocol ANimator for A VISPA

    Protocol Simulation:模拟协议并建立对应于HLPSL规范的特定MSC(Message Sequence Charts,消息序列图);

    春风大魔王
  • 算法训练 K好数

    问题描述 如果一个自然数N的K进制表示中任意的相邻的两位都不是相邻的数字,那么我们就说这个数是K好数。求L位K进制数中K好数的数目。例如K = 4,L = ...

    AI那点小事
  • 转载 | 利用动态规划求解旅行商问题(Travelling Salesman Problem)时空复杂度分析以及相关实验验证

    利用动态规划求解旅行商问题(Travelling Salesman Problem,简称TSP)在之前的推文中已经有了详细的介绍,今天我们要对这个问题进行更深一...

    短短的路走走停停
  • 利用动态规划求解旅行商问题时空复杂度分析以及相关实验验证

    利用动态规划求解旅行商问题(Travelling Salesman Problem,简称TSP)在之前的推文中已经有了详细的介绍,今天我们要对这个问...

    用户1621951
  • 2-AI--Activity启动方式

    张风捷特烈
  • 浙江工业大学校赛 小M和天平

    小M和天平 Time Limit: 2000/1000 MS (Java/Others)    Memory Limit: 32768/32768 K (Ja...

    ShenduCC
  • hanlp在Python环境中的安装失败后的解决方法

    Hanlp是由一系列模型与算法组成的javag工具包,目标是普及自然语言处理再生环境中的应用。有很多人在安装hanlp的时候会遇到安装失败的情况,下面就是某大神...

    IT小白龙
  • 循环比赛日程表

    w【问题描述】 w    设有N个选手进行循环比赛,其中N=2M,要求每名选手要与其他N-1名选手都赛一次,每名选手每天比赛一次,循环赛共进行N-1天,要求每天...

    attack

扫码关注云+社区

领取腾讯云代金券