role alice (A,B : agent,
Ka,Kb : public_key,
Snd,Rcv : channel (dy)) played_by A def=
local
State : nat,
Na : message,
Nb : text
init
State:=0
transition
1. State=0 /\ Rcv(start) =|>
State':=1
/\ Na':=new()
/\ Snd({Na'.A}_Kb)
/\ witness(A,B,bob_alice_na,Na')
/\ secret(Na',na,{A,B})
2. State=1 /\ Rcv({Nb'.xor(Na,B)}_Ka) =|>
State':=2
/\ Snd({Nb'}_Kb)
/\ wrequest (A,B,alice_bob_nb,Nb')
end role
role bob (B,A : agent,
Kb,Ka : public_key,
Snd,Rcv : channel (dy)) played_by B def=
local
State : nat,
Na : message,
Nb : text
init
State:=0
transition
1. State=0 /\ Rcv({Na'.A}_Kb) =|>
State':=1
/\ Nb':=new()
/\ Snd({Nb'.xor(Na',B)}_Ka)
/\ witness(B,A,alice_bob_nb,Nb')
/\ secret(Nb',nb,{A,B})
2. State=1 /\ Rcv({Nb}_Kb) =|>
State':=2
/\ wrequest(B,A,bob_alice_na,Na)
end role
role session (A,B: agent,
Ka, Kb: public_key,
SND, RCV: channel(dy) ) def=
composition
alice(A,B,Ka,Kb,SND,RCV) /\
bob(B,A,Kb,Ka,SND,RCV)
end role
role environment() def=
local
Snd, Rcv: channel(dy)
const
a, b, i: agent,
ka, kb, ki: public_key,
na, nb, alice_bob_nb, bob_alice_na: protocol_id
intruder_knowledge = {a,b,i,ka,kb,ki,inv(ki)}
composition
session(a,b,ka,kb,Snd,Rcv) /\
session(a,i,ka,ki,Snd,Rcv)
end role
goal
weak_authentication_on alice_bob_nb
weak_authentication_on bob_alice_na
secrecy_of na, nb
end goal
environment()