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任何一个实例化， 覆盖所有代理可能的组合。