VARIANT:
with PA-ENC-TIMESTAMP pre-authentication method

PURPOSE:
Mutual authentication
 

REFERENCE:

 

MODELER:

 

ALICE_BOB:

  C -> A: U,G,N1,{C,T0}_Kca
  A -> C: U,Tcg,{G,Kcg,T1start,T1expire,N1}_Kca

where Tcg := {U,C,G,Kcg,T1start,T1expire}_Kag A := Key Distribution Centre

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)

 

PROBLEMS:
7
 

CLASSIFICATION:
G1, G2, G3, G7, G8, G10
 

ATTACKS:
None

 

NOTES:

The AS, TGS and S cache the timestamps they have received in order to prevent replays as specified in RFC 1510.

 



HLPSL:

  role authenticationServer(
               A,C,G    : agent,
               Kca,Kag  : symmetric_key,
               SND, RCV : channel(dy),
               L        : text set)
  played_by A
  def=

    local State    : nat,
          N1       : text,
          U        : agent,
          T0       : text,
          Kcg      : symmetric_key,
          T1start  : text,
          T1expire : text

    const sec_a_Kcg : protocol_id

    init  State := 11

    transition
      1. State  = 11 /\ RCV(U'.G.N1'.{C.T0'}_Kca)
                     /\ not(in(T0',L)) =|> 
         State':= 12 /\ Kcg' := new()
                     /\ T1start' := new()
                     /\ T1expire' := new()
                     /\ SND(U'.
                            {U'.C.G.Kcg'.T1start'.T1expire'}_Kag.
                            {G.Kcg'.T1start'.T1expire'.N1'}_Kca)
                     /\ 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 : agent, 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 : agent, 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) /\ request(S,C,t2a,T2') /\ witness(S,C,t2b,T2') /\ secret(Kcs',sec_s_Kcs,{G,C,S}) end role
role client( C,G,S,A : agent, U : agent, Kca : symmetric_key, SND,RCV : channel(dy)) played_by C def= local State : nat, Kcs : symmetric_key, T1expire : text, T2expire : text, T1start : text, T2start : text, Kcg : symmetric_key, Tcg,Tcs : {agent.agent.agent.symmetric_key.text.text}_symmetric_key, T0,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() /\ T0' := new() /\ SND(U.G.N1'.{C.T0'}_Kca) /\ witness(C,A,t0,T0') 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,t2a,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,t2b,T2) end role
role session(A,G,C,S : agent, U : agent, Kca,Kgs,Kag : symmetric_key, LS,LG,LA : text set) def= local SendC,ReceiveC : channel (dy), SendS,ReceiveS : channel (dy), SendG,ReceiveG : channel (dy), SendA,ReceiveA : channel (dy) composition client(C,G,S,A,U,Kca,SendC,ReceiveC) /\ server(S,C,G,Kgs,SendS,ReceiveS,LS) /\ ticketGrantingServer(G,S,C,A,Kag,Kgs,SendG,ReceiveG,LG) /\ authenticationServer(A,C,G,Kca,Kag,SendA,ReceiveA,LA) end role
role environment() def= local LS, LG, LA : text set const a,g,c,s : agent, kgi, kca,kgs,kag : symmetric_key, kia : symmetric_key, u3, u1,u2 : agent, t0,t1,t2a,t2b,n1,n2 : protocol_id init LS := {} /\ LG := {} /\ LA := {} intruder_knowledge = {a,g,c,s,u1,u2,kia } composition session(a,g,c,s,u1,kca,kgs,kag,LS,LG,LA) % normal session /\ session(a,g,i,s,u2,kia,kgs,kag,LS,LG,LA) % i is Client end role
goal %secrecy_of Kcg,Kcs secrecy_of sec_a_Kcg, sec_t_Kcg, sec_t_Kcs, sec_s_Kcs, sec_c_Kcg, sec_c_Kcs % 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 t2b authentication_on t2b % addresses G1, G2, and G3 %Server authenticates Client on t2a authentication_on t2a % 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()