• Boichut Yohan, LIFC-INRIA Besancon, May 2004
• Sebastian Mödersheim, ETH Zürich, January 2005

  1. A -> S: S.Na.exp(G,X).H(S.Na.exp(G,X))
  2. S -> A: S.Na.Nb.exp(G,Y).{S.Na.Nb.exp(G,Y)}_inv(Ks)
  3. A -> S: {login.pwd}_K where K= exp(exp(G,Y),X) = exp(exp(G,X),Y)
 

In real life, the messages 1 and 2 contain respectively the two following items lists.

• target names,
• a fresh random number,
• a list of available confidentiality algorithms,
• a list of available integrity algorithms,
• a list of available key establishment algorithms,
• a context key (or key half) corresponding to the first key estb. alg. given in the previous list,
• GSS context options/choices (such as unilateral or mutual authentication, use of sequencing and replay detection, and so on).

and

• target names,
• the random number sent by the initiator,
• a fresh random number,
• the subset of offered confidentiality algorithms which are supported by the target,
• the subset of offered integrity algorithms which are supported by the target,
• an alternative key establishment algorithm (chosen from the offered list) if the first one offered is unsuitable,
• the key half corresponding to the initiator's key estb. alg. (if necessary), or a context key (or key half) corresponding to the key estb. alg. above,
• GSS context options/choices (such as unilateral or mutual authentication, use of sequencing and replay detection, and so on).

The sets of algorithms agreed are not used by LIPKEY, indeed LIPKEY only uses SPKM for a key establishment. Thus they are not modelled. Furthermore, the key establishment modelled is a la Diffie-Hellman and GSS context options are not modelled.

• strong authentication on k
• secrecy of sec_i_Log, sec_i_Pwd,

role initiator (
        A,S: agent,
        G: nat,
        H: hash_func,
        Ka,Ks: public_key,
        Login_A_S: hash(agent.agent), 
        Pwd_A_S: hash(agent.agent), 
                            
        SND, RCV: channel (dy))
played_by A def=

  local 
        State        : nat,
        Na,Nb        : text,
        Rnumber1     : text,
        X            : message,
        Keycompleted : message,
        W            : nat,
        K            : text.text

  const sec_i_Log, sec_i_Pwd : protocol_id



  init  State := 0



  transition     

  1.  State  = 0 /\ RCV(start) =|>
      State':= 1 /\ Na' := new()
                 /\ Rnumber1' := new()
                 /\ SND(S.Na'.exp(G,Rnumber1').
                      H(S.Na'.exp(G,Rnumber1')))

  2.  State  = 1 /\ RCV(S.Na.Nb'.X'.{S.Na.Nb'.X'}_inv(Ks)) =|>
      State':= 2 /\ Keycompleted' := exp(X',Rnumber1)
                 /\ SND({Login_A_S.Pwd_A_S}_Keycompleted' ) 
                 /\ secret(Login_A_S,sec_i_Log,{S}) 
                 /\ secret(Pwd_A_S,sec_i_Pwd,{S})  
                 /\ K' := Login_A_S.Pwd_A_S
                 /\ witness(A,S,k,Keycompleted') 

end role



role target( 
        A,S           : agent,    
        G             : nat,
        H             : hash_func,
        Ka,Ks         : public_key,
        Login, Pwd    : hash_func,
        SND, RCV      : channel (dy))
played_by S def=

  local State        : nat,
        Na,Nb        : text,
        Rnumber2     : text,
        Y            : message,
        Keycompleted : message,
        W            : nat,
        K            : text.text

  const sec_t_Log, sec_t_Pwd : protocol_id



  init  State := 0


  transition 

  1.  State  = 0 /\ RCV(S.Na'.Y'.H(S.Na'.Y')) =|>
      State':= 1 /\ Nb' := new()
                 /\ Rnumber2' := new()
                 /\ SND(S.Na'.Nb'.exp(G,Rnumber2').
                       {S.Na'.Nb'.exp(G,Rnumber2')}_inv(Ks))
                 /\ Keycompleted':=exp(Y',Rnumber2')
                 /\ secret(Login(A.S),sec_t_Log,{A}) 
                 /\ secret(Pwd(A.S),  sec_t_Log,{A})   

  21. State  = 1 /\ RCV({Login(A.S).Pwd(A.S)}_Keycompleted) =|>
      State':= 2 /\ K' := Login(A.S).Pwd(A.S)
                 /\ request(S,A,k,Keycompleted) 

end role



role session(
          A,S : agent,
          Login, Pwd: hash_func,
          Ka: public_key,
          Ks: public_key,
          H: hash_func,
          G: nat)
def=

  local SndI,RcvI : channel (dy),
        SndT,RcvT : channel (dy)
  
  composition 
     initiator(A,S,G,H,Ka,Ks,Login(A.S),Pwd(A.S),SndI,RcvI) /\
     target(   A,S,G,H,Ka,Ks,Login,Pwd,SndT,RcvT)

end role




role environment()
def=

  const a,s,i,b: agent,
        ka, ki, kb, ks: public_key,
        login, pwd : hash_func,
        h: hash_func,
        g: nat,
        k: protocol_id

  intruder_knowledge = {ki,i, inv(ki),a,b,s,h,g,ks,login(i.s),pwd(i.s),ka

                       } 

  composition
            session(a,s,login,pwd,ka,ks,h,g)
        /\  session(b,s,login,pwd,kb,ks,h,g)
        /\  session(i,s,login,pwd,ki,ks,h,g)

end role



goal 

  %Target authenticates Initiator on k
  authentication_on k % addresses G1, G2 and G3

  %secrecy_of Login, Pwd
  secrecy_of sec_i_Log, sec_i_Pwd, % adresses G7 and G10
             sec_t_Log, sec_t_Pwd  % adresses G7 and G10

end goal



environment()