C -> A: U,G,N1,{Kca,T0,N1,hash(U,G,N1)}inv(Kca)
In PKINIT, the first message contains additional
information in the pre-authentication field:
The public key of U, a timestamp, the nonce repeated,
and a checksum of the message body. This is all signed
with the private key of U.
A -> C: U,Tcg,{G,Kcg,T1start,T1expire,N1}Ktemp,{{Ktemp}Kca}inv(Pka)
where Tcg := {U,C,G,Kcg,T1start,T1expire}Kag
A replies as usual, except the reply is encrypted
with a random key, and this key is included in the
pre-authentication field and encrypted with the U's
public key and signed with the A's private key.
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)
The AS, TGS and S cache the timestamps they have received in order to prevent replays as specified in RFC 1510.
We assume that the Key Distribution Centre (KDC)
is the certifying authority here.
role authenticationServer(
A,C,G : agent,
Kca : public_key,
Kag : symmetric_key,
SND, RCV : channel(dy),
L : text set,
Pka : public_key,
Hash : hash_func)
played_by A
def=
local State : nat,
N1 : text,
U : text,
T0 : text,
Kcg : symmetric_key,
T1start : text,
T1expire : text,
Ktemp : symmetric_key
const sec_a_Kcg : protocol_id
init State := 11
transition
1. State = 11 /\ RCV(U'.G.N1'.
{Kca.T0'.N1'.Hash(U'.G.N1')}_inv(Kca))
/\ not(in(T0',L)) =|>
State' := 12 /\ Kcg' := new()
/\ T1start' := new()
/\ T1expire' := new()
/\ Ktemp' := new()
/\ SND(U'.
{U'.C.G.Kcg'.T1start'.T1expire'}_Kag.
{G.Kcg'.T1start'.T1expire'.N1'}_Ktemp'.
{{Ktemp'}_Kca}_inv(Pka))
/\ L' := cons(T0',L)
/\ witness(A,C,n1,Kcg'.N1')
/\ request(A,C,t0,T0')
/\ secret(Kcg',sec_a_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( C,G,S,A : agent,
SND,RCV : channel(dy),
Kca,Pka : public_key,
U : text,
Hash : hash_func)
played_by C
def=
local State : nat,
Kcs : symmetric_key,
T1expire : text,
T2expire : text,
T1start : text,
T2start : text,
Kcg : symmetric_key,
Tcg,Tcs : {text.agent.agent.symmetric_key.text.text}_symmetric_key,
T0,T1,T2 : text,
Ktemp : symmetric_key,
N1, N2 : text
const sec_c_Kcs,sec_c_Kcg : protocol_id
init State := 1
transition
1. State = 1 /\ RCV(start) =|>
State' := 2 /\ T0' := new()
/\ N1' := new()
/\ SND(U.G.N1'.{Kca.T0'.N1'.Hash(U.G.N1')}_inv(Kca))
/\ witness(C,A,t0,T0')
2. State = 2 /\ RCV(U.Tcg'.
{G.Kcg'.T1start'.T1expire'.N1}_Ktemp'.
{{Ktemp'}_Kca}_inv(Pka)) =|>
State' := 3 /\ T1' := new()
/\ N2' := 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(
A,G,C,S : agent,
Kag,Kgs : symmetric_key,
LS : text set,
Hash : hash_func,
U : text,
Kca,Pka : public_key)
def=
local
SendC,ReceiveC : channel (dy),
SendS,ReceiveS : channel (dy),
SendG,ReceiveG : channel (dy),
SendA,ReceiveA : channel (dy)
composition
client(C,G,S,A,SendC,ReceiveC,Kca,Pka,U,Hash)
/\ server(S,C,G,Kgs,SendS,ReceiveS,LS)
/\ ticketGrantingServer(G,S,C,A,Kag,Kgs,SendG,ReceiveG,LS)
/\ authenticationServer(A,C,G,Kca,Kag,SendA,ReceiveA,LS,Pka,Hash)
end role
role environment()
def=
local LS : text set
const a,g,c,s : agent,
k_gi,
k_ag,k_gs : symmetric_key,
kia,kca,pka : public_key,
hash_ : hash_func,
u1,u2 : text,
t0,t1,t2a,t2b,n1,n2 : protocol_id
init LS := {}
intruder_knowledge = {a,g,c,s,pka,hash_,k_gi,u1,u2,
kia,inv(kia)}
composition
session(a,g,c,s,k_ag,k_gs,LS,hash_,u1,kca,pka)
/\ session(a,g,i,s,k_ag,k_gs,LS,hash_,u2,kia,pka)
end role
goal
%secrecy_of Kcg,Kcs
secrecy_of sec_a_Kcg,
sec_t_Kcg, sec_t_Kcs,
sec_s_Kcs,
sec_c_Kcs,sec_c_Kcg % addresses G10
%Client authenticates AuthenticationServer 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 authenticates Client on t1
authentication_on t1 % addresses G1, G2, and G3
%AuthenticationServer authenticates Client on t0
authentication_on t0 % addresses G1, G2, and G3
end goal
environment()