前往小程序,Get更优阅读体验!
立即前往
首页
学习
活动
专区
工具
TVP
发布
社区首页 >专栏 >形式化分析工具(六):HLPSL Tutorial(Example 4,other)

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

原创
作者头像
春风大魔王
修改2020-07-24 14:20:03
1.2K0
修改2020-07-24 14:20:03
举报
文章被收录于专栏:认证协议的形式化分析

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

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)

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

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

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

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

评论
登录后参与评论
0 条评论
热度
最新
推荐阅读
目录
  • Example 4:Needham-Schroeder公钥协议
  • 3 HLPSL Tips
    • 3.1 Priming Variables
      • 3.2 Witness and Request
        • 3.3 Secrecy
          • 3.4 Constants and Variables
            • 3.5 Concatenation (.) and Commas (,)
              • 3.6 Exploring executability of your model
                • 3.7 Detecting Replay Attacks
                  • 3.8 Instantiating Sessions
                    • 3.9 Function Results
                      • 3.10 Declaring Channels
                      • 4 Questions and answers about HLPSL
                      • A Symbols and Keywords
                      相关产品与服务
                      NAT 网关
                      NAT 网关(NAT Gateway)提供 IP 地址转换服务,为腾讯云内资源提供高性能的 Internet 访问服务。通过 NAT 网关,在腾讯云上的资源可以更安全的访问 Internet,保护私有网络信息不直接暴露公网;您也可以通过 NAT 网关实现海量的公网访问,最大支持1000万以上的并发连接数;NAT 网关还支持 IP 级流量管控,可实时查看流量数据,帮助您快速定位异常流量,排查网络故障。
                      领券
                      问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档