PROTOCOL:
CTP: Context Transfer Protocol, non-predictive variant

PURPOSE:
Multiple authentication for mobile communication in PANA,

transmitting context of a client between PANA agents after handover of client  

REFERENCE:

 

MODELER:
Lan Liu, Siemens CT IC 3, February 2005
 

ALICE_BOB:

 PaC	: PANA Client
 PPAA	: previous PANA Authentication Agent
 NPAA	: new PANA Authentication Agent
 It is assumed that PPAA and NPAA have mutually authenticated each other
 before this protocol starts.
 1. NPAA ----------------------------- NPAA ----------------------------> PaC
 2. PaC  --------              IP_PaC.IP_pPAA.NPaC.
                  Hash(CTP_key.IP_PaC.IP_pPAA.NPaC) --------------------> NPAA
 3. NPAA --------             {IP_PaC.IP_pPAA.NPaC.
                  Hash(CTP_key.IP_PaC.IP_pPAA.NPaC)}_ESP_Key -----------> PPAA
 4. PPAA ----------- {AAA_ID.AAA_k_i.PaC}_ESP_Key ----------------------> NPAA
 5. NPAA ---------- NSId.NnPAA.Hash(MAC_key.NSId.NnPAA) ----------------> PaC
 6. PaC  --------------- NnPAA.Hash(MAC_key.NnPAA) ---------------------> NPAA 
 

PROBLEMS:
3
 

CLASSIFICATION:
G1, G3, G7
 

ATTACKS:
None
 

NOTES:



HLPSL:


role new_PANA_Authentication_Agent(
  NPAA, PaC, PPAA : agent, 
  ESP_Key         : symmetric_key,      
  AAA_ID          : text,
  Hash, Key_f     : hash_func,    
  Snd, Rcv        : channel(dy)) 
played_by NPAA def=

local
  State                       : nat,
  NnPAA, NSId,
  NPaC, IP_PaC, IP_pPAA       : text,
  AAA_k_i: hash(symmetric_key.text.text),
  New_AAA_k: hash(hash(symmetric_key.text.text).text.text),
  MAC_key: hash(hash(hash(symmetric_key.text.text).text.text).text.text.text),
  H1: hash(symmetric_key.text.text.text)

const mac_key : protocol_id  
            
init State:=0  

transition

  0.  State=0
      /\ Rcv(start)
  =|> State':=2
      /\ Snd(NPAA)

  2.  State=2
      /\ Rcv(IP_PaC'.IP_pPAA'.NPaC'.H1')
  =|> State':=4
      /\ Snd({IP_PaC'.IP_pPAA'.NPaC'.H1'}_ESP_Key)
                     
  4.  State=4
      /\ Rcv({AAA_ID.AAA_k_i'.PaC}_ESP_Key) 
  =|> State':= 6
      /\ NnPAA' := new()
      /\ NSId':=new()
      /\ New_AAA_k':=Key_f(AAA_k_i'.NPaC.NnPAA')
      /\ MAC_key':=Key_f(New_AAA_k'.NPaC.NnPAA'.NSId')  
      /\ Snd(NSId'.NnPAA'.Hash(MAC_key'.NSId'.NnPAA'))

  6.  State=6
      /\ Rcv(NnPAA.Hash(MAC_key.NnPAA))
  =|> State':=8
      /\ request(NPAA, PaC, npaa_pac_mac_key, MAC_key) 
      % only now PaC has been authenticated and secrecy may be checked!
      /\ secret(MAC_key, mac_key, {PaC, NPAA})

end role


role pANA_Client( NPAA, PaC, PPAA : agent, CTP_KEY, AAA_k : symmetric_key, Hash, Key_f : hash_func, IP_PaC, AAA_ID, Session_ID, IP_pPAA : text, Snd, Rcv : channel(dy)) played_by PaC def= local State : nat, NPaC : text, AAA_k_i: hash(symmetric_key.text.text), New_AAA_k: hash(hash(symmetric_key.text.text).text.text), MAC_key: hash(hash(hash(symmetric_key.text.text).text.text).text.text.text), NnPAA, NSId : text init State:=1 transition 1. State=1 /\ Rcv(NPAA) =|> State':=7 /\ NPaC':=new() /\ Snd(IP_PaC.IP_pPAA.NPaC'.Hash(CTP_KEY.IP_PaC.IP_pPAA.NPaC')) /\ witness(PaC, PPAA, ppaa_pac_ip_pac, IP_PaC) 7. State=7 /\ Rcv(NSId'.NnPAA'. Hash(MAC_key'.NSId'.NnPAA')) /\ MAC_key'=Key_f(New_AAA_k'.NPaC.NnPAA'.NSId') /\ New_AAA_k'=Key_f(AAA_k_i'.NPaC.NnPAA') /\ AAA_k_i'=Key_f(AAA_k.AAA_ID.Session_ID) =|> State':=9 /\ Snd(NnPAA'.Hash(MAC_key'.NnPAA')) /\ witness(PaC, NPAA, npaa_pac_mac_key, MAC_key') end role
role previous_PANA_Authentication_Agent( NPAA, PaC, PPAA : agent, CTP_KEY, ESP_Key, AAA_k : symmetric_key, Hash, Key_f : hash_func, IP_PaC, AAA_ID, Session_ID, IP_pPAA : text, Snd, Rcv : channel(dy)) played_by PPAA def= local State : nat, NPaC, NnPAA : text, AAA_k_i : hash(symmetric_key.text.text) % should be a symmetric_key init State:=3 transition 3. State=3 /\ Rcv({IP_PaC.IP_pPAA.NPaC'. Hash(CTP_KEY.IP_PaC.IP_pPAA.NPaC')}_ESP_Key) =|> State':=5 /\ AAA_k_i' := Key_f(AAA_k.AAA_ID.Session_ID) /\ Snd({AAA_ID.AAA_k_i'.PaC}_ESP_Key) /\ request(PPAA, PaC, ppaa_pac_ip_pac, IP_PaC) end role
role session( NPAA,PaC, PPAA : agent, CTP_KEY, ESP_Key, AAA_k : symmetric_key, Hash, Key_f : hash_func, IP_PaC, AAA_ID, Session_ID, IP_pPAA : text) def= local SPaC, SNPAA, SPPAA, RPaC, RNPAA, RPPAA : channel(dy) composition previous_PANA_Authentication_Agent( NPAA, PaC, PPAA, CTP_KEY, ESP_Key, AAA_k, Hash, Key_f, IP_PaC, AAA_ID, Session_ID, IP_pPAA, SPPAA, RPPAA) /\ new_PANA_Authentication_Agent( NPAA, PaC, PPAA, ESP_Key, AAA_ID, Hash, Key_f, SNPAA, RNPAA) /\ pANA_Client( NPAA, PaC, PPAA, CTP_KEY, AAA_k, Hash, Key_f, IP_PaC, AAA_ID, Session_ID, IP_pPAA, SPaC, RPaC) end role
role environment() def= const ppaa_pac_ip_pac, npaa_pac_mac_key : protocol_id, npaa, pac, ppaa : agent, h, key_f : hash_func, ctp_key, esp_key, aaa_k, aaa_k_i, ctp_key_i : symmetric_key, ip_pac, aaa_id, ip_pPAA, sid1, sidi, ip_i, session_id_i : text intruder_knowledge = {npaa, pac, ppaa, h, key_f, aaa_id, aaa_k_i, ip_pPAA, ctp_key_i, session_id_i, ip_i} composition session(npaa, pac, ppaa, ctp_key, esp_key, aaa_k, h, key_f, ip_pac, aaa_id, sid1, ip_pPAA) /\ session(npaa, i, ppaa, ctp_key_i, esp_key, aaa_k_i, h, key_f, ip_i, aaa_id, sidi, ip_pPAA) end role
goal secrecy_of mac_key authentication_on ppaa_pac_ip_pac % addresses G1 and G3 authentication_on npaa_pac_mac_key % addresses G3 and G7 end goal
environment()