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:

 

PROBLEMS:
3
 

ATTACKS:
None

 

NOTES:

 


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