VARIANT:
With SIM

 

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

 

REFERENCE:

 

MODELER:

 

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:

 

PROBLEMS:
3
 

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