-------------------------------------------------------------------------------- -- -- Murphi Model of the OTR Protocol -- -------------------------------------------------------------------------------- -- -- version: 1.0 -- -- written by: Andrew Morrison and Joe Bonneau -- date: Feb 2006 -- -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- constants, types and variables -------------------------------------------------------------------------------- -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - const INIT_TO_ADV: true; --Initiator will talk to adversary INTERCEPTS: true; --Intruder can intercept messages CHECK_IDENT_BINDING: false; --check for identity binding flaw NumInitiators: 1; -- number of initiators NumResponders: 1; -- number of responders NumIntruders: 1; -- number of intruders NetworkSize: 1; -- max. number of outstanding messages in network MaxKnowledge: 10; -- max. number of messages intruder can remember -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - type InitiatorId: scalarset (NumInitiators); -- identifiers ResponderId: scalarset (NumResponders); IntruderId: scalarset (NumIntruders); AgentId: union {InitiatorId, ResponderId, IntruderId}; MessageType : enum { -- different types of messages M_DHCommit, -- E_r(g^x), H(g^x) M_DHKey, -- g^y M_RevealSig, -- ... M_Sig -- ... }; KeyKnowledge : enum { K_none, -- No key knowledge K_x, -- Knowledge of x K_gx, -- Knowledge of g^x K_Hash_gx -- Knowledge of Hash(g^x) }; Message : record source: AgentId; -- Source Agent dest: AgentId; -- Destination Agent dhkey1: AgentId; dhkey2: AgentId; --Encryption and MACing based on two DH keys signkey: AgentId; --public key used for signature content1: AgentId; --four content slots, message dependent content2: AgentId; content3: AgentId; content4: AgentId; mType: MessageType; -- Type of message end; InitiatorStates : enum { I_SLEEP, -- state after initialization I_WAIT_DHKey, -- waiting for M_DHKey message I_WAIT_Sig, --waiting for M_Sig message I_COMMIT -- initiator commits to session }; Initiator : record state: InitiatorStates; serial: AgentId; keyId: AgentId; --what DHKey is actually seen responder: AgentId; -- agent with whom the initiator starts the end; ResponderStates : enum { R_SLEEP, R_WAIT_RevealSig, R_COMMIT }; Responder : record state: ResponderStates; serial: AgentId; initiator: AgentId; hashId: AgentId; --what hash value is seen in first message keyId: AgentId; --what DHKey is actually seen nonceId: AgentId; --what nonce is actually seen end; Intruder : record nonces: array[AgentId] of boolean; -- known nonces dhkeys: array[AgentId] of KeyKnowledge; -- known DH keys messages: multiset[MaxKnowledge] of Message; -- known messages end; -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - var -- state variables for net: multiset[NetworkSize] of Message; -- network ini: array[InitiatorId] of Initiator; -- initiators res: array[ResponderId] of Responder; -- responders int: array[IntruderId] of Intruder; -- intruders -------------------------------------------------------------------------------- -- rules -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- behavior of initiators ruleset i: InitiatorId do ruleset j: AgentId do rule 20 "Initiator sends DHCommit message" ini[i].state = I_SLEEP & !ismember(j,InitiatorId) & --only send to adversary if allowed to (INIT_TO_ADV | !ismember(j, IntruderId)) & multisetcount (l:net, true) < NetworkSize ==> var outM: Message; -- outgoing message begin undefine outM; outM.source := i; outM.dest := j; outM.mType := M_DHCommit; outM.content1 := i; --key being encrypted outM.content2 := i; --r value used outM.content3 := i; --hash value being sent outM.content4 := i; --source of message multisetadd (outM,net); ini[i].state := I_WAIT_DHKey; ini[i].responder := j; end; end; end; ruleset i: InitiatorId do choose j: net do rule 20 "Initiator reacts to DHKey message" ini[i].state = I_WAIT_DHKey & net[j].dest = i & net[j].mType = M_DHKey & (ismember(net[j].source,IntruderId) | !INTERCEPTS) ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); ini[i].keyId := inM.content1; undefine outM; outM.source := i; outM.dest := ini[i].responder; outM.dhkey1 := i; outM.dhkey2 := ini[i].keyId; outM.signkey := i; outM.mType := M_RevealSig; outM.content1 := i; --owner of g^x outM.content2 := ini[i].keyId; --owner of g^y outM.content3 := i; --serial number outM.content4 := i; --nonceId multisetadd (outM,net); ini[i].state := I_WAIT_Sig; end; end; end; ruleset i: InitiatorId do choose j: net do rule 20 "Initiator reacts to Sig message" ini[i].state = I_WAIT_Sig & net[j].dest = i & net[j].mType = M_Sig & (ismember(net[j].source,IntruderId) | !INTERCEPTS) ==> var inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); if (inM.dhkey1=i & inM.dhkey2=ini[i].keyId) then if inM.signkey=ini[i].responder then -- message is signed with correct key if (inM.content1=i & inM.content2=ini[i].keyId) then ini[i].serial := inM.content3; ini[i].state := I_COMMIT; else -- error "Sig message signed wrong DH keys" end; else -- error "Sig message signed incorrectly" end; else -- error "Sig message used wrong DH keys" end; end; end; end; -------------------------------------------------------------------------------- -- behavior of responders -- responder i reacts to initiators nonce (steps 3/6) ruleset i: ResponderId do choose j: net do rule 20 "Responder reacts to DHCommit message" res[i].state = R_SLEEP & net[j].dest = i & net[j].mType = M_DHCommit & (ismember(net[j].source,IntruderId) | !INTERCEPTS) ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); res[i].keyId := inM.content1; --owner of encrypted DH key res[i].nonceId := inM.content2; --owner of received nonce res[i].hashId := inM.content3; res[i].initiator := inM.content4; --apparent initiator undefine outM; outM.source := i; outM.dest := res[i].initiator; -- identifier of initiator outM.mType := M_DHKey; outM.content1 := i; multisetadd (outM,net); res[i].state := R_WAIT_RevealSig; end; end; end; ruleset i: ResponderId do choose j: net do rule 20 "Responder reacts to RevealSig message" res[i].state = R_WAIT_RevealSig & net[j].dest = i & net[j].mType = M_RevealSig & (ismember(net[j].source,IntruderId) | !INTERCEPTS) ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); if inM.content4 = res[i].nonceId then if res[i].keyId = res[i].hashId then if (inM.dhkey1 = res[i].keyId & inM.dhkey2=i) then if inM.signkey = res[i].initiator then -- message is signed with correct key if (inM.content1=res[i].keyId & inM.content2=i) then undefine outM; outM.source := i; outM.dest := res[i].initiator; outM.dhkey1 := res[i].keyId; outM.dhkey2 := i; outM.signkey := i; outM.mType := M_Sig; outM.content1 := res[i].keyId; --owner of g^x outM.content2 := i; --owner of g^y outM.content3 := i; --serial number multisetadd (outM,net); res[i].serial := inM.content3; res[i].state := R_COMMIT; else -- error "Reveal Sig message signed wrong DH keys" end; else -- error "Reveal Sig message signed incorrectly" end; else -- error "Reveal Sig message used wrong DH keys" end; else -- error "After seeing Reveal Sig, hashed value not equal to encrypted DHKey " end; else -- error "Reveal Sig message sent wrong r value" end; 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) & -- not for intruders messages (INTERCEPTS | net[j].dest = i) --must be intended for intruder --ifintercepting is disabled ==> var temp: Message; begin alias msg: net[j] do -- message to intercept alias messages: int[i].messages do if msg.mType = M_DHCommit then if int[i].dhkeys[msg.source] = K_none then int[i].dhkeys[msg.source] := K_Hash_gx; end; end; if msg.mType = M_DHKey then if int[i].dhkeys[msg.source] != K_x then int[i].dhkeys[msg.source] := K_gx; end; end; if msg.mType = M_RevealSig then int[i].nonces[msg.source] := true; if int[i].dhkeys[msg.source] != K_x then int[i].dhkeys[msg.source] := K_gx; end; end; temp := msg; undefine temp.source; -- delete useless information undefine temp.dest; if multisetcount (l:messages, -- add only if not there messages[l].mType = temp.mType & ((messages[l].mType = M_RevealSig | messages[l].mType = M_Sig) -> messages[l].dhkey1 = temp.dhkey1 & messages[l].dhkey2 = temp.dhkey2 & messages[l].signkey = temp.signkey) & messages[l].content1 = temp.content1 & ( messages[l].mType != M_DHKey -> messages[l].content2 = temp.content2) & ( messages[l].mType != M_DHKey -> messages[l].content3 = temp.content3) & ( (messages[l].mType = M_RevealSig | messages[l].mType = M_DHCommit) -> messages[l].content4 = temp.content4)) = 0 then multisetadd (temp, int[i].messages); end; end; multisetremove (j,net); end; end; end; end; ruleset i: IntruderId do -- arbitrary choice of choose j: int[i].messages do -- recorded message ruleset k: AgentId do -- destination rule 90 "intruder sends pre-recorded Sig message" !ismember(k, IntruderId) & -- not to intruders multisetcount (l:net, true) < NetworkSize & int[i].messages[j].mType = M_Sig ==> var outM: Message; begin outM := int[i].messages[j]; outM.source := i; outM.dest := k; multisetadd (outM,net); end; end; end; end; ruleset i: IntruderId do -- arbitrary choice of ruleset k: AgentId do -- destination ruleset u: AgentId do -- first dh-key ruleset v: AgentId do -- second dh-key rule 90 "intruder creates and sends Sig message" !ismember(k, IntruderId) & -- not to intruders multisetcount (l:net, true) < NetworkSize & ((int[i].dhkeys[u] = K_x & int[i].dhkeys[v] = K_gx) | (int[i].dhkeys[v] = K_x & int[i].dhkeys[u] = K_gx)) ==> var outM: Message; begin undefine outM ; outM.source := i; outM.dest := k; outM.dhkey1 := u; outM.dhkey2 := v; outM.signkey := i; outM.mType := M_Sig; outM.content1 := u; --owner of g^x outM.content2 := v; --owner of g^y outM.content3 := i; --serial number multisetadd (outM,net); end; end; end; end; end; ruleset i: IntruderId do -- arbitrary choice of ruleset k: AgentId do -- destination ruleset n: AgentId do -- nonce used ruleset u: AgentId do -- first dh-key ruleset v: AgentId do -- second dh-key rule 90 "intruder creates and sends RevealSig message" !ismember(k, IntruderId) & -- not to intruders multisetcount (l:net, true) < NetworkSize & int[i].nonces[n] & ((int[i].dhkeys[u] = K_x & int[i].dhkeys[v] = K_gx) | (int[i].dhkeys[v] = K_x & int[i].dhkeys[u] = K_gx)) ==> var outM: Message; begin undefine outM ; outM.source := i; outM.dest := k; outM.dhkey1 := u; outM.dhkey2 := v; outM.signkey := i; outM.mType := M_RevealSig; outM.content1 := u; --owner of g^x outM.content2 := v; --owner of g^y outM.content3 := i; --serial number outM.content4 := n; --nonceId multisetadd (outM,net); end; end; end; end; end; end; ruleset i: IntruderId do -- arbitrary choice of choose j: int[i].messages do -- recorded message ruleset k: AgentId do -- destination ruleset w: AgentId do -- nonce used rule 90 "intruder sends modified RevealSig message" !ismember(k, IntruderId) & -- not to intruders multisetcount (l:net, true) < NetworkSize & int[i].messages[j].mType = M_RevealSig & int[i].nonces[w] ==> var outM: Message; begin outM := int[i].messages[j]; outM.source := i; outM.dest := k; outM.content4 := w; multisetadd (outM,net); end; end; end; end; end; ruleset i: IntruderId do -- arbitrary choice of choose j: int[i].messages do -- recorded message ruleset k: AgentId do -- destination ruleset w: AgentId do -- dh_key used used rule 90 "intruder sends modified DHKey message" !ismember(k, IntruderId) & -- not to intruders multisetcount (l:net, true) < NetworkSize & int[i].messages[j].mType = M_DHKey & (int[i].dhkeys[w] = K_gx | int[i].dhkeys[w] = K_x) ==> var outM: Message; begin outM := int[i].messages[j]; outM.source := i; outM.dest := k; outM.content1 := w; multisetadd (outM,net); end; end; end; end; end; ruleset i: IntruderId do -- arbitrary choice of choose j: int[i].messages do -- recorded message ruleset k: AgentId do -- destination ruleset w: AgentId do -- written as the source ruleset u: AgentId do -- key encrypted ruleset v: AgentId do --nonce used rule 90 "intruder sends modified DHCommit" !ismember(k, IntruderId) & -- not to intruders multisetcount (l:net, true) < NetworkSize & int[i].messages[j].mType = M_DHCommit & (((int[i].dhkeys[u] = K_gx | int[i].dhkeys[u] = K_x) & int[i].nonces[v]) | (int[i].messages[j].content1 = u & int[i].messages[j].content2 = v & int[i].messages[j].content3 = u )) ==> var outM: Message; begin outM := int[i].messages[j]; outM.source := i; outM.dest := k; outM.content1 := u; outM.content2 := v; outM.content3 := u; outM.content4 := w; multisetadd (outM,net); end; end; end; end; end; end; end; -------------------------------------------------------------------------------- -- startstate -------------------------------------------------------------------------------- startstate -- initialize initiators undefine ini; for i: InitiatorId do ini[i].state := I_SLEEP; ini[i].responder := i; ini[i].keyId := i; ini[i].serial := i end; -- initialize responders undefine res; for i: ResponderId do res[i].state := R_SLEEP; res[i].initiator := i; res[i].keyId := i; res[i].nonceId := i; res[i].serial := i; end; -- initialize intruders undefine int; for i: IntruderId do -- the only nonce known is the own one for j: AgentId do int[i].nonces[j] := false; int[i].dhkeys[j] := K_none; end; int[i].nonces[i] := true; int[i].dhkeys[i] := K_x; end; -- initialize network undefine net; end; -------------------------------------------------------------------------------- -- invariants -------------------------------------------------------------------------------- invariant "responder correctly authenticated" forall i: InitiatorId do ini[i].state = I_COMMIT & ismember(ini[i].responder, ResponderId) -> res[ini[i].responder].initiator = i & res[ini[i].responder].state = R_COMMIT end; invariant "initiator correctly authenticated" forall i: ResponderId do res[i].state = R_COMMIT & ismember(res[i].initiator, InitiatorId) & CHECK_IDENT_BINDING -> ini[res[i].initiator].responder = i & (ini[res[i].initiator].state = I_WAIT_Sig | ini[res[i].initiator].state = I_COMMIT) end; invariant "initiator receives correct DH key" forall i: InitiatorId do ini[i].state = I_COMMIT & ismember(ini[i].responder, ResponderId) -> ini[i].keyId = ini[i].responder end; invariant "responder receives correct DH key" forall i: ResponderId do res[i].state = R_COMMIT & ismember(res[i].initiator, InitiatorId) -> res[i].keyId = res[i].initiator end; invariant "initiator receives correct serial number" forall i: InitiatorId do ini[i].state = I_COMMIT & ismember(ini[i].responder, ResponderId) -> ini[i].serial = ini[i].responder end; invariant "responder receives correct serial number" forall i: ResponderId do res[i].state = R_COMMIT & ismember(res[i].initiator, InitiatorId) -> res[i].serial = res[i].initiator end; invariant "responder commits with intruder" forall i: ResponderId do res[i].state = R_COMMIT & false -> !ismember(res[i].initiator, IntruderId) end; invariant "initiator commits with intruder" forall i: InitiatorId do ini[i].state = I_COMMIT & false -> !ismember(ini[i].responder, IntruderId) end;