形式化分析工具AVISPA(三)学习User micro-manual of AVISPA
前言
hlpsl2if:将用HLPSL语言编写的规范转换为IF语言的低级规范的工具。cl-atse:用于分析安全属性的工具
1 Specifying a Protocol
以NSPK协议为例:
S为认证服务器,A想要认证B
A/B均通过S服务器获得对方的公钥。
A、B都知道S的公钥
1.1 指明消息
一条信息是由若干信息组合而成的。
基本信息是:
- 参与者(类型agent)
- nonce(类型text)
- 对称密钥(类型symmetric_key)
- 公钥(类型public_key)
- 哈希函数(类型hash_func)
- 数字(类型nat)
- 布尔值(类型bool,常量true和false)
- 标签(类型 protocol_id)
- 通信通道(type channel(dy))
函数形式:
- 串联:A.PKa A后面跟着PKa
- 加密:{M}-{K} 由K加密的M
- 哈希函数:H(M)
常量:constants 变量:variables 旧值:X 新值:X‘
1.2 参与者的角色
role
role-name(typed-parameters)
played_by
player
def=
local
`declaration-of-local-variables`
const
`declaration-of-constants`
init
`initialization-of-variables`
transition
`list-of-transitions`
end role
variable [, variable]*:type [, variable [, variable]*:type]*
constant [, constant]*:type [, constant [, constant]*:type]*
variable := expression [/ variable := expression]*
label. condition [/ condition]* =|> aaction [/ action]*
例(复现图1第一步):
role
服务器角色:由S扮演。包含(参与者:类型,公钥:类型,设定的参数,两个信道参数(一个用于发送消息(Snd)和一个用于接收消息(Rcv)):类型)
参与者类型为:agent,公钥类型为:public_key,信道类型为:channel(dy)
local
此角色需要本地变量:两个代理名称(X, Y)和一个公钥(PKy)。
transition
标签:req1
触发条件:接收由两个代理名称组成的消息,并在其集合KeyMap中拥有第二个代理的公钥。(KeyMap的书写格式与前面一致)
执行:发送消息(Snd)由代理的名称及其公钥{Y, PKy}组成,所有这些都由服务器私钥加密。(参考:加密:{M}-{K} 由K加密的M)
注:
- 变量之间用“,”隔开
- 变量与类型之间用“:”号
- 类型参考:1.1 指明消息
- 与下一个变量之间与使用“,”
- 在transition中,条件与条件、动作与动作之间用 “ / ” 联接。满足某个条件,执行某个动作用 " =|> "
transition:
condition:
- 比较:
expression = expression
- 接收消息:
Rcv(message)
- 测试元素是否在集合中:
in(element,set) not (in(element,set))
action
- 赋值:
variable' := expression
- 创建一个新的信息:
variable' := new()
- 发送信息:
Snd(message)
- 添加元素至集合:
set' := cons(element,set)
例:(复现图1第二步)定义了B的属性及动作
witness/request/secret等语法参照1.5
1.3 协议会话
当参与者的角色被定义时,我们必须描述如何将它们组合到一个特定的角色中,从而构建协议的会话。
对于示例NSPK密钥服务器,此角色由以下定义:
在本例中,会话是角色alice和角色bob的组合。角色服务器未在此级别运行,因为它对协议的所有会话都是公用的。
1.4 环境和场景描述
协议被完全指定后,我们仍然需要定义分析该协议的环境(包括入侵者的初始知识),以及要执行的场景,即并行运行的会话实例。因此,作为参数传输到角色的信息是常量(除了通信信道)。
对于示例NSPK密钥服务器,环境可以用以下方式描述:
入侵者有一个预先定义的名称(i),它的初始知识是代理的名称、这些代理的公钥以及自己的一对公钥(pki)和私钥(inv(pki))。
所描述的场景是由一个包含三个会话的服务器组成:第一个会话中的玩家是a和b,第二个会话中的玩家是a和入侵者,第三个会话中的玩家是入侵者和b。
1.5 声明安全属性
必须在名为goal的部分中描述安全属性。如果未定义属性,则此部分不必存在。安全属性分为三类:
-
信息的机密性:
通过关键字
security of
完成声明,后跟一个常量标识符;此标识符用于生成信息(或第一次通信)的角色中,使用谓词secret
语法如下:secret(information,identifier,agents-set)
其中agents set是允许知道信息的agent集合 -
强身份认证
代理Y对代理X进行强身份验证以获取某些信息:声明是通过关键字
authentication_on
完成的,后跟常量标识符;此标识符用于与身份验证相关的角色; 首先,在经过身份验证的代理X的角色中,在谓词witness
使用以下语法:witness(X,Y,identifier,information)
第二,在执行身份验证的代理Y的角色中,在谓词request
中使用以下语法:request(Y,X,identifier,information)
这种身份验证的原理是,当发出request时,必须已经为相同的信息发出了相应的witness。 -
弱身份认证
与强身份认证类同。声明关键字:
weak_authentication_on
。用到的谓词为weak
与wrequest
例:NSPK协议的安全属性声明:
1.6 执行场景
environment()
相关代码可以关注公号:养两只猫。发送NSPK获取。
下节内容将从以下方面继续进行。
2 工具使用
2.1 hlps12if
2.2 cl-atse
- JavaScript 教程
- JavaScript 编辑工具
- JavaScript 与HTML
- JavaScript 与Java
- JavaScript 数据结构
- JavaScript 基本数据类型
- JavaScript 特殊数据类型
- JavaScript 运算符
- JavaScript typeof 运算符
- JavaScript 表达式
- JavaScript 类型转换
- JavaScript 基本语法
- JavaScript 注释
- Javascript 基本处理流程
- Javascript 选择结构
- Javascript if 语句
- Javascript if 语句的嵌套
- Javascript switch 语句
- Javascript 循环结构
- Javascript 循环结构实例
- Javascript 跳转语句
- Javascript 控制语句总结
- Javascript 函数介绍
- Javascript 函数的定义
- Javascript 函数调用
- Javascript 几种特殊的函数
- JavaScript 内置函数简介
- Javascript eval() 函数
- Javascript isFinite() 函数
- Javascript isNaN() 函数
- parseInt() 与 parseFloat()
- escape() 与 unescape()
- Javascript 字符串介绍
- Javascript length属性
- javascript 字符串函数
- Javascript 日期对象简介
- Javascript 日期对象用途
- Date 对象属性和方法
- Javascript 数组是什么
- Javascript 创建数组
- Javascript 数组赋值与取值
- Javascript 数组属性和方法
- Linux内核虚拟内存管理之匿名映射缺页异常分析
- Elasticsearch:如何把 Elasticsearch 中的数据导出为 CSV 格式的文件
- Nginx 负载均衡配置(实战教程)
- 教懂你什么是 “ 流量劫持 ”
- SAP Spartacus中使用到的Angular ModuleWithProviders类型
- 架构设计 | 基于消息中间件,图解柔性事务一致性
- 结构与算法(02):队列和栈结构
- 用Gaussian寻找圆锥交叉点
- kubernetes用户安全管理模型简析
- Unity3D网络通讯(一)--Asp.Net Core WebApi创建发布注意事项
- Unity3D网络通讯(二)--UnityWebRequest及JsonUtility请求Http Restful
- CS学习笔记 | 20、通过Socks转发的方法
- 构建的抽象
- 低成本个人建站系列二 —— 使用 Hexo+GitHub 搭建个人免费博客
- 42图揭秘,「后端技术学些啥」