VARIANT:

With SIM

PURPOSE:

Mutual authentication, key establishment, integrity protection,
replay protection, confidentiality.

REFERENCE:

http://www.ietf.org/internet-drafts/draft-haverinen-pppext-eap-sim-16.txt

MODELER:

Jing Zhang for Siemens CT IC 3, 2004
Peter Warkentin, Siemens CT IC 3
Vishal Sankhla, University of Southern California, 2004

ALICE_BOB:

 S -> P: request_id
         % P gets his UserId = IMSI/TMSI
         % here, we use UserID = P
 P -> S: respond_id.UserID
         % S sends a list of supported versions
         % and P must agree of one of them
         % here, we assume only one version
 S -> P: request_sim_start.Version
         % P generates a nonce Np
 P -> S: respond_sim_start.Version.Np
         % S uses an authentication triplet (Rand.SRES.Kc) which it has
         % previously obtained from some authentication center AuC
         % in the home environment HE of P. Here we have
         %    SRES = A3(Kps,Rand)
         %    Kc   = A8(Kps,Rand)
         % where Kps is some long term secret symmetric key shared by P and
         % AuC/S, and A3,A8 are some known one-way functions.
         % S computes a message authentication code MAC1 via
         %    MK   = SHA1(P,Kc,Np,Version)
         %    Mac1 = MAC1(MK,Rand.Np)
         % MK is a master key which will be used for generating keys for 
         % encryption, authentication and data-integrity.
 S -> P: request_sim_challenge.Rand.Mac1
         % P checks validity of Mac1
         % P computes SRES = A3(Kps,Rand) and MAC2(MK,SRES)
 P -> S: respond_sim_challenge.Mac2
         % S checks Mac2 and thus authenticates P.
 S -> P: request_success

LIMITATIONS:

The server S combines the (logically) different roles of the home environment HE, the network access server NAS and the EAP server.
No resumption of a previous session.

PROBLEMS:

secrecy of sec_mk1, sec_mk2
strong authentication on mac1
strong authentication on mac2

ATTACKS:

None

NOTES:

EAP-SIM (Subscriber Identity Module) provides an authentication and encryption mechanism based on the existing method of Global System for Mobile communications (GSM). GSM authentication algorithms run on SIM, a smart card device inserted into the GSM user device. This card stores the shared secret between the user and the Authentication Center (AuC) in the mobile operator� network the user is subscribed to. From the AuC, EAP-SIM gathers the "triplet" (RAND, SRES, Kc) and generates the secure session key.

HLPSL:


role peer (P, S  : agent,
           Kps   : symmetric_key,
           SHA1  : hash_func,
           A3,A8 : hash_func,
           MAC1  : hash_func,
           MAC2  : hash_func,
           SND, RCV : channel(dy))
played_by P def=

  local  State      : nat,
         Np         : text,         % nonce
         Kc    : hash(symmetric_key.text),      % key
         MK    : hash(agent.hash(symmetric_key.text).text.text),      % key
         Mac1  : hash(hash(agent.hash(symmetric_key.text).text.text).text.text),      % mac
         Mac2  : hash(hash(agent.hash(symmetric_key.text).text.text).hash(symmetric_key.text)),      % mac
         SRES  : hash(symmetric_key.text),      % signed response
         Ver        : text,         % version
         Rand       : text          % random number

  const  sec_mk1, mac1, mac2                          : protocol_id,
         request_id,            respond_id            : text,
         request_sim_start,     respond_sim_start     : text,
         request_sim_challenge, respond_sim_challenge : text,
         request_success                              : text
        
  init State := 0

  transition

  1. State   = 0 /\ RCV(request_id)
     =|>
     State' := 2 /\ SND(respond_id.P)
        
  2. State   = 2 /\ RCV(request_sim_start.Ver')
     =|>
     State' := 4 /\ Np' := new()
                 /\ SND(respond_sim_start.Ver'.Np')

  4. State   = 4 /\ RCV(request_sim_challenge.Rand'.Mac1')
                 /\ Kc'    = A8(Kps.Rand')
                 /\ MK'    = SHA1(P.Kc'.Np.Ver)
                 /\ Mac1'  = MAC1(MK'.Rand'.Np)
     =|>
     State' := 6 /\ SRES' := A3(Kps.Rand')
                 /\ Mac2' := MAC2(MK'.SRES')
                 /\ SND(respond_sim_challenge.Mac2')
                 /\ request(P,S,mac1,Mac1')
                 /\ witness(P,S,mac2,Mac2')
                 /\ secret(MK',sec_mk1,{S,P})

  6. State   = 6 /\ RCV(request_success)
     =|>
     State' := 8

end role



role server (P, S  : agent,
             Kps   : symmetric_key,
             SHA1  : hash_func,
             A3,A8 : hash_func,
             MAC1  : hash_func,
             MAC2  : hash_func,
             SND, RCV : channel(dy))
played_by S def=

  local  State : nat,
         Np    : text,         % nonce
         Kc    : hash(symmetric_key.text),      % key
         MK    : hash(agent.hash(symmetric_key.text).text.text),      % key
         Mac1  : hash(hash(agent.hash(symmetric_key.text).text.text).text.text),      % mac
         Mac2  : hash(hash(agent.hash(symmetric_key.text).text.text).hash(symmetric_key.text)),      % mac
         SRES  : hash(symmetric_key.text),      % signed response
         Ver   : text,         % version
         Rand  : text          % random number

  const  sec_mk2, mac1, mac2                          : protocol_id,
         request_id,            respond_id            : text,
         request_sim_start,     respond_sim_start     : text,
         request_sim_challenge, respond_sim_challenge : text,
         request_success                              : text

  init State := 1

  transition

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

  3. State   = 3 /\ RCV(respond_id.P)
     =|>
     Ver':= new()/\
     State' := 5 /\ SND(request_sim_start.Ver')

  5. State   = 5 /\ RCV(respond_sim_start.Ver.Np')
     =|>
     State' := 7 /\ Rand' := new()
                 /\ Kc'   := A8(Kps.Rand')
                 /\ MK'   := SHA1(P.Kc'.Np'.Ver)
                 /\ Mac1' := MAC1(MK'.Rand'.Np')
                 /\ SND(request_sim_challenge.Rand'.Mac1')
                 /\ witness(S,P,mac1,Mac1')

  7. State   = 7 /\ RCV(respond_sim_challenge.Mac2')
                 /\ Mac2'  = MAC2(MK.SRES')
                 /\ SRES'  = A3(Kps.Rand)
     =|>   
     State' := 9 /\ SND(request_success)
                 /\ secret(MK, sec_mk2, {S,P})
                 /\ request(S,P,mac2,Mac2') 

end role



role session(P, S  : agent,
             Kps   : symmetric_key,
             SHA1  : hash_func,
             A3,A8 : hash_func,
             MAC1  : hash_func,
             MAC2  : hash_func)
def=

   local 
     SNDP, RCVP, SNDS, RCVS : channel (dy)

  composition
           peer(  P,S,Kps,SHA1,A3,A8,MAC1,MAC2,SNDP,RCVP)
        /\ server(P,S,Kps,SHA1,A3,A8,MAC1,MAC2,SNDS,RCVS)

end role



role environment() def=

   const
     p, s               : agent,
     kps, kpi, kis      : symmetric_key,
     sha1 : hash_func,
     a3,a8 : hash_func,
     mc1 : hash_func,
     mc2 : hash_func

   intruder_knowledge = {p, s, sha1, a3, a8, mc1, mc2,
                         kpi,    
                         kis     
                        }

   composition
        session(p,s,kps, sha1,a3,a8,mc1,mc2)
    /\  session(p,i,kpi, sha1,a3,a8,mc1,mc2)
    /\  session(i,s,kis, sha1,a3,a8,mc1,mc2)

end role



goal
        %secrecy_of MK
        secrecy_of sec_mk1, sec_mk2

        %Peer authenticates Server on mac1
        authentication_on mac1
        %Server authenticates Peer on mac2
        authentication_on mac2
        
end goal



environment()