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

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