subprotocol for the establishment of child SAs


IKE is designed to perform mutual authentication and key exchange prior to setting up an IPsec connection.

This subprotocol of IKE, known as CREATE\_CHILD\_SA, is used to establish child security associations once an initial SA has been set up using the two initial exchanges of IKEv2.







IKEv2-CHILD consists of a single exchange called CREATE\_CHILD\_SA. Given a previously set up security association with key K, the users exchange two messages encrypted with K. These messages exchanges nonces and perform a Diffie-Hellman exchange, establishing a new security association called. A (respectively B) generates a nonce Na and a Diffie-Hellman half key KEa (respectively KEb). In addition, SAa contains A's cryptosuite offers and SAb B's preference for the establishment of the new SA. Authentication is provided based on the use of K, which is assumed to be known only to A and B.
 1. A -> B: {SAa, Na, KEa}K
 2. B -> A: {SAb, Nr, KEb}K
Note that because we abstract away from the negotiation of cryptographic algorithms, we have SAa = SAb.



Issues abstracted from:



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



role alice(A,B:agent,
           G: text,
           F: hash_func,
           SK: symmetric_key, 
           SND_B, RCV_B: channel (dy))
played_by A

  local Ni, SA, DHX: text, 
        Nr: text,
        KEr: message, % more specifically: exp(text,text)
        CSK: hash(text.text.text.message), % CHILD_SA to be established.
        State: nat,
        MA,MB: text

  const sec_a_CSK : protocol_id

  init  State := 0


  1. State = 0  /\ RCV_B(start) =|>
     State':= 2 /\ SA' := new()
                /\ Ni' := new()
                /\ DHX' := new()
                /\ SND_B( {SA'.Ni'.exp(G,DHX')}_SK ) 
                /\ witness(A,B,ni,Ni')

  2. State = 2  /\ RCV_B({SA.Nr'.KEr'}_SK) =|>
     State':= 4 /\ MA' := new()
                /\ CSK' := F(Ni.Nr'.SA.exp(KEr',DHX)) 
                /\ SND_B( {MA'.zero}_CSK' )

  4. State = 4  /\ RCV_B({MB'.one}_CSK) =|> 
     State':= 6 /\ request(A,B,nr,Nr)
                /\ secret(CSK,sec_a_CSK,{A,B})

end role

role bob (B,A:agent, G: text, F: hash_func, SK: symmetric_key, SND_A, RCV_A: channel (dy)) played_by B def= local Ni, SA: text, Nr, DHY: text, KEi: message, CSK: hash(text.text.text.message), State: nat, MA,MB: text const sec_b_CSK : protocol_id init State := 1 transition 1. State = 1 /\ RCV_A( {SA'.Ni'.KEi'}_SK ) =|> State':= 3 /\ Nr' := new() /\ DHY' := new() /\ CSK' := F(Ni'.Nr'.SA'.exp(KEi',DHY')) /\ SND_A( {SA'.Nr'.exp(G,DHY')}_SK ) /\ witness(B,A,nr,Nr') 2. State = 3 /\ RCV_A( {MA'.zero}_CSK ) =|> State':= 5 /\ MB' := new() /\ SND_A( {MB'.one}_CSK ) /\ request(B,A,ni,Ni) /\ secret(CSK,sec_b_CSK,{A,B}) end role
role session(A, B: agent, SK: symmetric_key, G: text, F: hash_func) def= local SAC, RA, SB, RB: channel (dy) composition alice(A,B,G,F,SK,SAC,RA) /\ bob(B,A,G,F,SK,SB,RB) end role
role environment() def= const ni,nr : protocol_id, a, b : agent, kab, kai, kbi : symmetric_key, g : text, f : hash_func, zero, one : text intruder_knowledge = {g,f,a,b,i,kai,kbi,zero,one } composition session(a,b,kab,g,f) /\ session(a,i,kai,g,f) /\ session(i,b,kbi,g,f) end role
goal %secrecy_of CSK secrecy_of sec_a_CSK,sec_b_CSK % addresses G9 %Alice authenticates Bob on nr authentication_on nr % addresses G1, G2, G3, G7, G10 %Bob authenticates Alice on ni authentication_on ni % addresses G1, G2, G3, G7, G10 end goal