--------------------------------------------------------------------------------
--
--  Murphi Model of the Enclaves protocol
--
--------------------------------------------------------------------------------
--
--  version:      1.0
--
--  written by:   Mohamed Layouni
--  date:         Jul 2002
--  affiliation:  HVG Group - ECE Dept., Concordia University
--
--------------------------------------------------------------------------------
--
--  Only the following first three steps of Enclaves "Authentication Module" are modeled:
--
--
--
--   1. A->Li: AuthInitReq,A,Li,{A,Li,Nai}Pai
--   2. Li->A: AuthKeyDist,Li,A,{Li,A,Nai,Nli,Kai}Pai     
--   3. A->Li: AuthAckKey,A,Li,{A,Li,Nli,N'ai}Kai            
--   4. Li->A: AuthCommit,Li,A,{Li,A,N'ai,GK}Kai  -- Once accepted in the group,
						  -- client A is provided with 
						  -- the group key GK
--
--   "A" denotes a client, "Li" the i(th) leader, and "GK" the group key 
--

--------------------------------------------------------------------------------
-- constants, types and variables
--------------------------------------------------------------------------------


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
const

  NumClients:      3;   -- number of clients
  NumLeaders:      1;   -- number of leaders/servers
  NumIntruders:    1;   -- number of intruders
  NetworkSize:     2;   -- max. number of outstanding messages in network
  MaxKnowledge:    3;   -- max. number of messages intruder can remember

-- experimental results
--
-- clients  ---  leaders --- intruder ---- net size --- cpu
--
--    2             4           2              2         ? 
--
--    3             6           1              2         ?
--
--    3             8           2              2         ?
--
--    2             4           2              4         ?
--                 
-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
type
  ClientId:  	scalarset (NumClients);   -- identifiers
  LeaderId:  	scalarset (NumLeaders);
  IntruderId:   scalarset (NumIntruders);
  
  AgentId:      union {ClientId, LeaderId, IntruderId};

  MessageType : enum {          -- different types of messages
    M_AuthInitReq,              --  AuthInitReq,A,Li,{A,Li,Nai}Pai 
    M_AuthKeyDist,              --  AuthKeyDist,Li,A,{Li,A,Nai,Nli,Kai}Pai
    M_AuthAckKey               --  AuthAckKey,A,Li,{A,Li,Nli,N'li}Kai
--    M_AuthCommit		--  AuthCommit,Li,A,{Li,A,N'ai,GK}Kai
  };

  Message : record
    mType:    MessageType;       -- type of message	
    psource:   AgentId;          -- plain source of message
    pdest:     AgentId;          -- plain intended destination of message
    csource:   AgentId;          -- ciphered source of message
    cdest:     AgentId;          -- ciphered intended destination of message
    key:      AgentId;           -- key used for encryption    
    nonce1:   AgentId;           -- nonce1
    nonce2:   AgentId;           -- nonce2 OR empty
    sessionKey: AgentId;	 -- Session Key shared by the leader and the 
    				 -- client,OR empty    
--    address:  AgentId;           -- sender identifier
  end;

  -- remark: keys, nonces and addresses are encoded in the message by their
  --         agent's identifier only. They can be distinguished by their po-
  --         sition and the type of the message
  

  ClientStates : enum {
    C_SLEEP,                  -- state after initialization
    C_WAIT,                   -- waiting for response from leader
    C_ACK		      -- acknowledging the session key
  };                          -- (thinks leaders authenticated him)

  Client : record
    state:  ClientStates;
    leader: AgentId;          -- Leader with whom the client starts the
  end;                        --  protocol

  LeaderStates : enum {
    L_SLEEP,
    L_WAIT,
    L_COMMIT
  };

  Leader : record
    state: LeaderStates;
    client: AgentId;
  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
  clnt: array[ClientId] of Client;     --  clients
  lead: array[LeaderId] of Leader;     --  leaders
  int: array[IntruderId] of Intruder;       --  intruders



--------------------------------------------------------------------------------
-- rules
--------------------------------------------------------------------------------


--------------------------------------------------------------------------------
-- behavior of clients

-- client i starts protocol with leader or intruder j (step 1)
ruleset i: ClientId do
  ruleset j: AgentId do
    rule 20 "client starts protocol (step 1)"

      clnt[i].state = C_SLEEP &
      !ismember(j,ClientId) &               -- only leaders and intruders
      multisetcount (l:net, true) < NetworkSize

    ==>
    
    var
      outM: Message;   -- outgoing message

    begin
      undefine outM;
      outM.psource  := i;
      outM.csource  := i;
      outM.pdest    := j;
      outM.cdest    := j;
      outM.key     := j;
      outM.mType   := M_AuthInitReq;
      outM.nonce1  := i;
--      outM.nonce2  := i;

      multisetadd (outM,net);

      clnt[i].state     := C_WAIT;
      clnt[i].leader := j;
    end;
  end;
end;

-- client i reacts to nonce received (steps 2/3)
ruleset i: ClientId do
  choose j: net do
    rule 20 "client reacts to nonce received (steps 2/3)"

      clnt[i].state = C_WAIT &
      net[j].pdest = i &
      ismember(net[j].psource,IntruderId)
    ==>

    var
      outM: Message;   -- outgoing message
      inM:  Message;   -- incoming message

    begin
      inM := net[j];
      multisetremove (j,net);

      if inM.key=i then   -- message is encrypted with i's key

        if inM.mType= M_AuthKeyDist then   -- correct message type
          if (inM.nonce1=i &                     -- correct nonce and source
             inM.csource=clnt[i].leader) then
            undefine outM;
            outM.psource  := i;
	    outM.csource  := i;
            outM.pdest    := clnt[i].leader;
	    outM.cdest    := clnt[i].leader;
            outM.key     := inM.sessionKey;
            outM.mType   := M_AuthAckKey;
            outM.nonce1  := inM.nonce2;

            multisetadd (outM,net);

            clnt[i].state := C_ACK;
          else
            --error "Client received incorrect nonce"
          end;
        end;

      end;
    end;
  end;
end;


--------------------------------------------------------------------------------
-- behavior of Leaders

-- leader i reacts to initiator's nonce (steps 1/2)
ruleset i: LeaderId do
  choose j: net do
    rule 20 "Leader reacts to client's nonce (steps 1/2)"

      lead[i].state = L_SLEEP &
      net[j].pdest = i &
      ismember(net[j].psource,IntruderId)

    ==>

    var
      outM: Message;   -- outgoing message
      inM:  Message;   -- incoming message

    begin
      inM := net[j];
      multisetremove (j,net);

      if inM.key=i then   -- message is encrypted with i's key
        if inM.mType= M_AuthInitReq then   -- correct message type
          undefine outM;
          outM.psource  := i;
	  outM.csource  := i;
          outM.pdest    := inM.psource;   -- identifier of initiator
          outM.key     := inM.key;
          outM.mType   := M_AuthKeyDist;
          outM.nonce1  := inM.nonce1;
          outM.nonce2  := i;
--          outM.address := i;
	  outM.sessionKey :=i;
	  
          multisetadd (outM,net);

          lead[i].state     := L_WAIT;
          lead[i].client := inM.nonce1;
        end;
      end;

    end;
  end;
end;

-- Leader i reacts to own nonce (step 3)
ruleset i: LeaderId do
  choose j: net do
    rule 20 "leader reacts to own nonce (step 3)"

      lead[i].state = L_WAIT &
      net[j].pdest = i &
      ismember(net[j].psource,IntruderId)

    ==>

    begin
      alias inM: net[j] do   -- incoming message

        if inM.key=i then   -- message is encrypted with i's key

          if inM.mType= M_AuthAckKey then   -- correct message type
            if inM.nonce1=i then   -- correct nonce received
              lead[i].state := L_COMMIT;
            else
              --error "leader received incorrect nonce"
            end;
          end;

        end;

        multisetremove (j,net);
      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].psource, IntruderId)    -- not for intruders' messages

      ==>

      var
        temp: Message;

      begin
        alias msg: net[j] do   -- message to intercept
        alias intruderknowledge: int[i].messages do  
        if multisetcount (f:intruderknowledge, true) < MaxKnowledge then 
          if msg.key=i then   -- message is encrypted with i's key
            int[i].nonces[msg.nonce1] := true;     -- learn nonces
            if msg.mType= M_AuthKeyDist  then
              int[i].nonces[msg.nonce2] := true;
            end;              
	    
--	    if multisetcount (l:msg,   -- add only if not there
--                   msg[l].key = temp.key & 
--                   msg[l].mType = temp.mType &
--                   msg[l].nonce1 = temp.nonce1 &
--                   ( messages[l].mType != M_AuthInitReq ->
--                     messages[l].nonce2 = temp.nonce2 ) &
--                   ( messages[l].mType = M_AuthKeyDist ->
--                     messages[l].sessionKey = temp.sessionKey ) ) = 0 then
--                multisetadd (temp, int[i].messages);
--	    end;
	    
          else                                     -- learn message
            alias messages: int[i].messages do
              temp := msg;
              undefine temp.psource;   -- delete useless information
              undefine temp.pdest;
              if multisetcount (l:messages,   -- add only if not there
                   messages[l].psource = temp.psource & 
		   messages[l].pdest = temp.pdest &
                   messages[l].mType = temp.mType &
		   messages[l].key = temp.key & 
                   messages[l].mType = temp.mType &
                   messages[l].nonce1 = temp.nonce1 &
                   ( messages[l].mType != M_AuthInitReq ->
                     messages[l].nonce2 = temp.nonce2 ) &
                   ( messages[l].mType = M_AuthKeyDist ->
                     messages[l].sessionKey = temp.sessionKey ) ) = 0 then
                multisetadd (temp, int[i].messages);
              end;
            end;
          end;
         end; -- end if < Maxknowledge
          multisetremove (j,net);
        end;
      end;
   end;
 end;
end;

-- intruder i sends recorded message
ruleset i: IntruderId do         -- arbitrary choice of
  choose j: int[i].messages do   --  recorded message
    ruleset k: AgentId do        --  destination
      rule 90 "intruder sends recorded message"

        !ismember(k, IntruderId) &                 -- not to intruders
        multisetcount (l:net, true) < NetworkSize

      ==>

      var
        outM: Message;

      begin
        outM        := int[i].messages[j];
        outM.psource := i;
        outM.pdest   := k;

        multisetadd (outM,net);
      end;
    end;
  end;
end;

-- intruder i generates message with the nonces it knows
ruleset i: IntruderId do       -- arbitrary choice of
 ruleset j: AgentId do         --  destination = key
  ruleset l: MessageType do    --  message type
   ruleset m: AgentId do       --  nonce1
    ruleset n: AgentId do      --  nonce2
       ruleset k: AgentId do   --  SessionKey
      rule 90 "intruder generates message"

        !ismember(j, IntruderId) &       -- not to intruders
        int[i].nonces[m] = true &        -- nonces must be known
        int[i].nonces[n] = true &
        multisetcount (t:net, true) < NetworkSize

      ==>

      var
        outM: Message;

      begin
        undefine outM;
        outM.psource := i;
	outM.csource := i;
        outM.pdest   := j;
	outM.cdest   := j;
        outM.key    := j;
        outM.mType  := l;

        switch l   -- set content dependent on message type
        case M_AuthAckKey:
          outM.nonce1 := m;
          outM.nonce2 := n;
        case M_AuthKeyDist:
          outM.nonce1  := m;
          outM.nonce2  := n;
          outM.sessionKey := k;
        case M_AuthInitReq:
          outM.nonce1 := m;
        end;

        multisetadd (outM,net);
      end;
     end;
    end;
   end;
  end;
 end;
end; 
         


--------------------------------------------------------------------------------
-- startstate
--------------------------------------------------------------------------------

startstate
  -- initialize clients
  undefine clnt;
  for i: ClientId do
    clnt[i].state     := C_SLEEP;
    clnt[i].leader := i;
  end;

  -- initialize leaders
  undefine lead;
  for i: LeaderId do
    lead[i].state  := L_SLEEP;
    lead[i].client := 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;
    end;
    int[i].nonces[i] := true;
  end;

  -- initialize network 
  undefine net;
end;



--------------------------------------------------------------------------------
-- invariants
--------------------------------------------------------------------------------

-- invariant "leaders correctly authenticated"
--  forall i: ClientId do
--    clnt[i].state = C_ACK &
--    ismember(clnt[i].leader, LeaderId)
--    ->
--    lead[clnt[i].leader].client = i &
--    ( lead[clnt[i].leader].state = L_WAIT |
--      lead[clnt[i].leader].state = L_COMMIT )
--  end;

invariant "client correctly authenticated"
  forall i: LeaderId do
    lead[i].state = L_COMMIT &
    ismember(lead[i].client, ClientId)
    ->
    clnt[lead[i].client].leader = i &
    clnt[lead[i].client].state = C_ACK
  end;
