首页
学习
活动
专区
工具
TVP
发布
社区首页 >专栏 >形式化分析工具(七)AVISPA v1.1 User Manual

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

原创
作者头像
春风大魔王
修改2020-07-27 10:43:10
1.4K0
修改2020-07-27 10:43:10
举报

本文为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表示法打印。

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

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

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

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

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

评论
登录后参与评论
0 条评论
热度
最新
推荐阅读
目录
  • HLPSL语法
    • a. Lexical entities.
      • b. Structure of a HLPSL specification.
        • c. Definition of roles.
          • l. Transitions in basic roles.
            • o. Instantiation of a role.
              • 2.1.3 Example
              • 相关资料查找位置
                • 分析结果及输出:
                相关产品与服务
                多因子身份认证
                多因子身份认证(Multi-factor Authentication Service,MFAS)的目的是建立一个多层次的防御体系,通过结合两种或三种认证因子(基于记忆的/基于持有物的/基于生物特征的认证因子)验证访问者的身份,使系统或资源更加安全。攻击者即使破解单一因子(如口令、人脸),应用的安全依然可以得到保障。
                领券
                问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档