%% PROTOCOL*: NSPK: Needham-Schroeder Public-Key Protocol
%% VARIANT: fix by Lowe (of 1995) without key server
%% PURPOSE: Two-party mutual authentication
%% MODELER: David von Oheimb, Siemens CT IC 3, January 2005
%% ALICE_BOB:
%%\begin{verbatim}
%% 1. A - {Na.A}_Kb ----> B
%% 2. A <- {Na.Nb.B}_Ka - B
%% 3. A - {Nb}_Kb ------> B
%%\end{verbatim}
%% PROBLEMS: 3
%% ATTACKS: None
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%HLPSL:
role alice (A, B: agent,
Ka, Kb: public_key,
SND, RCV: channel (dy))
played_by A def=
local State : nat,
Na, Nb: text
init State := 0
transition
0. State = 0 /\ RCV(start) =|>
State':= 2 /\ Na' := new() /\ SND({Na'.A}_Kb)
/\ secret(Na',na,{A,B})
/\ witness(A,B,bob_alice_na,Na')
%2. State = 2 /\ RCV({Na.Nb'.B}_Ka) =|>
%State':= 4 /\ SND({Nb'}_Kb)
% /\ request(A,B,alice_bob_nb,Nb')
2. State = 2 /\ RCV({Na.Nb'.B}_Ka) =|>
State':= 4 /\ request(A,B,alice_bob_nb,Nb')
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
role bob(A, B: agent,
Ka, Kb: public_key,
SND, RCV: channel (dy))
played_by B def=
local State : nat,
Na, Nb: text
init State := 1
transition
1. State = 1 /\ RCV({Na'.A}_Kb) =|>
State':= 3 /\ Nb' := new() /\ SND({Na'.Nb'.B}_Ka)
/\ secret(Nb',nb,{A,B})
/\ witness(B,A,alice_bob_nb,Nb')
%We do not need the code below anymore.
% 3. State = 3 /\ RCV({Nb}_Kb) =|>
% State':= 5 /\ request(B,A,bob_alice_na,Na)
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
role session(A, B: agent, Ka, Kb: public_key) def=
local SA, RA, SB, RB: channel (dy)
composition
alice(A,B,Ka,Kb,SA,RA)
/\ bob (A,B,Ka,Kb,SB,RB)
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
role environment() def=
const a, b : agent,
ka, kb, ki : public_key,
na, nb,
alice_bob_nb,
bob_alice_na : protocol_id
intruder_knowledge = {a, b, ka, kb, ki, inv(ki)}
composition
session(a,b,ka,kb)
/\ session(a,i,ka,ki)
/\ session(i,b,ki,kb)
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
goal
secrecy_of na, nb
%We no longer want this goal achieved.
%authentication_on alice_bob_nb
authentication_on bob_alice_na
end goal
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
environment()