专栏首页认证协议的形式化分析形式化分析工具(六):HLPSL Tutorial(Example 4,other)
原创

形式化分析工具(六):HLPSL Tutorial(Example 4,other)

本节主要内容为:代数运算符

XOR还具有X XOR X = 0的取消属性xor(a,b)

幂运算具有X1 = X的标识属性exp(g,a)

Example 4:Needham-Schroeder公钥协议

A-B表达式:

使用SPAN里的此CL-AtSe终端对协议里的异或分析

默认情况下,CL-AtSe打印的攻击痕迹可能不是最小的。实际上,这是CL-Atse的首次攻击。但是,可以使用-short选项要求CL-Atse输出最小的攻击之一(以步数为单位):

3 HLPSL Tips

3.1 Priming Variables

如果为变量分配了新值,则必须在:=左侧的变量名称中加注号 “

•在RCV通道中,如果接收到一个新值,则应准备用于存储该值的变量应该primed。 •在SND通道中,如果您要发送旧值,请不要prime变量。 •如果要发送刚刚在同一步骤中接收或计算的值,则对变量进行prime。 •局部变量应在初次读取或发送之前分配一个值:在init部分(不带primes)中,或通过为其prime实例分配值。

3.2 Witness and Request

参考前面的

3.3 Secrecy

参考前面的

注:

  1. secret在信息一创建就要进行声明。 如new()产生的现时,那么保密声明应在—并且仅在—角色中给出引入价值
  2. 如果秘密是来自多个角色的成分的组合,那么在所有角色中都应提供保密谓词,以构成非原子秘密价值。
  3. If a role played by A shares a secret T with some player U of another role, and the identity of U is not accessible for A (e.g. because of anonymity), the predicate secret(T,t,{U}) cannot be given in the role of A. In this case, it should be given in the role of U instead, right after the transition that sends T to U has been authenticated.

3.4 Constants and Variables

不要忘记声明模型中使用的所有常量,并为它们提供合适的类型。否则,编译器将发出警告,并且后端可能会产生意外的结果。另外,请勿在具有不同类型的不同角色中使用相同的变量(或常量)名称。

3.5 Concatenation (.) and Commas (,)

参考上一篇

3.6 Exploring executability of your model

没看懂,和工具上的对应不起来

SATMC对于HLPSL规范中类型的正确使用特别严格。因此,此功能对于查找可能导致协议规范不可执行的类型错误非常有用。

3.7 Detecting Replay Attacks

建议声明两个相同的会话。前文讲过

3.8 Instantiating Sessions

3.9 Function Results

并不友好,可以使用其它仿真软件如:Tamarin

3.10 Declaring Channels

4 Questions and answers about HLPSL

*我也没看明白

*1.request的位置问题。是一收到就验证,还是在最后的transition在验证。两者之间关系?

讲的不清楚,放在最后吧。先

2.message类型与text类型有什么区别

message是所有类型的超类型,例如nat和text,而后者代表未解释的位字符串。

*3.问:secret(T1,t1,{A})实际上是什么意思?该术语的值仅由A知道,还是该值在当前角色和A之间共享?在某些情况下,它似乎模棱两可。 A:这意味着A知道该值(以及在给定T1 = T2的情况下为其赋予谓词秘密(T2,t2,RS)的任何其他角色集RS)。

4.exp是像inv这样的特殊功能吗?这到底是什么意思?

exp(exp(X,Y),Z) = exp(exp(X,Z),Y) and exp(exp(X,Y),inv(Y) = X

5. 何时应允许入侵者扮演角色?

入侵者通常可以扮演不受信任的最终参与者的角色。 比如云服务器,一般认为是可信的。

A Symbols and Keywords

Symbol

Description

example

.

(消息的)关联级联

SND(ABC.XY.Z)

,

分隔集合的元素,或谓词或角色的参数

素数,用于在过渡中引用变量的下一个(新)值

X’

;

角色的顺序组成

Phase1(...); Phase2(...)

%

评论(直到行尾)

:=

初始化部分中(局部变量的)初始化

init X := 1

分配给(primed!)局部变量

X’ := 1

=

分配变量或其他表达式的相等性检验

X= 1

<

少于

X < 2

/\

连词(逻辑与)

X = 2 /\ Y = 3

/\

角色的平行组成

alice(...) /\ bob(...)

/\_

conjunction over elements in a set

/\_{in(A,Agents)} Kr(A)=[]

->

从一种数据类型到另一种数据类型的映射

KeyMap:agent -> public_key

=|>

指示过渡

RCV(X)=​​|> AND(Y)

{ }

设置分隔符在knowledge declaration中

{a,b}

{ }_

加密或签名

SND({X}_K)

( )

指示函数,发送或接收语句或角色的参数。

accept

用于顺序组成,以指示角色何时完成以及新角色可以开始

accept State=5 /\ Auth=1

agent

代理的数据类型

bool

布尔值的数据类型

channel(dy)

通道的数据类型。目前仅实施了Dolev-Yao信道

composition

标记组成角色的组成部分的开始

cons

添加元素到集合

L’ = cons(X,L)

def=

表示角色主体的开始

delete

从集合中删除元素

L’= delete(X,L)

end role

表示角色结束

exp

求幂运算符(前缀)

exp(g,x) represents gx

hash_func

单向功能的数据类型

i

入侵者的身份

in

检查元素是否在列表或集合中

in(X,L)

init

指示局部变量的初始化

init State := 0

inv

密钥的逆向:给定公共密钥时返回私有密钥

inv(Ka)

intruder_knowledge

定义入侵者的知识

intruder_knowledge={a,kai}

local

指示本地变量部分

local State : nat

message

消息内容的一般类型

nat

自然数的数据类型

not

逻辑否定

not(in(X,L))

owns

变量的所有权:如果角色拥有变量,则只有此角色才能更改变量的值

owns X

played_by

对于基本角色:指定哪个代理正在扮演此角色

played_by A

public_key

公钥的数据类型

request

用于检查强身份验证(与witness一起)

request(A,B,alice_bob_na,Na)

secret

用于检查机密性

secret(K,k,{A,B})

set

用于无序收集类型值的数据类型

local S : text set init S := {}

symmetric_key

对称密钥的数据类型

text

未解释的位字符串的数据类型(如随机数)

transition

标记基本角色的过渡部分

witness

用于检查身份验证(与(w)request一起)

witness(B,A,bob_alice_na,Na)

wrequest

用于检查弱认证(与witness一起)

wrequest(A,B,alice_bob_na,Na)

xor

前缀xor运算符

xor(a,b)

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

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

我来说两句

0 条评论
登录 后参与评论

相关文章

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

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

    春风大魔王
  • 形式化分析工具(六):HLPSL Tutorial

    本文为阅读笔记。文章题目为: HLPSL Tutorial A Beginner’s Guide to Modelling and Analysing Inte...

    春风大魔王
  • SPAN+A VISPA for Verifying Cryptographic Protocols

    春风大魔王
  • python3 解码base64遇到的问题与解决

    错误代码:binascii.Error: Incorrect padding 解决方法 在解码前使用这个方法 if len(message) % 4: ...

    98k
  • pip不能安装Tensorflow问题

    kongxx
  • 基于bs4+requests的python爬虫伪装 - 草稿

    要导入fake-useragent库,需要先用pip安装,安装命令:pip install fake-useragent params是爬虫伪装的参数,数据类...

    潇洒坤
  • RFID Hacking②:PM3入门指南

    0x00 前言 Proxmark3是由Jonathan Westhues在做硕士论文中研究Mifare Classic时设计、开发的一款开源硬件,可以用于RF...

    用户1631416
  • 浅谈script标签中的async和defer

    浅谈script标签中的async和defer script标签用于加载脚本与执行脚本,在前端开发中可以说是非常重要的标签了。 直接...

    贾顺名
  • MySQL 数据类型

    学会自定义表中每一个字段(列)的数据类型,对学习SQL数据库以及性能调优有着很大的帮助!

    技能锦囊
  • 在WebKit中并行加载外部脚本译:

    作者:Tony Gentilcore 原文:http://webkit.org/blog/1395/running-scripts-in-webkit/ Web...

    小李刀刀

扫码关注云+社区

领取腾讯云代金券