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任何一個實例化， 覆蓋全部代理可能的組合。