本文为A VISPA v1.1 User Manual.pdf阅读笔记
原文可关注“养两只猫”获取
A VISPA (Automated Validation of Internet Security Protocols and Applications) Internet安全协议和应用程序的自动验证
上文是个详细的AVISPA交互手册。分为两个部分,分别针对业余人员和专业人员。只记录我认为有用的信息。
在HLPSL中,所有变量都以大写字母开头,常量以小写字母开头;请注意,自然数也可以用作常量(没有任何特定的解释)。
在HLPSL规范中,注释和分隔符(例如“空白”,换行符和制表符)将被忽略:
HLPSL规范由三个部分组成:角色定义列表,目标声明列表(如果有)以及主要角色的实例化(读取调用)(通常不带参数)。
规范中的角色有两种:代理扮演的基本角色,以及描述在分析过程中要考虑的场景的组合角色(例如,描述什么是协议的会话或应使用的会话实例)。
一个角色可能包含许多声明:
•局部声明:声明变量及其类型;
•常量声明:声明其类型的常量不是角色的局部内容;一个角色中的任何常量都可以在另一角色中使用;
•初始化:局部变量的初始化;
•接受声明:可以认为角色已完成的条件;
•入侵者知识声明:在角色执行开始时提供给入侵者的一组信息。
常量声明。常量在角色中声明,但是是全局的。如果类型相同,则常量的多个声明不会引发错误。为了清楚起见,建议在主要角色(例如:环境)中声明所有常量。
入侵者知识仅在主要角色中定义(例如,环境)。
基本角色中的过渡既可以是自发动作,在左侧的状态谓词为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):与请求类似,但认证属性较弱。
创建角色的实例就像调用过程,为每个参数赋值。当然,参数的数量必须与形式参数的数量相同,并且每个参数的类型必须与相应形式参数的类型兼容。
个人理解,可以把这个语言想成python中的类的感觉。
定义role就是定义类
session就是实例化的过程
NSPK密钥服务器(NSPK-KS)
SUMMARY: “摘要”;它指示该协议是安全的,不安全的,或者分析结果是否定论
DETAILS: 第二部分将说明该协议在什么条件下被认为是安全的,或者已使用什么条件来发现攻击,或者最后说明了为什么分析尚无定论。
PROTOCOL:协议名称(已经转换为IF格式)
GOAL:分析的目标
BACKEND:后端使用名称
经过一些可能的评论和统计后,攻击的痕迹(如果有)以Alice&Bob表示法打印。
后面针对专业用户的部分比较难,可以作为参考资料需要时进行查阅。为了满足日常需要,无需进行研究。个人观点。
原创声明:本文系作者授权腾讯云开发者社区发表,未经许可,不得转载。
如有侵权,请联系 cloudcommunity@tencent.com 删除。
原创声明:本文系作者授权腾讯云开发者社区发表,未经许可,不得转载。
如有侵权,请联系 cloudcommunity@tencent.com 删除。