model - Diffie-Hellman using Casper

Question

I have an assignment to model the Diffie-Hellman Key exchange protocol using Casper (in a .spl file). I got the basics down and am finding it really hard to come up with the correct protocol desciption (#Protocol description). I searched everywhere and tries everything(as far as my knowledge of Casper can take me) and no solution. I'm very surprised that there is so little documentation on this.

If anyone could help me get started on this, it would be greatly appreciated.

Thanks in advanced!

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}