Diffie-Hellman using Casper

Question

У меня есть задание моделировать обменный код ключа Diffie-Hellman Key с использованием Casper (в файле .spl). Я получил основы, и мне очень сложно найти правильное описание протокола (описание #Protocol). Я искал повсюду и все старался (насколько мне известно о Каспере), и никакого решения. Я очень удивлен, что в этом есть небольшая документация.

Если бы кто-нибудь мог помочь мне начать работу с этим, было бы весьма полезно.

Спасибо, продвинутый!

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}