Formal verification. simulation results: LAKA is ver- ified using the on-the-fly model checker (OFMC) backend, which is widely utilized by several schemes, e.g., [17], [22], [39], [40]. The OFMC verifies against the replay attack and the MITM attack with the bounded number of sessions. Fig. 7 depicts the verification results, i.e., SAFE from the Xxxxx-Xxx attack model and GOALs are achieved as specified. role environment() def= Const SmartMeter, NANGatway: agent, SK : symmetric_key, ST : symmetric_key, SMpub : public_key, H: hash_func, XXxx,Nid,uSM, vN, alpha, beta, t1, t2 : text, SmartMeter_NAN_uSM, NAN_SmartMeter_vN, : protocol_id, SmartMeter_NAN_SMid, NAN_SmartMeter_Nid : protocol_id, SmartMeter_NAN_T1, NAN_SmartMeter_T2 : protocol_id, SmartMeter_NAN_alpha, NAN_SmartMeter_beta : protocol_id, sub1, sub2, sub3 : protocol_id intruder knowledge = {SmartMeter, NANGateway, H} composition session (SmartMeter, NANGateway, H) /\ session (SmartMeter, i, H) /\ session (NANGateway, i, H) end role goal secrecy_of sub1 % secrecy_of sub2 % secrecy_of sub3 authentication_on SmaterMeter_NAN_SMid authentication_on NAN_SmartMeter_Nid authentication_on SmaterMeter_NAN_T1 authentication_on NAN_SmaterMeter_T2 end goal environment() Fig. 6. Environment and goal in HLPSL. % OFMC % Version of 2006/02/13 SUMMARY SAFE DETAILS BOUNDED_NUMBER_OF_SESSIONS PROTOCOL /home/span/span/project/LAKA.if GOAL as_specified BACKEND OFMC COMMENTS STATISTICS parseTime: 0.00s searchTime: 0.07s visitedNodes: 12 nodes depth: 1000 plies
Appears in 4 contracts
Samples: Authentication and Key Agreement, Authentication and Key Agreement, Authentication and Key Agreement
