-------------------------------------------------------------------------------- -- -- Murphi Model of the Mobike protocol -- -------------------------------------------------------------------------------- -- -- version: 1.0 -- -- written by: Faisal Memon and Erik Weathers -- date: February 2006 -- affiliation: Stanford University (students) -- -------------------------------------------------------------------------------- -- -- Initiator Responder -- ----------- ----------- -- 1) (IP_I1:500 -> IP_R1:500) -- HDR, SAi1, KEi, Ni, -- N(NAT_DETECTION_SOURCE_IP), -- N(NAT_DETECTION_DESTINATION_IP) --> -- -- <-- (IP_R1:500 -> IP_I1:500) -- HDR, SAr1, KEr, Nr, -- N(NAT_DETECTION_SOURCE_IP), -- N(NAT_DETECTION_DESTINATION_IP) -- -- 2) (IP_I1:4500 -> IP_R1:4500) -- HDR, SK { IDi, CERT, AUTH, -- CP(CFG_REQUEST), -- SAi2, TSi, TSr, -- N(MOBIKE_SUPPORTED) } --> -- -- <-- (IP_R1:4500 -> IP_I1:4500) -- HDR, SK { IDr, CERT, AUTH, -- CP(CFG_REPLY), -- SAr2, TSi, TSr, -- N(MOBIKE_SUPPORTED) } -- -- (Initiator gets information from lower layers that its attachment -- point and address have changed.) -- -- 3) (IP_I2:4500 -> IP_R1:4500) -- HDR, SK { N(UPDATE_SA_ADDRESSES), -- N(NAT_DETECTION_SOURCE_IP), -- N(NAT_DETECTION_DESTINATION_IP) } --> -- -- <-- (IP_R1:4500 -> IP_I2:4500) -- HDR, SK { N(NAT_DETECTION_SOURCE_IP), -- N(NAT_DETECTION_DESTINATION_IP) } -- -- (Responder verifies that the initiator has given it -- a correct IP address.) -- -- 4) <-- (IP_R1:4500 -> IP_I2:4500) -- HDR, SK { N(COOKIE2) } -- -- (IP_I2:4500 -> IP_R1:4500) -- HDR, SK { N(COOKIE2) } --> -- -- -------------------------------------------------------------------------------- -- -- -------------------------------------------------------------------------------- -- constants, types and variables -------------------------------------------------------------------------------- -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - const NO_NATS_ALLOWED: true; -- are we allowing NATs in this test run? NumInitiators: 1; -- number of initiators NumResponders: 1; -- number of responders NumInitiators_p: 1; -- number of initiator primes NumIntruders: 1; -- number of intruders NetworkSize: 1; -- max number of outstanding messages in network MaxKnowledge: 10; -- max number of messages intruder can remember MaxRandom: 268435455; -- max value for random numbers MaxSpis: 10; -- max number of spis SharedSecret: 12345; Generator: 2; Prime: 7919; -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - type InitiatorId: scalarset (NumInitiators); -- identifiers InitiatorIdP: scalarset (NumInitiators_p); -- identifiers ResponderId: scalarset (NumResponders); IntruderId: scalarset (NumIntruders); SpiId: 0..MaxSpis; Random: 0..MaxRandom; Integer: 0..99999; AgentId: union {InitiatorId, InitiatorIdP, ResponderId, IntruderId}; MessageType : enum { -- different types of messages PRE_MOBIKE_1, -- state of initiator prior to start of protocol MOBIKE_1, -- IKE_INIT --> MOBIKE_2, -- <-- IKE_INIT MOBIKE_3, -- IKE_AUTH --> MOBIKE_4, -- <-- IKE_AUTH MOBIKE_5, -- IKE_UPDATE_ADDR --> MOBIKE_6, -- <-- IKE_UPDATE_ADDR MOBIKE_7, -- <-- IKE_RETURN_ROUTE MOBIKE_8, -- IKE_RETURN_ROUTE --> MOBIKE_ADDR_CHANGE, -- only used as state for session when transitioning -- from initiator to initiator-prime, not as a real -- msg type. MOBIKE_DONE }; Ke: record random: Random; end; SessionKey: record random: Random; end; Spi: record ke: Ke; peer_ke: Ke; peer: AgentId; peer_spi_id: SpiId; spi_id: SpiId; nonce: Random; peer_nonce: Random; msgid: Integer; peer_msgid: Integer; cookie: Random; exponent: Random; -- a or b, depending on who we are session_key: SessionKey; state: MessageType; in_use: boolean; end; Auth: record msgid: Integer; ke: Ke; nonce: Random; spi: SpiId; peer_nonce: Random; id_p: AgentId; shared_secret: Integer; end; Message : record source: AgentId; -- source of message dest: AgentId; -- intended destination of message msgid: Integer; init_spi: SpiId; resp_spi: SpiId; mType: MessageType; -- type of message ke_i: Ke; -- Ke used for encryption ke_r: Ke; -- dh partial Ke OR ID nonce_i: Random; nonce_r: Random; id_i: AgentId; id_r: AgentId; auth: Auth; mobike_s: boolean; upd_addr: AgentId; cookie: Random; -- cookie used for return routability check no_nats_allowed_source: AgentId; no_nats_allowed_dest: AgentId; session_key: SessionKey; from_intruder: boolean; end; Intruder : record nonces: array[AgentId] of boolean; -- known nonces messages: multiset[MaxKnowledge] of Message; -- known messages end; -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - var -- state variables for net: multiset[NetworkSize] of Message; -- network initiator_spi: array[SpiId] of Spi; responder_spi: array[SpiId] of Spi; next_random: Random; initiator_num_spis: SpiId; int: array[IntruderId] of Intruder; -- intruders -------------------------------------------------------------------------------- -- utility functions -------------------------------------------------------------------------------- -- Generate a fresh random number function new_random(): Random; var tmp: Random; begin tmp := next_random; next_random := next_random + 1; return tmp; end; function make_ke(exponent: Random): Ke; var tmp_ke: Ke; var tmp_exp: Random; begin tmp_exp := exponent; if (tmp_exp = 0) then error "make_ke: exponent not allowed to be 0\n"; else tmp_ke.random := Generator; while tmp_exp > 1 do tmp_ke.random := tmp_ke.random * Generator; tmp_exp := tmp_exp - 1; end; tmp_ke.random := (tmp_ke.random % Prime); end; return tmp_ke; end; -- Using "DH group 0", our made up group that uses a pitifully small -- prime number -- raise g to the exponent, and function make_session_key (ke_peer: Ke; exponent: Random): SessionKey; var tmp_sk: SessionKey; var tmp_exp: Random; begin tmp_exp := exponent; if (tmp_exp = 0) then error "make_session_key: exponent not allowed to be 0\n"; else tmp_sk.random := ke_peer.random; while tmp_exp > 1 do tmp_sk.random := tmp_sk.random * Generator; tmp_exp := tmp_exp - 1; end; tmp_sk.random := (tmp_sk.random % Prime); end; return tmp_sk; end; function initiator_new_spi(): Spi; begin for i: SpiId do if i != 0 & initiator_spi[i].in_use = false then initiator_spi[i].in_use := true; initiator_num_spis := initiator_num_spis + 1; return initiator_spi[i]; end; end; error "initiator: no more spis available"; end; function responder_new_spi(): Spi; begin for i: SpiId do if i != 0 & responder_spi[i].in_use = false then responder_spi[i].in_use := true; return responder_spi[i]; end; end; error "responder: no more spis available"; end; -------------------------------------------------------------------------------- -- rules -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- behavior of initiators -- initiator i starts protocol with responder or intruder j (step 1) ruleset i: InitiatorId do ruleset j: ResponderId do rule 20 "initiator starts protocol (step 1)" initiator_num_spis = 0 & multisetcount (l:net, true) < NetworkSize ==> var outM: Message; -- outgoing message spi: Spi; begin -- Create the SPI for this session undefine spi; spi := initiator_new_spi(); put "pas initiator_new_spi stuff\n"; spi.peer := j; spi.exponent := new_random(); -- Form the first message and send it out undefine outM; outM.source := i; outM.dest := j; outM.init_spi := spi.spi_id; outM.resp_spi := 0; outM.mType := MOBIKE_1; outM.ke_i := make_ke(spi.exponent); outM.nonce_i := new_random(); outM.from_intruder := false; outM.msgid := 0; outM.session_key := spi.session_key; multisetadd (outM,net); -- add SPI to multiset spi.state := MOBIKE_2; spi.peer_spi_id := 0; spi.nonce := outM.nonce_i; spi.ke := outM.ke_i; spi.msgid := outM.msgid; initiator_spi[spi.spi_id] := spi; end; end; end; -- initiator i main process ruleset i: InitiatorId do choose j: net do rule 20 "initiator main process" net[j].dest = i ==> var outM: Message; -- outgoing message inM: Message; -- incoming message spi_id: SpiId; spi: Spi; auth: Auth; continue_MOBIKE: boolean; begin inM := net[j]; multisetremove (j,net); spi_id := inM.init_spi; spi := initiator_spi[spi_id]; continue_MOBIKE := true; switch inM.mType case MOBIKE_2: if (spi.in_use = true & spi.peer = inM.source & spi.state = MOBIKE_2) then if spi.peer_msgid != inM.msgid then put "initiator: mismatch of msgid\n"; else -- Update the SPI spi.state := MOBIKE_4; spi.peer_spi_id := inM.resp_spi; spi.peer_nonce := inM.nonce_r; spi.peer_ke := inM.ke_r; spi.peer_msgid := inM.msgid + 1; spi.session_key := make_session_key(inM.ke_r, spi.exponent); put "Initiator: session_key: "; put spi.session_key; -- Create the Auth payload undefine auth; auth.msgid := spi.msgid; auth.ke := spi.ke; auth.nonce := spi.nonce; auth.spi := spi.spi_id; auth.peer_nonce := spi.peer_nonce; auth.id_p := i; auth.shared_secret := SharedSecret; undefine outM; outM.source := i; outM.dest := spi.peer; outM.mType := MOBIKE_3; outM.msgid := spi.msgid + 1; outM.init_spi := spi_id; outM.resp_spi := spi.peer_spi_id; outM.id_i := i; outM.auth := auth; if NO_NATS_ALLOWED then outM.no_nats_allowed_source := outM.source; outM.no_nats_allowed_dest := outM.dest; endif; outM.mobike_s := true; outM.from_intruder := false; outM.session_key := spi.session_key; multisetadd (outM,net); spi.msgid := outM.msgid; initiator_spi[spi_id] := spi; end; else put "initiator received unsolicited MOBIKE_2 message\n"; end; case MOBIKE_4: if (spi.in_use = true & spi.peer = inM.source & spi.peer_spi_id = inM.resp_spi & spi.state = MOBIKE_4) then -- First check correctness of received message if inM.id_r != spi.peer then put "initiator: incorrect id_r\n"; continue_MOBIKE := false; end; if spi.peer_msgid != inM.msgid then put "initiator: mismatch of msgid\n"; continue_MOBIKE := false; end; -- Check the auth payload undefine auth; auth := inM.auth; if auth.ke.random != spi.peer_ke.random | auth.nonce != spi.peer_nonce | auth.spi != spi.peer_spi_id | auth.peer_nonce != spi.nonce | auth.id_p != spi.peer | auth.shared_secret != SharedSecret | auth.msgid != spi.peer_msgid - 1 then put "initiator: invalid auth payload\n"; continue_MOBIKE := false; end; if continue_MOBIKE = true then spi.peer_msgid := inM.msgid + 1; spi.state := MOBIKE_ADDR_CHANGE; initiator_spi[spi_id] := spi; end; else put "initiator received unsolicited MOBIKE_4 message\n"; end; endswitch; end; end; end; ruleset i: InitiatorIdP do ruleset spi_id: SpiId do rule 20 "initiator address change (step 6)" initiator_spi[spi_id].in_use = true & initiator_spi[spi_id].state = MOBIKE_ADDR_CHANGE ==> var outM: Message; -- outgoing message spi: Spi; begin undefine outM; undefine spi; spi := initiator_spi[spi_id]; put "received addr change message\n"; outM.source := i; outM.dest := spi.peer; outM.init_spi := spi.spi_id; outM.resp_spi := spi.peer_spi_id; outM.mType := MOBIKE_5; outM.from_intruder := false; if NO_NATS_ALLOWED then outM.no_nats_allowed_source := outM.source; outM.no_nats_allowed_dest := outM.dest; end; outM.msgid := spi.msgid + 1; outM.session_key := spi.session_key; multisetadd (outM,net); initiator_spi[spi_id].msgid := outM.msgid; initiator_spi[spi_id].state := MOBIKE_6; end; end; end; -- initiator prime main process ruleset i: InitiatorIdP do choose j: net do rule 20 "initiator_p main process" net[j].dest = i ==> var outM: Message; -- outgoing message inM: Message; -- incoming message spi_id: SpiId; spi: Spi; begin inM := net[j]; multisetremove (j,net); spi_id := inM.init_spi; spi := initiator_spi[spi_id]; if spi.peer_msgid != inM.msgid then put "initiator: mismatch of msgid\n"; else switch inM.mType case MOBIKE_6: if (spi.in_use = true & spi.peer = inM.source & spi.peer_spi_id = inM.resp_spi & spi.state = MOBIKE_6) then put "initiator received expected MOBIKE_6 message\n"; spi.peer_msgid := inM.msgid + 1; spi.state := MOBIKE_7; initiator_spi[spi_id] := spi; else put "initiator received unsolicited MOBIKE_6 message\n"; end; case MOBIKE_7: if (spi.in_use = true & spi.peer = inM.source & spi.peer_spi_id = inM.resp_spi & spi.state = MOBIKE_7) then put "initiator received MOBIKE_7 message\n"; undefine outM; outM.source := i; outM.dest := inM.source; outM.init_spi := spi.spi_id; outM.resp_spi := spi.peer_spi_id; outM.mType := MOBIKE_8; outM.cookie := inM.cookie; outM.from_intruder := false; outM.msgid := spi.msgid + 1; outM.session_key := spi.session_key; multisetadd(outM,net); spi.msgid := outM.msgid; spi.peer_msgid := inM.msgid + 1; spi.state := MOBIKE_DONE; initiator_spi[spi_id] := spi; else put "initiator received unsolicited MOBIKE_7 message\n"; end; endswitch; end; -- if/else end; end; end; -------------------------------------------------------------------------------- -- behavior of responders -- responder i reacts to MOBIKE_1 ruleset i: ResponderId do choose j: net do rule 20 "responder main process" net[j].dest = i ==> var outM: Message; -- outgoing message inM: Message; -- incoming message spi: Spi; spi_id: SpiId; auth: Auth; continue_MOBIKE : boolean; begin undefine inM; undefine spi; inM := net[j]; multisetremove (j,net); continue_MOBIKE := true; spi_id := inM.resp_spi; spi := responder_spi[spi_id]; switch inM.mType case MOBIKE_1: -- Create a new SPI based on this message spi := responder_new_spi(); spi.peer := inM.source; spi.peer_spi_id := inM.init_spi; spi.peer_ke := inM.ke_i; spi.peer_nonce := inM.nonce_i; spi.peer_msgid := 0; spi.exponent := new_random(); if spi.peer_msgid != inM.msgid then put "responder: mismatch of msgid\n"; else -- respond to the message undefine outM; outM.source := i; outM.dest := spi.peer; -- identifier of initiator outM.mType := MOBIKE_2; outM.ke_r := make_ke(spi.exponent); outM.nonce_r := new_random(); outM.init_spi := spi.peer_spi_id; outM.resp_spi := spi.spi_id; outM.from_intruder := false; outM.msgid := 0; outM.session_key := spi.session_key; multisetadd (outM,net); -- Update the Spi spi.session_key := make_session_key(inM.ke_i, spi.exponent); put "Responder: session_key: "; put spi.session_key; spi.msgid := outM.msgid; spi.peer_msgid := inM.msgid + 1; spi.nonce := outM.nonce_r; spi.ke := outM.ke_r; spi.state := MOBIKE_3; responder_spi[spi.spi_id] := spi; end; case MOBIKE_3: if (spi.in_use = true & spi.peer = inM.source & spi.peer_spi_id = inM.init_spi & spi.state = MOBIKE_3) then if NO_NATS_ALLOWED then if inM.no_nats_allowed_source != inM.source then put "NO_NATS_ALLOWED, but the MOBIKE_3's "; put "source address changed\n"; continue_MOBIKE := false; end; if inM.no_nats_allowed_dest != inM.dest then put "NO_NATS_ALLOWED, but the MOBIKE_3's "; put "dest address changed\n"; continue_MOBIKE := false; end; end; if inM.id_i != spi.peer then put "responder: incorrect id_i\n"; continue_MOBIKE := false; end; if spi.peer_msgid != inM.msgid then put "responder: mismatch of msgid\n"; continue_MOBIKE := false; end; -- Check the auth payload undefine auth; auth := inM.auth; if auth.ke.random != spi.peer_ke.random | auth.nonce != spi.peer_nonce | auth.spi != spi.peer_spi_id | auth.peer_nonce != spi.nonce | auth.id_p != spi.peer | auth.msgid != spi.peer_msgid - 1 | auth.shared_secret != SharedSecret then put "responder: invalid auth payload\n"; continue_MOBIKE := false; end; if continue_MOBIKE then -- Create the Auth payload undefine auth; auth.ke := spi.ke; auth.nonce := spi.nonce; auth.peer_nonce := spi.peer_nonce; auth.spi := spi.spi_id; auth.id_p := i; auth.shared_secret := SharedSecret; auth.msgid := spi.msgid; undefine outM; outM.source := i; outM.dest := spi.peer; -- identifier of initiator outM.mType := MOBIKE_4; outM.init_spi := spi.peer_spi_id; outM.resp_spi := spi.spi_id; outM.id_r := i; outM.auth := auth; outM.mobike_s := true; outM.from_intruder := false; outM.msgid := spi.msgid + 1; outM.session_key := spi.session_key; multisetadd (outM,net); spi.msgid := outM.msgid; spi.peer_msgid := inM.msgid + 1; spi.state := MOBIKE_5; responder_spi[spi.spi_id] := spi; end; else put "responder received unsolicited MOBIKE_3 message\n"; end; case MOBIKE_5: if (spi.in_use = true & spi.peer_spi_id = inM.init_spi & spi.state = MOBIKE_5) then if NO_NATS_ALLOWED then if inM.no_nats_allowed_source != inM.source then put "NO_NATS_ALLOWED, but the MOBIKE_5's "; put "source address changed\n"; continue_MOBIKE := false; end; if inM.no_nats_allowed_dest != inM.dest then put "NO_NATS_ALLOWED, but the MOBIKE_5's "; put "dest address changed\n"; continue_MOBIKE := false; end; end; if spi.peer_msgid != inM.msgid then put "responder: mismatch of msgid\n"; continue_MOBIKE := false; end; if continue_MOBIKE then -- Update the spi spi.peer := inM.source; -- And acknowledge the address change undefine outM; outM.source := i; outM.dest := spi.peer; -- identifier of initiator outM.mType := MOBIKE_6; outM.init_spi := spi.peer_spi_id; outM.resp_spi := spi.spi_id; outM.from_intruder := false; outM.msgid := spi.msgid + 1; outM.session_key := spi.session_key; multisetadd (outM,net); spi.msgid := outM.msgid; spi.peer_msgid := inM.msgid + 1; spi.state := MOBIKE_7; responder_spi[spi.spi_id] := spi; end; else put "responder received unsolicited MOBIKE_5 message\n"; end; case MOBIKE_8: if (spi.in_use = true & spi.peer = inM.source & spi.peer_spi_id = inM.init_spi & spi.state = MOBIKE_8) then assert(inM.cookie = spi.cookie); if spi.peer_msgid != inM.msgid then put "responder: mismatch of msgid\n"; else put "Cookie received, we're done\n"; spi.peer_msgid := inM.msgid + 1; responder_spi[spi.spi_id].state := MOBIKE_DONE; end; else put "responder received unsolicited MOBIKE_8 message\n"; end; endswitch; end; end; end; ruleset i: ResponderId do ruleset j: SpiId do rule 20 "responder sub process" responder_spi[j].in_use = true & responder_spi[j].state = MOBIKE_7 & multisetcount(l:net, true) < NetworkSize ==> var outM: Message; -- outgoing message spi: Spi; begin undefine spi; undefine outM; spi := responder_spi[j]; outM.source := i; outM.dest := spi.peer; -- identifier of initiator outM.mType := MOBIKE_7; outM.init_spi := spi.peer_spi_id; outM.resp_spi := spi.spi_id; outM.cookie := new_random(); -- random cookie for outM.from_intruder := false; -- res[i].cookie := outM.cookie; outM.msgid := spi.msgid + 1; outM.session_key := spi.session_key; multisetadd (outM,net); spi.cookie := outM.cookie; spi.msgid := outM.msgid; spi.state := MOBIKE_8; responder_spi[j] := spi; end; end; end; -------------------------------------------------------------------------------- -- behavior of intruders -- intruder i intercepts messages ruleset i: IntruderId do choose j: net do rule 10 "intruder intercepts" !ismember (net[j].source, IntruderId) & !net[j].from_intruder ==> var temp: Message; begin alias msg: net[j] do -- message to intercept if msg.dest = i then -- message is to intruder i -- do nothing for now else -- learn message alias messages: int[i].messages do temp := msg; if multisetcount (l:messages, -- add only if not there messages[l].source = temp.source & messages[l].dest = temp.dest & messages[l].mType = temp.mType & ( messages[l].mType = MOBIKE_1 -> messages[l].nonce_i = temp.nonce_i ) & ( messages[l].mType = MOBIKE_2 -> messages[l].nonce_r = temp.nonce_r )) = 0 then multisetadd (temp, int[i].messages); put "Intruder picking up message "; put temp.mType; end; end; -- alias end; -- if/else multisetremove (j,net); end; -- alias end; -- begin end; -- choose end; -- ruleset -- intruder i sends recorded message ruleset i: IntruderId do -- arbitrary choice of ruleset j: AgentId do ruleset k: AgentId do choose msg_index: int[i].messages do -- recorded message rule 90 "intruder sends recorded message" j != k & multisetcount (l:net, true) < NetworkSize ==> var outM: Message; begin alias outM: int[i].messages[msg_index] do outM.from_intruder := true; outM.source := j; outM.dest := k; -- outM.id_r := j; multisetadd (outM,net); -- multisetremove(l, int[i].messages); -- put "Intruder sending message "; -- put outM.mType; end; multisetremove(msg_index, int[i].messages); end; end; end; end; end; -------------------------------------------------------------------------------- -- startstate -------------------------------------------------------------------------------- startstate -- initialize variables next_random := 7; -- initialize initiators initiator_num_spis := 0; undefine initiator_spi; for i: SpiId do initiator_spi[i].ke.random := 0; initiator_spi[i].peer_ke.random := 0; initiator_spi[i].session_key.random := 0; initiator_spi[i].msgid := 0; initiator_spi[i].peer_msgid := 0; initiator_spi[i].nonce := 0; initiator_spi[i].peer_nonce := 0; initiator_spi[i].cookie := 0; initiator_spi[i].exponent := 0; initiator_spi[i].spi_id := i; initiator_spi[i].in_use := false; end; -- initialize responders undefine responder_spi; for i: SpiId do responder_spi[i].ke.random := 0; responder_spi[i].peer_ke.random := 0; responder_spi[i].session_key.random := 0; responder_spi[i].msgid := 0; responder_spi[i].peer_msgid := 0; responder_spi[i].nonce := 0; responder_spi[i].peer_nonce := 0; responder_spi[i].cookie := 0; responder_spi[i].exponent := 0; responder_spi[i].spi_id := i; responder_spi[i].in_use := false; end; -- initialize network undefine net; end; -------------------------------------------------------------------------------- -- invariants -------------------------------------------------------------------------------- invariant "responder correctly authenticated" forall i: InitiatorIdP do forall j: SpiId do initiator_spi[j].in_use = true & initiator_spi[j].state = MOBIKE_DONE & ismember(initiator_spi[j].peer, ResponderId) -> responder_spi[initiator_spi[j].peer_spi_id].in_use = true & responder_spi[initiator_spi[j].peer_spi_id].peer = i & ( responder_spi[initiator_spi[j].peer_spi_id].state = MOBIKE_DONE | responder_spi[initiator_spi[j].peer_spi_id].state = MOBIKE_8 ) end end; invariant "initiator correctly authenticated" forall i: ResponderId do forall j: SpiId do responder_spi[j].in_use = true & responder_spi[j].state = MOBIKE_DONE & ismember(responder_spi[j].peer, InitiatorIdP) -> initiator_spi[responder_spi[j].peer_spi_id].in_use = true & initiator_spi[responder_spi[j].peer_spi_id].peer = i & initiator_spi[responder_spi[j].peer_spi_id].state = MOBIKE_DONE end end; invariant "responder and initiator have same session key" forall i: ResponderId do forall j: SpiId do responder_spi[j].in_use = true & responder_spi[j].state = MOBIKE_DONE & ismember(responder_spi[j].peer, InitiatorIdP) -> initiator_spi[responder_spi[j].peer_spi_id].in_use = true & initiator_spi[responder_spi[j].peer_spi_id].session_key.random = responder_spi[j].session_key.random end end;