CODEWITHSUNDEEP
modelkeyprotocolsspldiffie-hellman
user2782125
user2782125

Reputation: 51

Diffie-Hellman using Casper

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.

Upvotes: 0

Views: 103

Answers (1)

user2842417
user2842417

Reputation: 1

here it is! ( done by Gavin Low) I am doing a research in these stuff, and you are right it hard to fine. Copy this code to new file and save it as .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}

Upvotes: 0

Related Questions