形式化分析工具AVISPA（三）学习User micro-manual of AVISPA

前言

hlpsl2if：将用HLPSL语言编写的规范转换为IF语言的低级规范的工具。cl-atse：用于分析安全属性的工具

1 Specifying a Protocol

以NSPK协议为例：

S为认证服务器，A想要认证B

图1：PKx:x的公钥。Nx：X协议过程中产生的一个临时数。inv（PKx）：对应的私钥

A/B均通过S服务器获得对方的公钥。

A、B都知道S的公钥

1.1 指明消息

一条信息是由若干信息组合而成的。

基本信息是：

1. 参与者（类型agent）
2. nonce（类型text）
3. 对称密钥（类型symmetric_key）
4. 公钥（类型public_key）
5. 哈希函数（类型hash_func）
6. 数字（类型nat）
7. 布尔值（类型bool，常量true和false）
8. 标签（类型 protocol_id）
9. 通信通道（type channel（dy））

函数形式：

1. 串联：A.PKa A后面跟着PKa
2. 加密：{M}-{K} 由K加密的M
3. 哈希函数：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

精细语法表述（1）

精细语法表述（2）

variable [, variable]*:type [, variable [, variable]*:type]*

constant [, constant]*:type [, constant [, constant]*:type]*

variable := expression [/\ variable := expression]*

label. condition [/\ condition]* =|> aaction [/\ action]*

例（复现图1第一步）：

定义服务器S的属性及动作

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. 变量之间用“，”隔开
2. 变量与类型之间用“：”号
3. 类型参考：1.1 指明消息
4. 与下一个变量之间与使用“，”
5. 在transition中，条件与条件、动作与动作之间用 “ /\ ” 联接。满足某个条件，执行某个动作用 " =|> "

transition：

condition：

1. 比较：expression = expression
2. 接收消息：Rcv(message)
3. 测试元素是否在集合中：in(element,set) not (in(element,set))

transition中的condition

action

1. 赋值：variable' ：= expression
2. 创建一个新的信息：variable' := new()
3. 发送信息：Snd(message)
4. 添加元素至集合：set' := cons(element,set)

transition 中的 actions

例：（复现图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的部分中描述安全属性。如果未定义属性，则此部分不必存在。安全属性分为三类：

1. 信息的机密性： 通过关键字security of完成声明，后跟一个常量标识符；此标识符用于生成信息（或第一次通信）的角色中，使用谓词secret语法如下： secret(information,identifier,agents-set) 其中agents set是允许知道信息的agent集合
2. 强身份认证 代理Y对代理X进行强身份验证以获取某些信息：声明是通过关键字authentication_on完成的，后跟常量标识符；此标识符用于与身份验证相关的角色； 首先，在经过身份验证的代理X的角色中，在谓词witness使用以下语法： witness(X,Y,identifier,information) 第二，在执行身份验证的代理Y的角色中，在谓词request中使用以下语法： request(Y,X,identifier,information) 这种身份验证的原理是，当发出request时，必须已经为相同的信息发出了相应的witness。
3. 弱身份认证 与强身份认证类同。声明关键字：weak_authentication_on。用到的谓词为weak与wrequest

例：NSPK协议的安全属性声明：

1.6 执行场景

environment()

相关代码可以关注公号：养两只猫。发送NSPK获取。

下节内容将从以下方面继续进行。

2 工具使用

2.1 hlps12if

2.2 cl-atse