Notes

%% HLPSL definition on Andrew Secure RPC protocol.
%% This patched version is that proposed by principle 10 proposed by Juan Carlos Lopez P.
%% By Juan Carlos Lopez Pimentel
%1 A --> B : A, {Na}_|Kab|
%2 B --> A : {Succ(Na), Nb}_|Kab|
%3 A --> B : {Succ(Nb)}_|Kab|
%4 B --> A : {Kpab,Nbp}_|Kab|
%Add the following steps
%5 A --> B : {Nap}_|Kpab|
%6 B --> A : {Succ(Nap)}_|Kpab|


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

role alice(A,B:agent,
Kab: symmetric_key,
Succ: hash_func,
Snd, Rcv: channel (dy))
played_by A
def=

local State: nat,
Na, Nb, Nap, Nbp: text,
Kpab: symmetric_key

const nap, na, nb, alice_bob_kpab, alice_bob_na, bob_alice_nb: protocol_id

init State := 0

transition

%% Start of the protocol
step1. State = 0 / Rcv(start) =|>

%1 A --> B : A, {Na}_|Kab|
State':= 2 / Na':= new()
/ Snd(A.{Na'}_Kab)

%% Receving the first response of B

%2 B --> A : {Succ(Na), Nb}_|Kab|

step2and3. State = 2 / Rcv({Succ(Na).Nb'}_Kab) =|>

%3 A --> B : {Succ(Nb)}_|Kab|
State':= 4 / Snd({Succ(Nb')}_Kab)
/ witness(A,B,bob_alice_nb,Nb')

%% Receving the second response of B

%4 B --> A : {Kpab,Nbp}_|Kab|
step4and5. State = 4 / Rcv({Kpab'.Nbp'}_Kab) =|>

%5 A --> B : {Nap}_|Kpab|
State':= 6
% q2.
/ request(A,B,alice_bob_kpab,Kpab')
% / wrequest(A,B,alice_bob_kpab,Kpab')
/ request(A,B,alice_bob_na,Na)


%%%%%%%%%%%%%%
end role

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

role bob(A,B:agent,
Kab: symmetric_key,
Succ: hash_func,
Snd, Rcv: channel (dy))
played_by B
def=

local State: nat,
Na, Nb, Nap, Nbp: text,
Kpab: symmetric_key

const kpab,nbp,alice_bob_kpab,alice_bob_na,bob_alice_nb: protocol_id

init State := 1

transition

%1 A --> B : A, {Na}_|Kab|
step1and2. State = 1 / Rcv(A.{Na'}_Kab) =|>
%2 B --> A : {Succ(Na), Nb}_|Kab|
State':= 3 / Nb':= new()
/ Snd({Succ(Na').Nb'}_Kab)
/ witness(B,A,alice_bob_na,Na')

%3 A --> B : {Succ(Nb)}_|Kab|
step3and4. State = 3 / Rcv({Succ(Nb)}_Kab) =|>
%4 B --> A : {Kpab,Nbp}_|Kab|
State':= 5 / Kpab':= new()
/ Nbp':= new()
/ Snd({Kpab'.Nbp'}_Kab)
/ witness(B,A,alice_bob_kpab,Kpab')
/ secret(Kpab',kpab,{A,B})
/ secret(Nbp',nbp,{A,B})
/ request(B,A,bob_alice_nb,Nb)



end role

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% The role representing a partial session between alice and bob
role andrewSRPC(A,B: agent,
Kab: symmetric_key,
Succ:hash_func)

def=

local SAB, RAB, SBA, RBA: channel (dy)

composition
alice (A,B,Kab,Succ,SAB,RAB)
/ bob (A,B,Kab,Succ,SBA,RBA)

end role

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% The main role
role environment()
def=

const a, b : agent,
kab,kai,kib : symmetric_key,
succ : hash_func

intruder_knowledge = {a, b, kai, kib, succ}

composition
andrewSRPC(a,b,kab,succ)
/ andrewSRPC(a,b,kab,succ)
/ andrewSRPC(a,i,kai,succ)
/ andrewSRPC(i,b,kib,succ)

end role

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Properties to verify
goal

% secrecy_of nbp,kpab
% authentication_on bob_alice_nb
% authentication_on alice_bob_na
% q2.
authentication_on alice_bob_kpab
% weak_authentication_on alice_bob_kpab

end goal

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Call of the main role
environment()