------------------------------------------------------------------------------- -- -- Murphi Model of the OTR Data Exchange 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 MODIFY_OLD_MACS: true; --Intruder will modify MAC keys on old messages SEND_TO_RANDOM: false; --Intruder will forward messages to random parties CHECK_INTEGRITY: true; --check for violations of message integrity CHECK_DENIABILITY: false; TALK_TO_ADV: false; --intruder also talks as a messenger NumPrincipals: 2; -- number of initiators NumMessages: 4; -- max messages a principal will send NumIntruders: 1; -- number of intruders NetworkSize: 1; -- max. number of outstanding messages in network MaxKnowledge: 10; -- max. number of messages intruder can remember StartSerial: 2; --starting point in conversation NumKeys: NumPrincipals * NumPrincipals * (NumMessages + 2); -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - type PrincipalId: scalarset (NumPrincipals); IntruderId: scalarset (NumIntruders); KeyId: scalarset (MaxKnowledge); AgentId: union {PrincipalId, IntruderId}; val: -1..10; DH_Key: record owner: AgentId; --owner of this key partner: AgentId; --intended partner serial: val; --serial number end; Message : record source: AgentId; -- Source Agent dest: AgentId; -- Destination Agent sender: AgentId; -- nominal sender of the message k_A: DH_Key; -- keyid_A k_B: DH_Key; -- keyid_B k_new: DH_Key; --proposed next dh key k_old_mac: DH_Key; -- public mac value modified: boolean; --intruder has modified malleable parts of message touched : boolean; -- has the intruder fucked with this message yet end; Conversation : record k_our_curr: DH_Key; --our current key k_our_next: DH_Key; k_their_curr: DH_Key; --their key k_their_prev: DH_Key; k_publish: DH_Key; -- expired key needing publication end; Principal : record c: array[AgentId] of Conversation; mcount : val; -- num messages sent by principal end; Intruder : record messages: multiset[MaxKnowledge] of Message; mac_keys: array[AgentId] of array[AgentId] of val; end; -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - var -- state variables net: multiset[NetworkSize] of Message; -- network pri: array[AgentId] of Principal; -- principals int: array[IntruderId] of Intruder; -- intruders published_keys: multiset[NumKeys] of DH_Key; -- published keys -------------------------------------------------------------------------------- -- functions/procedures -------------------------------------------------------------------------------- -- CREATE A NEW MESSAGE procedure send_message(a : AgentId; b : AgentId); var outM: Message; -- outgoing message c: Conversation; begin alias c: pri[a].c[b] do undefine outM; --create the message outM.source := a; outM.dest := b; outM.sender := a; outM.k_A := c.k_our_curr; outM.k_B := c.k_their_curr; outM.k_new := c.k_our_next; outM.touched := false; outM.modified := false; --publish old mac keys if necessary if !isundefined(c.k_publish.serial) then outM.k_old_mac := c.k_publish; undefine c.k_publish; else undefine outM.k_old_mac; end; --send multisetadd (outM,net); --increment message count pri[a].mcount := pri[a].mcount + 1; end; end; -- Equality function for key objects function k_equals(a : DH_Key; b : DH_Key): boolean; begin if (a.owner = b.owner & a.partner = b.partner & a.serial = b.serial) then return true; end; return false; end; -- Max function function max(a : val; b : val): val; begin if a > b then return a; end; return b; end; -------------------------------------------------------------------------------- -- rules -------------------------------------------------------------------------------- -- PRINCIPAL SENDS A MESSAGE ruleset a: AgentId do ruleset b: AgentId do rule 20 "Principal sends a message" pri[a].mcount < NumMessages & multisetcount(l:net,true) < NetworkSize & a != b & (TALK_TO_ADV | (!ismember(a,IntruderId) & !ismember(b, IntruderId))) ==> begin send_message(a,b); end; end; end; -- PRINCIPAL RECEIVES A MESSAGE ruleset i: AgentId do choose j: net do rule 20 "Principal receives a message" net[j].dest = i & multisetcount (l:net, true) > 0 & (ismember(net[j].source,IntruderId) | (TALK_TO_ADV & ismember(net[j].dest,IntruderId))) ==> var sender: AgentId; -- initiator inM: Message; -- incoming message begin alias c : pri[i].c[net[j].sender] do inM := net[j]; sender := inM.sender; multisetremove(j,net); -- Ignore messages bounced back to me if inM.sender = i then return; end; --check for usage of proper keys if (!k_equals(inM.k_B, c.k_our_curr) & !k_equals(inM.k_B, c.k_our_next) | (!k_equals(inM.k_A, c.k_their_curr) & !k_equals(inM.k_A, c.k_their_prev))) then return; end; if(k_equals(inM.k_B, c.k_our_next)) then c.k_publish := c.k_our_curr; c.k_our_curr := c.k_our_next; c.k_our_next.owner := i; c.k_our_next.partner := sender; c.k_our_next.serial := c.k_our_next.serial + 1; else undefine c.k_publish; end; if(inM.k_new.serial = c.k_their_curr.serial + 1 & (c.k_their_curr.serial = c.k_our_curr.serial | c.k_their_curr.serial + 1 = c.k_our_curr.serial)) then c.k_their_prev := c.k_their_curr; c.k_their_curr := inM.k_new; end; if(CHECK_DENIABILITY & !isundefined(inM.k_old_mac.serial)) then multisetadd(inM.k_old_mac, published_keys); end; --MESSAGE ACCEPTED, CHECK INVARIANTS if(CHECK_INTEGRITY & inM.modified) then error "Message Integrity Failed: Honest Principal accepted modified message" end; if(CHECK_DENIABILITY) then if(multisetcount(k: published_keys, published_keys[k].owner = i & published_keys[k].partner = sender & published_keys[k].serial = c.k_our_curr.serial - 2) = 0 | multisetcount(k: published_keys, published_keys[k].owner = sender & published_keys[k].partner = i & published_keys[k].serial = c.k_their_curr.serial - 2) = 0) then error "Strong Deniability Failed" end; end; end; end; end; end; -------------------------------------------------------------------------------- -- behavior of intruders -- INTRUDER INTERCEPT A MESSAGE ruleset i: IntruderId do choose j: net do rule 20 "Intruder Intercepts a Message" !ismember(net[j].dest,IntruderId) & !ismember(net[j].source,IntruderId) & -- not my own msg multisetcount(l:net,true) > 0 & -- there is a message to get multisetcount(l:int[i].messages,true) < MaxKnowledge ==> var temp: Message; source: AgentId; dest: AgentId; begin source := net[j].source; dest := net[j].dest; --Examine published mac keys if(!isundefined(net[j].k_old_mac.serial)) then int[i].mac_keys[source][dest] := max(int[i].mac_keys[source][dest], net[j].k_old_mac.serial); end; multisetadd(net[j],int[i].messages); multisetremove(j,net); end; end; end; -- INTRUDER MODIFIES MALEABLE ENCRYPTION ruleset i: IntruderId do choose j: int[i].messages do rule 20 "Intruder modifies a malleable message with known mac keys" multisetcount(l:int[i].messages,true) > 0 & int[i].messages[j].modified = false & (int[i].mac_keys[int[i].messages[j].source][int[i].messages[j].dest] >= int[i].messages[j].k_A.serial | int[i].mac_keys[int[i].messages[j].dest][int[i].messages[j].source] >= int[i].messages[j].k_B.serial) ==> begin int[i].messages[j].modified := true; end; end; end; -- INTRUDER ALTERS PUBLISHED MAC KEYS ruleset i: IntruderId do choose j: int[i].messages do rule 20 "Intruder alters published MAC keys" MODIFY_OLD_MACS & multisetcount(l:int[i].messages,true) > 0 & int[i].messages[j].touched = false & !isundefined(int[i].messages[j].k_old_mac.serial) ==> begin int[i].messages[j].k_old_mac.owner := i; int[i].messages[j].k_old_mac.serial := -1; int[i].messages[j].touched := true; end; end; end; -- INTRUDER SEND A RECORDED MESSAGE ruleset i: IntruderId do choose j: int[i].messages do ruleset k: AgentId do rule 20 "Intruder sends stored message" !ismember(k,IntruderId) & multisetcount(l:int[i].messages,true) > 0 & multisetcount(l:net,true) < NetworkSize & (SEND_TO_RANDOM | int[i].messages[j].dest = k) ==> var outM: Message; begin outM := int[i].messages[j]; outM.source := i; outM.dest := k; multisetadd(outM,net); multisetremove(j,int[i].messages); end; end; end; end; -------------------------------------------------------------------------------- -- startstate -------------------------------------------------------------------------------- startstate -- start at serial number 2 -- with keys 0 and 1 published undefine published_keys; undefine pri; for i: AgentId do pri[i].mcount := 0; for j: AgentId do if(i != j) then alias c: pri[i].c[j] do c.k_our_curr.owner := i; c.k_our_curr.partner := j; c.k_our_curr.serial := StartSerial - 2; multisetadd(c.k_our_curr, published_keys); c.k_our_curr.serial := StartSerial - 1; multisetadd(c.k_our_curr, published_keys); c.k_our_curr.serial := StartSerial; c.k_our_next.owner := i; c.k_our_next.partner := j; c.k_our_next.serial := StartSerial + 1; c.k_their_curr.owner := j; c.k_their_curr.partner := i; c.k_their_curr.serial := StartSerial; c.k_their_prev.owner := j; c.k_their_prev.partner := i; c.k_their_prev.serial := StartSerial - 1; undefine c.k_publish; end; end; end; end; -- initialize intruders undefine int; for i: IntruderId do for j: AgentId do for k: AgentId do int[i].mac_keys[j][k] := StartSerial - 1; end; end; end; -- initialize network undefine net; end;