形式化分析工具（六）：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
参考前面的
注：
- secret在信息一创建就要进行声明。 如new（）产生的现时，那么保密声明应在—并且仅在—角色中给出引入价值
- 如果秘密是来自多个角色的成分的组合，那么在所有角色中都应提供保密谓词，以构成非原子秘密价值。
- 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 删除。
腾讯云开发者
