本节主要内容为:代数运算符
XOR还具有X XOR X = 0的取消属性,xor(a,b)
而幂运算具有X1 = X的标识属性。...exp(g,a)
Example 4:Needham-Schroeder公钥协议
A-B表达式:
image.png
使用SPAN里的此CL-AtSe终端对协议里的异或分析
默认情况下,CL-AtSe...•在SND通道中,如果您要发送旧值,请不要prime变量。
•如果要发送刚刚在同一步骤中接收或计算的值,则对变量进行prime。...B,
alice_bob_na,Na) secret 用于检查机密性 secret(K,k,{A,B}) set 用于无序收集类型值的数据类型 local S : text set...(A,B,
alice_bob_na,Na) xor 前缀xor运算符 xor(a,b)