专栏首页认证协议的形式化分析形式化分析工具AVISPA(三)学习User micro-manual of AVISPA
原创

形式化分析工具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。用到的谓词为weakwrequest

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

1.6 执行场景

environment()

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

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

2 工具使用

2.1 hlps12if

2.2 cl-atse

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

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

我来说两句

0 条评论
登录 后参与评论

相关文章

  • 基础知识补充3:对称加密与非对称加密简介

    对称加密是最快速、最简单的一种加密方式,加密(encryption)与解密(decryption)用的是同样的密钥(secret key)。

    春风大魔王
  • 形式化分析工具:在虚拟操作系统和主机操作系统之间配置共享文件夹

    1. 在VirtualBox应用程序中,单击虚拟机名称,然后单击“配置”,然后单击“共享文件夹”,然后添加与主机OS上的路径关联的永久性虚拟共享文件夹。如图所示...

    春风大魔王
  • 形式化分析工具(五)使用CAS +语法轻松编写HLPSL规范

    在协议执行的开始,每个主体都需要一些初步的知识来撰写他的消息。知识之后的字段将与每个用户相关联的标识符列表,描述了协议开始之前他所知道的所有数据(names,k...

    春风大魔王
  • Python列表与数字的四则运算

    本文要点在于map()、eval()、repr()等内置函数的运用。 >>> def myMap(iterable, op, value): if ((not...

    Python小屋屋主
  • zabbix设置邮件告警的两种方式(内部mail和脚本)

    Zabbix监控服务端、客户端都已经部署完成,被监控主机已经添加,Zabiix监控运行正常。

    拓荒者
  • 如何在CentOS 7上安装和配置Zabbix以安全地监视远程服务器

    Zabbix是用于网络和应用程序的开源监控软件。它提供对从服务器,虚拟机和任何其他类型的网络设备收集的数千个指标的实时监控。这些指标可帮助您确定IT基础架构当前...

    风研雨墨
  • WPF 源代码 从零开始写一个 UI 框架

    需要知道 WPF 是一个 UI 框架,作为一个 UI 框架,最主要的就是交互。也就是 UI 框架需要有渲染显示和处理用户输入的功能。 如果直接告诉大家 WPF ...

    林德熙
  • 前端基础建设之export、import使用

    在ES6前, 前端就使用RequireJS或者seaJS实现模块化, requireJS是基于AMD规范的模块化库, 而像seaJS是基于CMD规范的模块化库...

    用户5166330
  • python3 购物车小程序

    #定义商品列表 List_of_commodities = [ ('Iphone',6888), ('Mac Pro',12888), ('Bike',3000...

    py3study
  • 面对日益精细化的需求,品牌该如何寻找突破点?

    随着消费升级,我们迈入了场景化消费时代。“场景+零售”的模式已经成为了商业领域的重要风口,对许多行业的发展方向起着很大的作用。

    汇桔宝官方账号

扫码关注云+社区

领取腾讯云代金券