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:

version strings and matching
algorithm negotiation for encryption, hashing, etc.
Binary packet protocol/format, MAC, sequence numbers
message numbers (i.e. message type identifiers)
first_kex_packet_follows
alternative key exchange algorithms (other than Diffie-Hellman)
SSH_MSG_NEWKEYS, key re-exchange
SSH_MSG_DISCONNECT, SSH_MSG_DEBUG, SSH_MSG_IGNORE, SSH_MSG_UNIMPLEMENTED
SSH_MSG_SERVICE_REQUEST, SSH_MSG_SERVICE_ACCEPT

PROBLEMS:

secrecy of sec_K, sec_KCS, sec_KSC %%
strong authentication on k

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