PROTOCOL:
SSH Transport Layer Protocol

PURPOSE:

Secure authentication mechanism (of server) and key exchange  

REFERENCE:

http://www.ietf.org/internet-drafts/draft-ietf-secsh-transport-24.txt [secsh-transport]

 

MODELER:

David von Oheimb, Siemens CT IC 3, August 2004

 

ALICE_BOB:

setting up the transport, including key exchange:
 1. C -> S: NC
 2. S -> C: NS
 3. C -> S: exp(g,X)
 4. S -> C: k_S.exp(g,Y).{H}_inv(k_S) 
 with K=exp(exp(g,X),Y), H=hash(NC.NS.k_S.exp(g,X).exp(g,Y).K)
user authentication, connections, etc:
 5. C -> S: {XXX}_KCS with SID=H, KCS=hash(K.H.c.SID)
 6. S -> C: {YYY}_KSC with SID=H, KSC=hash(K.H.d.SID)

 

LIMITATIONS:

Issues abstracted from:

 

PROBLEMS:
2
 

ATTACKS:
None

 

NOTES:

Modelling of authentication property:  
The common way (see "standard version" in the HLPSL code) is done by augmenting the Server role with witness(S,C,n,K') and the Client-role with request(C,S,n,K') where K' is the common (secret!) key. This model yields a spurious attack in which the intruder always forwards the current message. The intruder does not know the common key! Thus, in this attack the intruder plays a dummy role. The attack only results since the intruder is also playing an active role and thus is witness for the final request:
 Request c s n exp(exp(g,Y(4)),X(3))
 Witness s i n exp(exp(g,X(3)),Y(4))
To avoid such a dummy attack a different modelling was chosen.  
The property is split into two parts. First, assuring that the client has communicated with the server. This is achieved by augmenting the Server role by witness(S,S,n,K') and the Client role by request(S,S,n,K'). Second, assuring that the common key is only(!) known to the client and the server and not(!) to the intruder. This is achieved by augmenting the Client-role by secret(K',S). Using this modelling no attack results.  
The protocol only authenticates the server and not the client. Therefore, messages sent by the server after completion of the protocol may not stay secret.

In the IETF draft (SSH Transport Layer Protocol) it is mentioned that the 'exchange hash SHOULD be kept secret'. This recommendation is violated by the send-operation in the 2nd protocol step in the IETF draft. Here, the 'exchange hash' corresponds to H in role Server and the violation concerns the SND-operation in transition 6 of role Server.  



HLPSL:


role client(C, S             : agent,
            SND, RCV         : channel(dy),
            Hash             : hash_func,
            HostKey          : hash_func,
            G                : nat,
            LetterC, LetterD : text)

played_by C def=

  local State:    nat,
        NC:       text,
        NS:       text,
        X:        text,
        EGY,K:    message, %should be: text
        H,SID_:   message, %should be: text
        KCS, KSC: message, %should be: symmetric_key
        SecretS:  text
  
  const secretC     : text,
        k           : protocol_id,
        sec_K,
        sec_KCS,
        sec_KSC,
        sec_secretC : protocol_id

  init   State := 1



  transition

   1. State  = 1 /\ RCV(start) =|> 
      State':= 3 /\ NC' := new()
                 /\ SND(NC')

   3. State  = 3 /\ RCV(NS') =|> 
      State':= 5 /\ X' := new()
                 /\ SND(exp(G,X'))

   5. State  = 5 /\ RCV(HostKey(S).EGY'.{H'}_inv(HostKey(S)))
                 /\ H' = Hash(NC.NS.HostKey(S).exp(G,X).EGY'.K') 
                 /\ K' = exp(EGY',X) =|> 
      State':= 7 /\ SID_' := H' 
                 /\ KCS' := Hash(K'.H'.LetterC.SID_')
                 /\ KSC' := Hash(exp(EGY',X).H'.LetterD.H')
                 /\ secret(K',  sec_K,  {C,S})
                 /\ secret(KCS',sec_KCS,{C,S})
                 /\ secret(KSC',sec_KSC,{C,S})
                 /\ SND({secretC}_KCS')
                 %/\ secret(secretC,sec_secretC,{C,S})
                 %/\ request(C,S,k,K')  % standard version
                 /\ request(S,S,k,K')

   7. State  = 7 /\ RCV({SecretS'}_KSC) =|> 
      State':= 9 

end role


role server(C, S : agent, SND, RCV : channel(dy), Hash : hash_func, HostKey : hash_func, G : nat, LetterC, LetterD : text) played_by S def= local State: nat, NS: text, NC: text, Y: text, EGX,K: message, %should be: text H,SID_: message, %should be: text KCS, KSC: message, %should be: symmetric_key SecretC: text const k: protocol_id init State := 2 transition 2. State = 2 /\ RCV(NC') =|> State':= 6 /\ NS' := new() /\ SND(NS') 6. State = 6 /\ RCV(EGX') =|> State':= 8 /\ Y' := new() /\ K' := exp(EGX',Y') /\ H' := Hash(NC.NS.HostKey(S).EGX'.exp(G,Y').K') /\ SID_' := H' /\ KCS' := Hash(K'.H'.LetterC.SID_') /\ KSC' := Hash(K'.H'.LetterD.SID_') /\ SND(HostKey(S).exp(G,Y').{H'}_inv(HostKey(S))) %/\ witness(S,C,k,K') % standard version /\ witness(S,S,k,K') 8. State = 8 /\ RCV({SecretC'}_KCS) =|> State':=10 end role
role session(C, S : agent, CS, SC : channel (dy), Hash : hash_func, HostKey : hash_func, G : nat, LetterC, LetterD : text) def= composition client(C, S, CS, SC, Hash, HostKey, G, LetterC, LetterD) /\ server(C, S, SC, CS, Hash, HostKey, G, LetterC, LetterD) end role
role environment() def= const c,s : agent, cs,sc,is,si,ci,ic : channel (dy), hash_,host_key : hash_func, g : nat, letter_c, letter_d : text intruder_knowledge = {c,s,hash_,host_key,g,letter_c,letter_d, inv(host_key(i))} composition session(c,s,cs,sc,hash_,host_key,g,letter_c,letter_d) /\ session(i,s,is,si,hash_,host_key,g,letter_c,letter_d) /\ session(c,i,ci,ic,hash_,host_key,g,letter_c,letter_d) end role
goal %secrecy_of K, KCS, KSC, secretC secrecy_of sec_K, sec_KCS, sec_KSC %Client authenticates Server on k authentication_on k end goal
environment()