-------------------------------------------------------------------------------
--
--  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;

