VARIANT:
Unknown initiator

PURPOSE:

Provide a method to supply a secure channel between a client and server, authenticating the client with a password, and a server with a public key certificate.

 

REFERENCE:
[RFC2847,RFC2025]
 

MODELER:

 

ALICE_BOB:

  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)
 

 

LIMITATIONS:

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

and

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.

 

PROBLEMS:
5
 

CLASSIFICATION:
G1, G2, G3, G7, G10
 

ATTACKS:
None

 

NOTES:

 



HLPSL:


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()