VARIANT:
authentication based on digital signatures, extended

PURPOSE:

IKE is designed to perform mutual authentication and key exchange prior to setting up an IPsec connection. IKEv2 exists in several variants, the defining difference being the authentication method used.

This variant, which we call IKEv2-DSx, uses digital signatures and contains a slight extension in order to provide key confirmation, thus precluding the attack possible on the previous variant, IKEv2-DS.

 

REFERENCE:

[ipsec-ikev2]  

MODELER:

 

ALICE_BOB:

IKEv2-DSx proceeds in three so-called exchanges. In the first, called IKE\_SA\_INIT, the users exchange nonces and perform a Diffie-Hellman exchange, establishing an initial security association called the IKE\_SA. The second exchange, IKE\_SA\_AUTH, then authenticates the previous messages, exchanges the user identities, and establishes the first so-called "child security association" or CHILD\_SA which will be used to secure the subsequent IPsec tunnel. A (respectively B) generates a nonce Na and a Diffie-Hellman half key KEa (respectively KEb). In addition, SAa1 contains A's cryptosuite offers and SAb1 B's preference for the establishment of the IKE\_SA. Similarly SAa2 and SAb2 for the establishment of the CHILD\_SA. We extend these standard two exchanges with a third which we call EXTENSION. It consists of two messages, each containing a nonce (MA and MB, respectively) and a distinguished constant (0 and 1, respectively) encrypted with the IKE\_SA key K. This is sufficient to preclude the attack that is possible on IKEv2-DS, as it provides key confirmation. 
 IKE_SA_INIT
 1. A -> B: SAa1, KEa, Na
 2. B -> A: SAb1, KEb, Nb
 IKE_SA_AUTH
 3. A -> B: {A, AUTHa, SAa2}K
    where K = H(Na.Nb.SAa1.g^KEa^KEb) and 
      AUTHa = {SAa1.g^KEa.Na.Nb}inv(Ka)
 4. B -> A: {B, AUTHb, SAb2}K
    where 
      AUTHb = {SAb1.g^KEb.Na.Nb}inv(Kb)
 EXTENSION
 5. A -> B: {MA, 0}K
 6. B -> A: {MB, 1}K
Note that because we abstract away from the negotiation of cryptographic algorithms, we have SAa1 = SAb1 and SAa2 = SAb2.

 

LIMITATIONS:

Issues abstracted from:

 

PROBLEMS:
3
 

CLASSIFICATION:
G1, G2, G3, G7, G9, G10, G11
 

ATTACKS:
None

 


HLPSL: 

role alice(A,B:agent,
           G: text,
           F: hash_func,
           Ka,Kb: public_key,
           SND_B, RCV_B: channel (dy))
played_by A
def=

  local Ni, SA1, SA2, DHX: text, 
        Nr: text,
        KEr: message, %% more specifically: exp(text,text)
        SK: hash(text.text.text.message),
        State: nat,
        MA: text,
        MB: text,
        AUTH_B: message

  const sec_a_SK : protocol_id

  init  State := 0

  transition

  %% The IKE_SA_INIT exchange:
  %% I have abstracted away from the negotiation of cryptographic
  %% parameters.  Alice sends a nonce SAi1, which is meant to
  %% model Alice sending only a single crypto-suite offer.  Bob must
  %% then respond with the same nonce.
  1. State = 0  /\ RCV_B(start) =|>
     State':= 2 /\ SA1' := new()
                /\ DHX' := new()
                /\ Ni' := new()
                /\ SND_B( SA1'.exp(G,DHX').Ni' )

  %% Alice receives message 2 of IKE_SA_INIT, checks that Bob has
  %% indeed sent the same nonce in SAr1, and then sends the first 
  %% message of IKE_AUTH.
  %% As authentication Data, she signs her first message and Bob's nonce.
  2. State = 2  /\ RCV_B(SA1.KEr'.Nr') =|>
     State':= 4 /\ SA2' := new()
                /\ SK' := F(Ni.Nr'.SA1.exp(KEr',DHX))
                /\ SND_B( {A.{SA1.exp(G,DHX).Ni.Nr'}_(inv(Ka)).SA2'}_SK' )





  3. State = 4  /\ RCV_B({B.{SA1.KEr.Nr.Ni}_(inv(Kb)).SA2}_SK) =|>
     State':= 6 /\ MA' := new()
                /\ SND_B({MA'.zero}_SK)
                /\ AUTH_B' := {SA1.KEr.Nr.Ni}_(inv(Kb))
                /\ secret(SK,sec_a_SK,{A,B})
                /\ witness(A,B,sk2,SK)

  4. State = 6  /\ RCV_B({MB'.one}_SK) =|>
     State':= 8 /\ request(A,B,sk1,SK)

end role




role bob (B,A:agent,
          G: text,
          F: hash_func,
          Kb, Ka: public_key,
          SND_A, RCV_A: channel (dy))
played_by B
def=

  local Ni, SA1, SA2: text, 
        Nr, DHY: text,
        SK: hash(text.text.text.message),
        KEi: message,
        State: nat,
        MA: text,
        MB: text,
        AUTH_A: message

  const sec_b_SK : protocol_id

  init  State := 1

  transition

  1. State = 1  /\ RCV_A( SA1'.KEi'.Ni' ) =|>
     State':= 3 /\ DHY' := new()
                /\ Nr' := new()
                /\ SND_A(SA1'.exp(G,DHY').Nr')
                /\ SK' := F(Ni'.Nr'.SA1'.exp(KEi',DHY'))

  2. State = 3  /\ RCV_A( {A.{SA1.KEi.Ni.Nr}_(inv(Ka)).SA2'}_SK ) =|>
     State':= 5 /\ SND_A( {B.{SA1.exp(G,DHY).Nr.Ni}_(inv(Kb)).SA2'}_SK )
                /\ AUTH_A' := {SA1.KEi.Ni.Nr}_(inv(Ka))
                /\ witness(B,A,sk1,SK)
                /\ secret(SK,sec_b_SK,{A,B})

  3. State = 5  /\ RCV_A({MA'.zero}_SK) =|> 
     State':= 7 /\ MB' := new()
                /\ SND_A({MB'.one}_SK)
                /\ request(B,A,sk2,SK)

end role




role session(A, B: agent,
             Ka, Kb: public_key,
             G: text,
             F: hash_func)
def=

  local SA, RA, SB, RB: channel (dy)

  composition

     alice(A,B,G,F,Ka,Kb,SA,RA)
  /\ bob(B,A,G,F,Kb,Ka,SB,RB)

end role




role environment()
def=
 
  const sk1, sk2   : protocol_id,
        a, b       : agent,
        ka, kb, ki : public_key,
        g          : text,
        f          : hash_func,
        zero, one  : text

  intruder_knowledge = {g,f,a,b,ka,kb,i,ki,inv(ki),zero,one

                       }

  composition

        session(a,b,ka,kb,g,f)
     /\ session(a,i,ka,ki,g,f)
     /\ session(i,b,ki,kb,g,f)

end role




goal    

  %secrecy_of SK
  secrecy_of sec_a_SK, sec_b_SK % Addresses G9

  %Alice authenticates Bob on sk1
  authentication_on sk1 % Addresses G1, G2, G3, G7, G10
  %Bob authenticates Alice on sk2
  authentication_on sk2 % Addresses G1, G2, G3, G7, G10

end goal




environment()