VARIANT:

using the EAP-Archie method

PURPOSE:

The protocol should provide fresh key agreement, 3P-authorisation and DoS resilience.

REFERENCE:

http://www.ietf.org/internet-drafts/draft-tschofenig-eap-ikev2-05.txt

MODELER:

Daniel Plasto for Siemens CT IC 3, 2004

ALICE_BOB:

 A is the client
 B is the server and AAA server
  1. A -> B: SAi1.KEi.Ni
  2. B -> A: SAr1.KEr.Nr

  3. A -> B: {IDi}_SK_e_i               
  4. B -> A: {IDr.AUTH2.S.SessionID}_SK_e_r

  5. A -> B: {SessionID.P.{nonceP}_KEK.Binding.MAC1}_SK_e_i
  6. B -> A: {SessionID.{nonceS}_KEK.Binding.MAC2}_SK_e_r

  7. A -> B: {SessionID.MAC3.AUTH3}_SK_e_i
  8. B -> A: {Success.AUTH4}_SK_e_r

 - SAi1: ciphersuite (actually a single nonce)
 - SAr1: ciphersuite response (actually the nonce returned)
 - KEi: DH message 1. exp(G,DHX)
 - KEr: DH message 2. exp(G,DHY)
 - Ni: nonce
 - Nr: nonce
 - SK: key derived from DH plus nonces.
      PRF(Ni.Nr.SAi1.exp(KEr,DHX)) for A
      PRF(Ni.Nr.SAr1.exp(KEi,DHY)) for B
 - SK_e_i: key derived from SK for the initiator's encryption PRFP1(SK)
 - SK_e_r: key derived from SK for the initiator's encryption PRFP2(SK)
 - Idi: initiator's identity
 - Idr: responder's identity
 - AUTH2: {message2.Ni.PRF(SK_a_r,IDr)},signed with Kb
 - AUTH3: PRF(EMK,message1.Nr.PRF(SK_a_i,IDi))
 - AUTH4: PRF(EMK,message2.Ni.PRF(SK_a_r,IDr))
 - SK_a_i: key derived from SK for the initiator's 
           authentication operations PRFP3(SK)
 - SK_a_r: key derived from SK for the responder's 
           authentication operations PRFP4(SK)
 - Ka: public key of A
 - Kb: public key of B
 - 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.nonceS.nonceP)
 - Binding: a nonce
 - MAC1: MAC(KCK.S.SessionID.P.{nonceP}_KEK.Binding)
 - MAC2: MAC(KCK.P.{nonceP}_KEK.SessionID.{nonceS}_KEK.Binding)
 - MAC3: MAC(KCK.SessionID)

LIMITATIONS:

The optional certificates are excluded for now.
The CREATE_CHILD_SA exchange is excluded, as are related fields.
The ciphersuite is modelled as a nonce which must be returned by B. Similar to only having one option available.

PROBLEMS:

secrecy of sec_SK, sec_EMK
strong authentication on ker_nr_sid__nonces
strong authentication on kei_ni_binding_noncep

ATTACKS:

None

NOTES:

For simplicity, the server and the AAA server are merged.
In this version, the AUTH payloads are included in messages 7 and 8. Note that this is the first possible place to include them. Three other variations on this have been modelled, which change the position for the AUTH messages.
The EAP Master Key is used as the Session Key, instead of applying another transform to get the Master Session Key.

HLPSL:

role alice(
    A,B                             : agent,
    G                               : text,
    Success                         : message,
    PRF,PRFP1,PRFP2,PRFP3,PRFP4,MAC : hash_func,
    Ka,Kb                           : public_key,
    KCK,KEK,KDK                     : symmetric_key,
    SND, RCV                        : channel (dy))
played_by A def=

  local
    Ni, SAi1, DHX                   : text, 
    Nr                              : text,
    SK                              : hash(text.text.text.message),
    KEr                             : message,
    SID_                            : text,
    State                           : nat,
    Binding,NonceP                  : text,
    NonceS                          : text,
    EMK                             : hash(symmetric_key.text.text),
    KEr_Nr_SID__NonceS,
    KEi_Ni_Binding_NonceP           : message

  const
    sec_SK, sec_EMK  : protocol_id

  init 
    State := 0

  transition

 1. State  = 0  /\ RCV(start) =|>
    State':= 2  /\ Ni' := new()
                /\ SAi1' := new()
                /\ DHX' := new()
                /\ SND(SAi1'.exp(G,DHX').Ni') 

 2. State  = 2  /\ RCV(SAi1.KEr'.Nr') =|>
    State':= 4  /\ SK' := PRF(Ni.Nr'.SAi1.exp(KEr',DHX)) 
                /\ SND({A}_PRFP1(SK')) 

 3. State  = 4  /\ RCV({ B.
                         {SAi1.KEr.Nr.Ni.PRF(PRFP4(SK).B)}_inv(Kb).
                         B.SID_'
                       }_PRFP2(SK)) =|>
    State':= 6  /\ Binding' := new()
                /\ NonceP' := new()
                /\ SND({ SID_'.A.
                         {NonceP'}_KEK.
                         Binding'.
                         MAC(KCK.B.SID_'.A.{NonceP'}_KEK.Binding')
                       }_PRFP1(SK))
                /\ KEi_Ni_Binding_NonceP' := exp(G,DHX).Ni.Binding'.NonceP'
                /\ witness(A,B,kei_ni_binding_noncep,KEi_Ni_Binding_NonceP')

 4. State  = 6  /\ RCV({ SID_.
                         {NonceS'}_KEK.
                         Binding.
                         MAC(KCK.A.{NonceP}_KEK.SID_.{NonceS'}_KEK.Binding)
                       }_PRFP2(SK)) =|>
    State':= 8  /\ EMK' := PRF(KDK.NonceS'.NonceP)
                /\ SND({ SID_.
                         MAC(KCK.SID_).
                         PRF(EMK'.SAi1.exp(G,DHX).Ni.Nr.PRF(PRFP3(SK).A))
                       }_PRFP1(SK))

 5. State  = 8  /\ RCV({ Success.
                         PRF(EMK.SAi1.KEr.Nr.Ni.PRF(PRFP4(SK).B))
                       }_PRFP2(SK)) =|>
    State':= 10  
                /\ secret(SK, sec_SK, {A,B})
                /\ secret(EMK,sec_EMK,{A,B})
                /\ KEr_Nr_SID__NonceS' := KEr.Nr.SID_.NonceS
                /\ request(A,B,ker_nr_sid__nonces,KEr_Nr_SID__NonceS')

end role



role bob (
    A,B                             : agent,
    G                               : text,
    Success                         : message,
    PRF,PRFP1,PRFP2,PRFP3,PRFP4,MAC : hash_func,
    Ka, Kb                          : public_key,
    KCK,KEK,KDK                     : symmetric_key,
    SND, RCV                        : channel (dy))
played_by B def=

  local
    Ni,SAr1                         : text, 
    Nr,DHY,SID_,NonceS              : text,
    KEi                             : message,
    SK                              : hash(text.text.text.message),
    EMK                             : hash(symmetric_key.text.text),
    NonceP,Binding                  : text,
    State                           : nat,
    KEr_Nr_SID__NonceS,
    KEi_Ni_Binding_NonceP           : message

  init 
    State := 1

  transition

 1. State  = 1  /\ RCV(SAr1'.KEi'.Ni') =|>
    State':= 3  /\ Nr' := new()
                /\ DHY' := new()
                /\ SND(SAr1'.exp(G,DHY').Nr') 
                /\ SK' := PRF(Ni'.Nr'.SAr1'.exp(KEi',DHY')) 

 2. State  = 3  /\ RCV({A}_PRFP1(SK)) =|>
    State':= 5  /\ SID_' := new()
                /\ SND({ B.
                         {SAr1.exp(G,DHY).Nr.Ni.PRF(PRFP4(SK).B)}_inv(Kb).
                         B.SID_'
                       }_PRFP2(SK))

 3. State  = 5  /\ RCV({ SID_.A.
                         {NonceP'}_KEK.
                         Binding'.
                         MAC(KCK.B.SID_.A.{NonceP'}_KEK.Binding')
                       }_PRFP1(SK)) =|>
    State':= 7  /\ NonceS' := new()
                /\ SND({ SID_.
                         {NonceS'}_KEK.
                         Binding'.
                         MAC(KCK.A.{NonceP'}_KEK.SID_.{NonceS'}_KEK.Binding')
                       }_PRFP2(SK))
                /\ EMK' := PRF(KDK.NonceS'.NonceP')
                /\ KEr_Nr_SID__NonceS' := exp(G,DHY).Nr.SID_.NonceS'
                /\ witness(B,A,ker_nr_sid__nonces,KEr_Nr_SID__NonceS')

 4. State  = 7  /\ RCV({ SID_.
                         MAC(KCK.SID_).
                         PRF(EMK.SAr1.KEi.Ni.Nr.PRF(PRFP3(SK).A))
                       }_PRFP1(SK)) =|>
    State':= 9  /\ SND({ Success.
                         PRF(EMK.SAr1.exp(G,DHY).Nr.Ni.PRF(PRFP4(SK).B))
                       }_PRFP2(SK))
                /\ KEi_Ni_Binding_NonceP' := KEi.Ni.Binding.NonceP
                /\ request(B,A,kei_ni_binding_noncep,KEi_Ni_Binding_NonceP')

end role



role session(
    A,B                             : agent,
    G                               : text, 
    Success                         : message,
    PRF,PRFP1,PRFP2,PRFP3,PRFP4,MAC : hash_func, 
    Ka,Kb                           : public_key,
    KCK,KEK,KDK                     : symmetric_key)
def=

  local
     S1, S2 : channel (dy),
     R1, R2 : channel (dy)

  composition
     alice(A,B,G,Success,
           PRF,PRFP1,PRFP2,PRFP3,PRFP4,MAC,Ka,Kb,KCK,KEK,KDK,S1,R1)
  /\ bob(  A,B,G,Success,
           PRF,PRFP1,PRFP2,PRFP3,PRFP4,MAC,Ka,Kb,KCK,KEK,KDK,S2,R2)

end role



role environment() def=
 
  const 
    ker_nr_sid__nonces,
    kei_ni_binding_noncep : protocol_id,
    a,b                         : agent,
    ka,kb,ki1,ki2               : public_key,
    kck,kek,kdk                 : symmetric_key,
    kck_ib,kek_ib,kdk_ib        : symmetric_key,
    kck_ia,kek_ia,kdk_ia        : symmetric_key,
    g                           : text,
    success                     : message,
    prf,prfp1,prfp2,prfp3,prfp4 : hash_func,
    mac                         : hash_func

  intruder_knowledge = {prf,prfp1,prfp2,prfp3,prfp4,
                        g,mac,a,b,i,
                        ka,kb,ki1,inv(ki1),ki2,inv(ki2),
                        success}

  composition

%   session(a,b,g,success,prf,prfp1,prfp2,prfp3,prfp4,
%           mac,ka,kb,kck,kek,kdk) 
% /\ 
    session(a,b,g,success,prf,prfp1,prfp2,prfp3,prfp4,
            mac,ka,kb,kck,kek,kdk)
 /\ session(i,b,g,success,prf,prfp1,prfp2,prfp3,prfp4,
            mac,ki1,kb,kck_ib,kek_ib,kdk_ib)
 /\ session(a,i,g,success,prf,prfp1,prfp2,prfp3,prfp4,
            mac,ka,ki2,kck_ia,kek_ia,kdk_ia)

end role



goal

  %secrecy_of SK,EMK
  secrecy_of sec_SK, sec_EMK

  %Alice authenticates Bob on ker_nr_sid__nonces
  authentication_on ker_nr_sid__nonces
  %Bob authenticates Alice on kei_ni_binding_noncep
  authentication_on kei_ni_binding_noncep

end goal



environment()