Diffie-Hellman使用Casper

Question

我的任务是使用Casper (在.spl文件中)对Diffie-Hellman密钥交换协议进行建模。我记下了基础知识，发现真的很难提出正确的协议描述(#Protocol description)。我到处寻找，尝试了所有的方法(就我对Casper的了解而言)，但没有任何解决方案。我非常惊讶，关于这方面的文档如此之少。

如果有人能帮助我开始这方面的工作，我将不胜感激。

在进阶时谢谢！

Answer 1

这就是了！( Gavin Low完成)我正在做一个关于这些东西的研究，你是对的，它很难被罚款。将此代码复制到新文件，并将其另存为.spl

-- Diffie Hellman

#Free variables  
datatype Field = Gen | Exp(Field,Num)  unwinding 2  
A, B : Agent  
x, y : Num  
expx, expy, k : Field  
text : TEXT  

InverseKeys =  (k,k), (Exp,Exp), (Gen,Gen)  

#Processes  
INITIATOR(A, x, text)   
RESPONDER(B, y)   

#Protocol description  
0.    -> A : B  
[A != B]  
1.  A -> B : Exp(Gen,x) % expx  
[A != B and expx!=Gen]  
<k := Exp(expx, y)>  
2.  B -> A : Exp(Gen,y) % expy  
<k := Exp(expy, x)>  
3.  A -> B : {text}{k}  

#Specification  
Secret(A, text, [B])  
Secret(B, text, [A])  

#Actual variables  
Alice, Bob, Mallory : Agent  
X, Y, Z : Num  
Text1, Text2 : TEXT  

#Equivalences  
forall x, y : Num . Exp ( Exp(Gen,x), y ) = Exp( Exp(Gen,y), x )  

#System  
INITIATOR(Alice, X, Text1)  
RESPONDER(Bob,  Y)  

#Intruder Information
Intruder = Mallory
IntruderKnowledge = {Alice, Bob, Mallory, Z, Text2}