• http://www.ietf.org/internet-drafts/draft-ietf-seamoby-ctp-11.txt
• Handover-Aware Access Control Mechanism: CTP for PANA [CTP-for-PANA]
• Use of Context Transfer Protocol (CTP) for PANA,
  http://ietfreport.isoc.org/idref/draft-bournelle-pana-ctp/

 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 

• secrecy of mac_key
• strong authentication on ppaa_pac_ip_pac
• strong authentication on npaa_pac_mac_key

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