Scyther Advanced Topics

建立非对称秘钥对

声明一个公钥函数和一个私钥函数：

const pk2: Function ;

const sk2: Function ；

我们还声明这些函数代表非对称密钥对：

inversekeys(pk2, sk2) ;

近似等式理论，通用的加密结构更加自然的建模通过特定的等式。

g^ab（mod N）and g^ba（mod N）,建模 diffie-Hellman 的幂，

k(A,B) and k(B,A) 模拟双向长期秘钥

对于Scyther来时不直接支持这种等式理论，是仍然存在直接的，

核心思想是，如果对手学习其中的一个元素，我们就可以为攻击者提供学习等价类中所以术语的能力。例如：对于等式类型 {k(A,B),K(B,A)} ，我们能够提供敌手从k (A,B )学习 k(B,A )的能能力。我们能工提供一个适当的帮助协议（在定义的时候前面加上前缀 ‘@’）

protocol @ keysymmNaive (X){

reole X{

var Y: Agent;

recv_!1(X,X,k(x,y));

send_!2（X,X,k(x,y)）;

}}

因为角色可以被代理 X,Y任何一个实例化，覆盖所有代理可能的组合。

巴特西