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