PROTOCOL:
CRAM-MD5 Challenge-Response Authentication Mechanism

PURPOSE:

CRAM-MD5 is intended to provide an authentication extension to IMAP4 that neither transfers passwords in cleartext nor requires significant security infrastructure in order to function. To this end, the protocol assumes a shared password (which we model, without loss of generality, as a shared cryptographic key) between the IMAP4 server (called S in our model) and each client A. Only a hash value of the shared password is ever sent over the network, thus precluding plaintext transmission.

 

REFERENCE:

RFC 2195 [RFC2195]  

MODELER:

Paul Hankes Drielsma, ETH Zürich, July 2004

 

ALICE_BOB: 

 Alice-Bob Notation:
  1. A -> S: A
  2. S -> A: Ns.T.S
  3. A -> S: F(SK.T)
  where
      Ns is a nonce generated by the server;
      T is a timestamp (currently abstracted with a nonce)
      SK is the shared key between A and S
      F is a cryptographic hash function (MD5 in practice, but this is
       unimportant for our purposes).  The use of F
       is intended to ensure that only a digest of the shared
       key is transmitted, with T assuring freshness of the 
       generated hash value.

 

LIMITATIONS:

Issues abstracted from:

 

PROBLEMS:
2
 

CLASSIFICATION:
G1, G2, G3, G12
 

ATTACKS:
None
 

NOTES:

RFC 2195 [RFC2195] states that the first message from the server S begins with a "presumptively arbitrary string of random digits"; that is, a nonce. Unspecified, however, is what the client should do with this nonce. It does not appear in subsequent protocol message. We therefore presume it is intended to ensure replay protection, but our HLPSL specification at present does not explicitly model that the client should maintain a list of nonces previously received from the server.  

HLPSL: 

role client(A, S: agent,
            SK: hash(agent.agent),
            F: hash_func,
            SND, RCV: channel (dy))
played_by A
def=

  local  State : nat, 
         T, Ns : text

  const  sec_SK : protocol_id

  init   State := 0

  transition 

  1. State = 0   /\ RCV(start) 
     =|>
     State' := 1 /\ SND(A)

  2. State = 1   /\ RCV(Ns'.T'.S)
     =|>
     State' := 2 /\ SND(F(SK.T')) 
                 /\ witness(A,S,auth,F(SK.T')) 
                 /\ secret(SK,sec_SK,{S})

end role




role server(S : agent,
            K, F: hash_func,
            SND, RCV: channel (dy))
played_by S
def=

  local State : nat,
        A     : agent,
        T, Ns : text,
        Auth  : hash(hash(agent.agent).text)

  init  State := 0

  transition 
   1. State = 0   /\ RCV(A') 
      =|>
      State' := 1 /\ Ns' := new()
                  /\ T' := new()
                  /\ SND(Ns'.T'.S)

   2. State = 1   /\ RCV(F(K(A.S).T)) 
      =|>
      State' := 2 /\ Auth' := F(K(A.S).T) 
                  /\ request(S,A,auth,F(K(A.S).T))

end role




role session(A, S: agent,
             K, F: hash_func)
def=

  local SK: hash(agent.agent),
        SNDA, SNDS, RCVA, RCVS: channel (dy)

  init SK := K(A.S)

  composition
       client(A,S,SK,F,SNDA,RCVA)
    /\ server(S,K,F,SNDS,RCVS)

end role




role environment()
def=

 const a, s : agent,
       k, f : hash_func,
       auth : protocol_id

 intruder_knowledge = {a,s,i,f}

 composition
      session(a,s,k,f)
   /\ session(i,s,k,f)
   /\ session(a,s,k,f)

end role




goal

  %secrecy_of SK
  secrecy_of sec_SK  % Addresses G12

  %Server authenticates Client on auth
  authentication_on auth  % Addresses G1, G2, G3

end goal




environment()