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