专栏首页认证协议的形式化分析形式化分析工具AVISPA(四) SPAN工具简要介绍
原创

形式化分析工具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. 根据需要进行调试(根据哪些信息不安全进行,进行安全调试)

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

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

我来说两句

0 条评论
登录 后参与评论

相关文章

  • SPAN+A VISPA for Verifying Cryptographic Protocols

    春风大魔王
  • 形式化分析工具:在虚拟操作系统和主机操作系统之间配置共享文件夹

    1. 在VirtualBox应用程序中,单击虚拟机名称,然后单击“配置”,然后单击“共享文件夹”,然后添加与主机OS上的路径关联的永久性虚拟共享文件夹。如图所示...

    春风大魔王
  • 形式化分析工具AVISPA

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

    春风大魔王
  • cvm跨可用区迁移

    前言:cvm无法直接迁移的,以下给出的方式是备份数据重新购买云主机,然后销毁原有的云主机。所以操作前首先要确认自己的云主机是可以退还的,并且认可退还金额的。

    cdc
  • Python里面这些点,据说80%的新手都会一脸懵逼

    Python虽然语法简单,通俗易懂,但是再简单它也是一门语言,就像一棵大树,总有一些树枝是弯弯绕绕的,让新手看完之后一脸懵逼,今天我们就来说说这几个点,反正我学...

    一墨编程学习
  • 在本地环境中开发微信公众号网页

    我司采取的是前后端分离的开发模式,后端技术栈陈旧,且无法根据前端开发需求变更服务器配置。一个生产环境的https域名,根目录访问403。后端技术栈.Net,后端...

    枫林带
  • DevOps概述

    持续集成:版本管理、自动构建、自动测试、集成到主线并构建、克隆生产环境的测试、所有人参与、自动部署

    用户5760343
  • iOS音视频接入-TRTC接入前期key、秘钥等准备

    在接入前我们可以先体验下腾讯为开发者提供的Demo(体验地址),体验之后我们就可以进行快速入门Demo试跑,在跑Demo之前我们必须确认以下信息:

    小明同学接音视频
  • 如何设计报表?

    报表就是报告状况的表,是通过表格、图表来展示指标,从而方便业务部门掌握业务的情况。

    猴子数据分析
  • Node.js基础

    达达前端

扫码关注云+社区

领取腾讯云代金券