C -> A: U,G,N1
A -> C: U,Tcg,{G,Kcg,T1start,T1expire,N1}_Kca
where Tcg := {U,C,G,Kcg,T1start,T1expire}_Kag
A := Authentication Server
C -> G: S,N2,Tcg,Acg
G -> C: U,Tcs,{S,Kcs,T2start,T2expire,N2}_Kcg
where Acg := {C,T1}_Kcg (T1 is a timestamp)
Tcs := {U,C,S,Kcs,T2start,T2expire}_Kgs
C -> S: Tcs,Acs
S -> C: {T2'}_Kcs
where Acs := {C,T2'}_Kcs (T2 is a timestamp)
Both the TGS and S cache the timestamps they have received in order to prevent replays as specified in RFC 1510.
role keyDistributionCentre(
A,C,G : agent,
Kca,Kag : symmetric_key,
SND, RCV : channel(dy))
played_by A
def=
local State : nat,
N1 : text,
U : text,
Kcg : symmetric_key,
T1start : text,
T1expire: text
const sec_k_Kcg : protocol_id
init State := 11
transition
1. State = 11 /\ RCV(U'.G.N1') =|>
State':= 12 /\ Kcg' := new()
/\ T1start' := new()
/\ T1expire' := new()
/\ SND(U'.{U'.C.G.Kcg'.T1start'.T1expire'}_Kag.
{G.Kcg'.T1start'.T1expire'.N1'}_Kca)
/\ witness(A,C,n1,Kcg'.N1')
/\ secret(Kcg',sec_k_Kcg,{A,C,G})
end role
role ticketGrantingServer (
G,S,C,A : agent,
Kag,Kgs : symmetric_key,
SND,RCV : channel(dy),
L : text set)
played_by G
def=
local State : nat,
N2 : text,
U : text,
Kcg : symmetric_key,
Kcs : symmetric_key,
T1start, T1expire : text,
T2start, T2expire : text,
T1 : text
const sec_t_Kcg, sec_t_Kcs : protocol_id
init State := 21
transition
1. State = 21 /\ RCV( S.N2'.
{U'.C.G.Kcg'.T1start'.T1expire'}_Kag.
{C.T1'}_Kcg')
/\ not(in(T1',L))
=|>
State':= 22 /\ Kcs' := new()
/\ T2start' := new()
/\ T2expire' := new()
/\ SND( U'.
{U'.C.S.Kcs'.T2start'.T2expire'}_Kgs.
{S.Kcs'.T2start'.T2expire'.N2'}_Kcg')
/\ L' := cons(T1',L)
/\ request(G,C,t1,T1')
/\ witness(G,C,n2,Kcs'.N2')
/\ secret(Kcg',sec_t_Kcg,{A,C,G})
/\ secret(Kcs',sec_t_Kcs,{G,C,S})
end role
role server( S,C,G : agent,
Kgs : symmetric_key,
SND, RCV : channel(dy),
L : text set)
played_by S
def=
local State : nat,
U : text,
Kcs : symmetric_key,
T2expire: text,
T2start : text,
T2 : text
const sec_s_Kcs : protocol_id
init State := 31
transition
1. State = 31 /\ RCV({U'.C.S.Kcs'.T2start'.T2expire'}_Kgs.{C.T2'}_Kcs')
/\ not(in(T2',L)) =|>
State':= 32 /\ SND({T2'}_Kcs')
/\ L' := cons(T2',L)
/\ witness(S,C,t2a,T2')
/\ request(S,C,t2b,T2')
/\ secret(Kcs',sec_s_Kcs,{G,C,S})
end role
role client( U : text,
C,G,S,A : agent,
Kca : symmetric_key,
SND,RCV : channel(dy))
played_by C
def=
local State : nat,
Kcs,Kcg : symmetric_key,
T1expire: text,
T2expire: text,
T1start : text,
T2start : text,
Tcg,Tcs : {text.agent.agent.symmetric_key.text.text}_symmetric_key,
T1,T2 : text,
N1,N2 : text
const sec_c_Kcg, sec_c_Kcs : protocol_id
init State := 1
transition
1. State = 1 /\ RCV(start) =|>
State':= 2 /\ N1' := new()
/\ SND(U.G.N1')
2. State = 2 /\ RCV(U.Tcg'.{G.Kcg'.T1start'.T1expire'.N1}_Kca) =|>
State':= 3 /\ N2' := new()
/\ T1' := new()
/\ SND(S.N2'.Tcg'.{C.T1'}_Kcg')
/\ witness(C,G,t1,T1')
/\ request(C,A,n1,Kcg'.N1)
/\ secret(Kcg',sec_c_Kcg,{A,C,G})
3. State = 3 /\ RCV(U.Tcs'.{S.Kcs'.T2start'.T2expire'.N2}_Kcg) =|>
State':= 4 /\ T2' := new()
/\ SND(Tcs'.{C.T2'}_Kcs')
/\ witness(C,S,t2b,T2')
/\ request(C,G,n2,Kcs'.N2)
/\ secret(Kcs',sec_c_Kcs,{G,C,S})
4. State = 4 /\ RCV({T2}_Kcs) =|>
State':= 5 /\ request(C,S,t2a,T2)
end role
role session(
U : text,
A,G,C,S : agent,
Kca,Kgs,Kag : symmetric_key,
LS,LG : text set)
def=
local
SendC,ReceiveC : channel (dy),
SendS,ReceiveS : channel (dy),
SendG,ReceiveG : channel (dy),
SendA,ReceiveA : channel (dy)
composition
client(U,C,G,S,A,Kca,SendC,ReceiveC)
/\ server(S,C,G,Kgs,SendS,ReceiveS,LS)
/\ ticketGrantingServer(G,S,C,A,Kag,Kgs,SendG,ReceiveG,LG)
/\ keyDistributionCentre(A,C,G,Kca,Kag,SendA,ReceiveA)
end role
role environment()
def=
local LS, LG : text set
const
u1,u2 : text,
a,g,c,s : agent,
k_ca,k_gs,k_ag,k_ia : symmetric_key,
t1,t2a,t2b,n1,n2 : protocol_id
init LS := {} /\ LG := {}
intruder_knowledge = {u1,u2,a,g,c,s,k_ia
}
composition
session(u1,a,g,c,s,k_ca,k_gs,k_ag,LS,LG)
/\ session(u2,a,g,i,s,k_ia,k_gs,k_ag,LS,LG)
end role
goal
%secrecy_of Kcg,Kcs
secrecy_of sec_k_Kcg,
sec_t_Kcg, sec_t_Kcs,
sec_s_Kcs,
sec_c_Kcg, sec_c_Kcs % addresses G10
%Client authenticates KeyDistributionCentre on n1
authentication_on n1 % addresses G1, G3, G7, and G8
%Client authenticates TicketGrantingServer on n2
authentication_on n2 % addresses G1, G3, G7, and G8
%Client authenticates Server on t2a
authentication_on t2a % addresses G1, G2, and G3
%Server authenticates Client on t2b
authentication_on t2b % addresses G1, G2, and G3
%TicketGrantingServer weakly authenticates Client on t1
authentication_on t1 % addresses G1, G2, and G3
end goal
environment()