authentication based on digital signatures, extended


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.







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.
 1. A -> B: SAa1, KEa, Na
 2. B -> A: SAb1, KEb, Nb
 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
      AUTHb = {SAb1.g^KEb.Na.Nb}inv(Kb)
 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.



Issues abstracted from:



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




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

  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


  %% 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