专栏首页认证协议的形式化分析形式化分析工具(七)AVISPA v1.1 User Manual
原创

形式化分析工具(七)AVISPA v1.1 User Manual

本文为A VISPA v1.1 User Manual.pdf阅读笔记

原文可关注“养两只猫”获取

A VISPA (Automated Validation of Internet Security Protocols and Applications) Internet安全协议和应用程序的自动验证

上文是个详细的AVISPA交互手册。分为两个部分,分别针对业余人员和专业人员。只记录我认为有用的信息。

HLPSL语法

a. Lexical entities.

在HLPSL中,所有变量都以大写字母开头,常量以小写字母开头;请注意,自然数也可以用作常量(没有任何特定的解释)。

在HLPSL规范中,注释和分隔符(例如“空白”,换行符和制表符)将被忽略:

b. Structure of a HLPSL specification.

HLPSL规范由三个部分组成:角色定义列表,目标声明列表(如果有)以及主要角色的实例化(读取调用)(通常不带参数)。

c. Definition of roles.

规范中的角色有两种:代理扮演的基本角色,以及描述在分析过程中要考虑的场景的组合角色(例如,描述什么是协议的会话或应使用的会话实例)。

一个角色可能包含许多声明:

•局部声明:声明变量及其类型;

•常量声明:声明其类型的常量不是角色的局部内容;一个角色中的任何常量都可以在另一角色中使用;

•初始化:局部变量的初始化;

•接受声明:可以认为角色已完成的条件;

•入侵者知识声明:在角色执行开始时提供给入侵者的一组信息。

常量声明。常量在角色中声明,但是是全局的。如果类型相同,则常量的多个声明不会引发错误。为了清楚起见,建议在主要角色(例如:环境)中声明所有常量。

入侵者知识仅在主要角色中定义(例如,环境)。

l. Transitions in basic roles.

基本角色中的过渡既可以是自发动作,在左侧的状态谓词为true时启用,也可以在非停顿事件(即基于某些变量值变化的事件)发生时立即触发立即反应。左侧是正确的。

起始(start)消息用作发送给角色播放器的信号,用于要求其启动协议会话。

上面列出的四个预定义目标谓词包含以下信息:

•secret(E,id,S):将信息E声明为集合S的代理共享的秘密;这个秘密将由目标部分中的常数id标识; •witness(A,B,id,E):对于B在E上由B进行的A的(弱)身份验证属性,声明代理A为见证人用于信息E;该目标将由目标部分中的常量ID标识; •request(B,A,id,E):对于B在E上由A进行的强身份验证,声明代理B请求检查值E;该目标将由目标部分中的常量ID标识; •wrequest(B,A,id,E):与请求类似,但认证属性较弱。

o. Instantiation of a role.

创建角色的实例就像调用过程,为每个参数赋值。当然,参数的数量必须与形式参数的数量相同,并且每个参数的类型必须与相应形式参数的类型兼容。

个人理解,可以把这个语言想成python中的类的感觉。

定义role就是定义类

session就是实例化的过程

2.1.3 Example

NSPK密钥服务器(NSPK-KS)

相关资料查找位置

  1. 形式化分析工具SPAN里面后端的相关参考可以在P34页中查找!
  2. 虚拟机AVISPA PACKAGE / bin / backends /目录中的cl.bash,ofmc.bash,satmc.bash和ta4sp.bash文件中都有详细说明。
  3. HLPSL规范问题:给出了日志文件的名称(通常在$ AVISPA_PACKAGE / logs目录中);该文件包含有关位置和错误原因的信息;

分析结果及输出:

SUMMARY: “摘要”;它指示该协议是安全的,不安全的,或者分析结果是否定论

DETAILS: 第二部分将说明该协议在什么条件下被认为是安全的,或者已使用什么条件来发现攻击,或者最后说明了为什么分析尚无定论。

PROTOCOL:协议名称(已经转换为IF格式)

GOAL:分析的目标

BACKEND:后端使用名称

经过一些可能的评论和统计后,攻击的痕迹(如果有)以Alice&Bob表示法打印。

后面针对专业用户的部分比较难,可以作为参考资料需要时进行查阅。为了满足日常需要,无需进行研究。个人观点。

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

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

我来说两句

0 条评论
登录 后参与评论

相关文章

  • SPAN: a Security Protocol ANimator for A VISPA

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

    春风大魔王
  • 形式化分析工具(六):HLPSL Tutorial

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

    春风大魔王
  • 形式化分析工具AVISPA(二):使用及教程资料

    参考资料:https://blog.csdn.net/pan_tian/article/details/22619687

    春风大魔王
  • docker入门笔记-images和container创建

    后面的多个命令中会用到container的id,所以先介绍一下查看container id的方法:

    marsggbo
  • spring/springboot的整合分布式配置中心(ACM diamond nacos Apollo)

    代码下载:https://gitee.com/hong99/spring/issues/I1N1DF

    逍遥壮士
  • 新数据时代:“黑马”浪潮存储的飞轮

    一个巨大的飞轮,要想把它转动起来,实现的难度可谓空前。你只有每一次推动都用尽全力,顺着同一个方向转动,刚开始可能会非常慢,随着时间的推移,每一次努力的积累,一旦...

    大数据在线
  • 综合开源靶场搭建

    Vulfocus是一个漏洞集成平台,可以通过平台添加多种类型的漏洞靶场,操作简单,易学易用。接下来小编将带领大家一同搭建一个简单的测试靶场环境。

    贝塔安全实验室
  • Python中最常见的五种算法,你确定你都会了吗?

    在我们平常编写程序时,算法的使用是必不可少的,今天就来挑五种最常见的算法分享给大家!

    双面人
  • java9系列(八)Multi-Release JAR Files

    java9新支持了multi-release jar的功能,包括jar、javac、javap、jdeps等命令都能支持这个特性。所谓multi-release...

    codecraft
  • GitHub修改昵称和用户名(图解详细教程)

    4.要想修改登录名,要选择Account下的Change username,也就是修改用户名。

    bboy枫亭

扫码关注云+社区

领取腾讯云代金券