VARIANT:
With Archie method

PURPOSE:
Mutual authentication, Key Derivation

EAP-Archie is a native EAP authentication method [20]. Therefore, there is no defined stand-alone version of Archie outside EAP. Archie is one of the symmetric cryptography methods that use a pre-shared secret key. The Archie´┐Ż 512-bit shared secret key consists of two 128-bit keys called key-confirmation key (KCK), key-encryption key (KEK), and the 256-bit key-derivation key (KDK). The key-confirmation key is used for mutual authentication. The key-encryption key is used for distributing the secret nonces for session key derivation. The key-derivation key is used for deriving the session keys.

Note: the original draft has expired. The new version is EAP-PSK.

 

REFERENCE:

 

MODELER:

 

ALICE_BOB:

 S -> P: request_id
 P -> S: respond_id.P
 S -> P: S.SessionID
 P -> S: SessionID.P.{nonceP}_KEK.Bind.MAC1
 S -> P: SessionID.{nonceA}_KEK.Bind.MAC2
 P -> S: SessionID.MAC3

 

PROBLEMS:
5
 

ATTACKS:
None
 

NOTES:

 - SessionID: Nonce
 - KCK:  Shared Key used for Authentication
 - KEK:  Shared Key used for Encryption
 - KDK:  Shared Key used for Key Derivation
 - EMK:  EAP Master Key: PRF(KDK.nonceA.nonceP)
 - MAC1: MAC(KCK.S.SessionID.P.{nonceP}_KEK.Bind)
 - MAC2: MAC(KCK.P.{nonceP}_KEK.SessionID.{nonceA}_KEK.Bind)
 - MAC3: MAC(KCK.SessionID)
 - Bind: addressing information (address_of_peer,address_of_server)

 



HLPSL:

role peer (
    P,S          : agent,
    MAC          : hash_func,
    KEK,KCK,KDK  : symmetric_key,
    SND,RCV      : channel (dy))
played_by P def=

  local
    Np,Bind      : text,
    Na,Sd        : text,           % Sd (=SessionID)
    State        : nat

  const
    request_id,
    respond_id    : text,
    sec_np,
    na,np,sd,bind : protocol_id

  init 
    State := 0

  transition

 0. State   = 0 /\ RCV(request_id) =|>
    State' := 1 /\ SND(respond_id.P)

 1. State   = 1 /\ RCV(S.Sd') =|>
    State' := 2 /\ Np'   := new()
                /\ Bind' := new()
                /\ SND(Sd'.P.
                       {Np'}_KEK.Bind'.
                       MAC(KCK.S.Sd'.P.{Np'}_KEK.Bind'))
                /\ secret(Np',sec_np,{P,S})
                /\ witness(P,S,np,Np')
                /\ witness(P,S,bind,Bind')

 2. State   = 2 /\ RCV(Sd.{Na'}_KEK.Bind.
                      MAC(KCK.P.{Np}_KEK.Sd.{Na'}_KEK.Bind)) =|>
    State' := 4 /\ SND(Sd.MAC(KCK.Sd))
                /\ request(P,S,sd,Sd)
                /\ request(P,S,na,Na')

end role


role server ( S,P : agent, MAC : hash_func, KEK,KCK,KDK : symmetric_key, SND,RCV : channel (dy)) played_by S def= local Np,Bind : text, Na,Sd : text, State : nat const request_id, respond_id : text, sec_na, na,np,sd,bind : protocol_id init State := 0 transition 0. State = 0 /\ RCV(start) =|> State' := 1 /\ SND(request_id) 1. State = 1 /\ RCV(respond_id.P) =|> State' := 3 /\ Sd' := new() /\ SND(S.Sd') /\ witness(S,P,sd,Sd') 2. State = 3 /\ RCV(Sd.P.{Np'}_KEK.Bind'. MAC(KCK.S.Sd.P.{Np'}_KEK.Bind')) =|> State' := 5 /\ Na' := new() /\ SND(Sd.{Na'}_KEK.Bind'. MAC(KCK.P.{Np'}_KEK.Sd.{Na'}_KEK.Bind')) /\ witness(S,P,na,Na') /\ request(S,P,np,Np') /\ request(S,P,bind,Bind') /\ secret(Na',sec_na,{P,S}) 3. State = 5 /\ RCV(Sd.MAC(KCK.Sd)) =|> State' := 7 end role
role session ( S,P : agent, MAC,PRF : hash_func, KEK,KCK,KDK : symmetric_key) def= local Speer,Rpeer,Sserver,Rserver : channel (dy) composition peer( P,S,MAC,KEK,KCK,KDK,Speer,Rpeer) /\ server(S,P,MAC,KEK,KCK,KDK,Sserver,Rserver) end role
role environment() def= const s,p : agent, mac,prf : hash_func, kek,kck,kdk : symmetric_key, kek_is,kck_is,kdk_is : symmetric_key, kek_ip,kck_ip,kdk_ip : symmetric_key, sd,na,np,bind : protocol_id intruder_knowledge = {s,p,mac,prf} composition session(s,p,mac,prf,kek,kck,kdk) /\ session(s,p,mac,prf,kek,kck,kdk) end role
% - P wants to be sure that S sent SessionID and nonceA. % - S wants to be sure that P sent nonceP and Bind. % - Secrecy of nonceA and nonceP, which are used for key derivation. goal %Peer authenticates Server on sd authentication_on sd %Peer authenticates Server on na authentication_on na %Server authenticates Peer on bind authentication_on bind %Server authenticates Peer on np authentication_on np %secrecy_of Na, Np secrecy_of sec_na, sec_np end goal
environment()