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


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
const
  VERBOSE:                false; -- whether to print out all actions
  REGENERATE_CHANNEL_KEY: true;  -- whether to regenerate channel keys
  MAL_CLIENTS:            true;  -- whether an intruder has a partner client
  MAL_SERVERS:            false; -- whether an intruder has a partner server
  INTERCEPT_ALL:          false; -- if false, only intercept msgs and newkeys
                                 -- and don't intercept intruder msgs or
                                 -- messages from/to partners
  NumClients:          2;  -- number of client nodes
  NumServers:          1;  -- number of server nodes
  NumIntruders:        1;  -- number of intruder nodes
  NumChannels:         1;  -- number of channels a server has
  NumChannelKeys:      5;  -- number of keys a channel has
  NumMessages:         2;  -- number of sent messages a client stores
  NumIntruderMessages: 2;  -- number of messages that an intruder can store
  NetworkSize:         5;  -- number of commands the network holds

-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
type
  ClientId:     scalarset (NumClients);   -- client identifier
  ServerId:     scalarset (NumServers);   -- server identifier
  IntruderId:   scalarset (NumIntruders); -- intruder identifier
  ChannelId:    scalarset (NumChannels);  -- channel identifier
  ChannelKeyId: 0..NumChannelKeys;        -- channel key identifier
                                          -- (not a scalar set
                                          -- because individual ones need to be
				          -- referenced)
  MsgId:        0..NumMessages;           -- message identifier (not a scalar
					  -- set because individual ones need
					  -- to be referenced)

  -- generic agent identifier
  AgentId:      union {ClientId, ServerId, IntruderId};

  -- all the commands that may be sent
  CommandType : enum {
    C_Join,
    C_Part,
    C_NewChannelKey,
    C_Msg
  };

  -- a command "packet"
  Command : record
    -- each command has a source, a destination, intended destination.

    -- packet header (always encrypted with (source, intDest)
    source:  AgentId; -- source
    dest:    AgentId; -- destination
    intDest: AgentId; -- intended destination

    -- packet payload (usually encrypted with (source, intDest)
    -- if cType = C_Msg, encrypted with (channel, channelKey)
    cType:  CommandType;

    -- Common parameters: all commands reference a channel
    channel: ChannelId;

    -- NewKey and Msg parameters: the ID of the new key
    channelKey: ChannelKeyId;

    -- Message-only parameters: the ID of the sent message
    message:   MsgId;

    -- Intruder-only parameters
    origSource: AgentId; -- original source of message
    origDest:   AgentId; -- original dest of message

    -- whether or not partner client was joined in the channel at time of message
    sentWhilePartnerClientJoined: boolean;
  end;

  -- the client data record for a channel
  ChannelRecord : record
    channel:    ChannelId;
    joined:     boolean;  -- if the client is joined to this channel
    channelKey: ChannelKeyId; -- the key as the client sees it
  end;

  -- the client stores the its partner server,
  -- the set of channels it is waiting to join, the records of the
  -- channel it has joined, how many messages it has sent,
  -- and the messages it has sent.
  Client : record
    partnerServer:  ServerId;
    numMsgs:        MsgId; -- also serves as next message to send
    lastSeenMsg:    Command;
    wtjChannels:    multiset[NumChannels] of ChannelId;
    channelRecords: multiset[NumChannels] of ChannelRecord;
    messagesSent:   multiset[NumMessages] of Command;

    -- only used if malicious
    partnerIntruder: IntruderId;
  end;

  -- a channel roster is the server data record for a channel.
  -- it has the current channel
  -- key, and the clients that are joined to that channel, represented
  -- as an array of ClientIds (true means joined)
  ChannelRoster : record
    channelKey: ChannelKeyId;
    clients:    array[AgentId] of boolean; -- cannot be a multiset because
		                           -- of sendChannelKey
		                           -- should be array of AgentId
		                           -- but if so, breaks for some reason
  end;

  -- a server is just an array of channel rosters
  Server : record
    channels: array[ChannelId] of ChannelRoster;

    -- only used if malicious
    partnerIntruder: IntruderId;
  end;

  -- an intruder contains a partnerClient and a partnerServer,
  -- either which may be undefined, and a set of intercepted messages
  Intruder : record
    partnerClient: ClientId;
    partnerServer: ServerId;
    messages:      multiset[NumIntruderMessages] of Command;
  end;

-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
var
  -- the network itself
  net: multiset[NetworkSize] of Command;
  -- the clients
  cli: array[ClientId] of Client;
  -- the servers
  svr: array[ServerId] of Server;
  -- the intruders
  int: array[IntruderId] of Intruder;

--------------------------------------------------------------------------------
-- procedures
--------------------------------------------------------------------------------

-- returns true iff the given channel has no members
function channelEmpty(var channel: ChannelRoster): boolean;
begin
  for i:AgentId do
    if channel.clients[i] then 
      return false;
    end;
  end;
  return true;
end;

-- generates a new key for a channel
-- should not be called directly
procedure incrementChannelKey(var kid: ChannelKeyId);
if isundefined(kid) then
    kid := 0;
  else
    kid := kid + 1;
  end;
end;

-- regenerates a new channel key only if REGENERATE_CHANNEL_KEY is on.
procedure regenerateChannelKey(var kid: ChannelKeyId);
  if REGENERATE_CHANNEL_KEY then
    incrementChannelKey(kid);
  end;
end;

function validChannelKey(var kid:ChannelKeyId): boolean;
  return !REGENERATE_CHANNEL_KEY | isundefined(kid) | (kid != NumChannelKeys)
end;

-- sends the channel key to all joined clients for a channel
procedure sendChannelKey(sid: ServerId; hid: ChannelId);
  var
    outC: Command;

  begin
  for j:ClientId do
    if svr[sid].channels[hid].clients[j] then
      undefine outC;
      outC.source     := sid;
      outC.dest       := j;
      outC.intDest    := j;
      outC.cType      := C_NewChannelKey;
      outC.channel    := hid;
      outC.channelKey := svr[sid].channels[hid].channelKey;

      multisetadd(outC, net);

      if VERBOSE then
        put " -- NEW_KEY -->\n";
        put outC; put "\n";
      end;
    end;
  end;
end;

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

-- the main protocol
		       
/*
 Precondition:
 The client has no partner.

 Action:
 The client picks an arbitrary server.

 Postcondition:
 The client has an arbitrary server as a partner.
 */
ruleset i: ClientId do
  ruleset j: ServerId do
    rule 10 "client connects to server (step 1)"
      isundefined(cli[i].partnerServer)
    ==>
    begin
      cli[i].partnerServer := j;

      if VERBOSE then
        put i; put " -- CONNECT --> "; put j; put "\n\n";
      end;
    end; 
  end;
end;   

/*
 Precondition:
  The client has a partner, has not already joined the channel, is
  not already waiting to join the channel, and the network is empty.

 Action:
  The client sends a join command to a its partner to join a channel.

 Postcondition:
  The channel is added to the wait list.  The network has a new
  join message as described above.
*/
ruleset i: ClientId do
  ruleset j: ChannelId do
    rule 20 "client joins channel (step 2a)"
      -- has a partner
      !isundefined(cli[i].partnerServer) &
      -- has not already joined channel
      multisetcount(k:cli[i].channelRecords,
	              cli[i].channelRecords[k].channel = j) = 0 &
      -- is not waiting for the channel
      multisetcount(k:cli[i].wtjChannels,
    	              cli[i].wtjChannels[k] = j) = 0 &
      -- network is empty
      multisetcount(k:net, true) = 0
    ==>
      var
        outC: Command;

      begin
      undefine outC;
      outC.source     := i;
      outC.dest       := cli[i].partnerServer;
      outC.intDest    := cli[i].partnerServer;
      outC.cType      := C_Join;
      outC.channel    := j;

      multisetadd(outC, net);

      if VERBOSE then
        put i; put " -- JOIN -->\n";
        put outC;
      end;
		       
      multisetadd(j, cli[i].wtjChannels);
      if VERBOSE then
        put j; put " -> "; put i; put ".wtjChannels\n\n";
      end;
    end;
  end;
end;

/*
 Precondition:
  There is a message for the server from a client wishing to join
  a channel, and that client
  is not already in that channel.  Also, the network has just the join message.
  Finally, key is valid.

 Action:
  The message is removed from the network.  The client is added to the channel.
  The key is incremented if it was not initialized.

 Postcondition:
  The channel exists with the client in the channel.  A new
  key has been created. The message is no longer on the network.
*/
ruleset i: ServerId do
  ruleset j:ChannelId do
    choose k:net do
      rule 21 "server reacts to client's join command (step 2b)"
        -- join message from client for the server
        net[k].dest    = i &
        net[k].intDest = i &
        net[k].cType   = C_Join &
        net[k].channel = j &
        -- not already in the channel
        !svr[i].channels[j].clients[net[k].source] &
        -- just the join msesage exists
        multisetcount(m:net, true) = 1 &
	-- key valid
	validChannelKey(svr[i].channels[j].channelKey)
      ==>
      begin
        if VERBOSE then
          put "-- JOIN --> "; put i; put "\n";
          put net[k];
        end;

        regenerateChannelKey(svr[i].channels[j].channelKey);

        if VERBOSE then
          put "Key is "; put svr[i].channels[j].channelKey;
          put "Adding client to channel.\n\n";
        end;

        svr[i].channels[j].clients[net[k].source] := true;

        multisetremove(k, net);

        sendChannelKey(i, j);
      end;
    end;
  end;
end;

/*
 Precondition:
  The new key message is from the client's partner and the client is
  waiting for the channel.

 Action:
  The client joins the channel with the given key.

 Postcondition:
  The client has the most current key for the given channel.  Message
  is removed from network.
 */
ruleset i: ClientId do
  choose j: cli[i].wtjChannels do
    choose k:net do
      rule 22 "client receives new key (step 2c.1)"
        -- from client's partner to the client
        net[k].source  = cli[i].partnerServer &
        net[k].dest    = i &
        net[k].intDest = i &
        net[k].cType   = C_NewChannelKey &
        -- client waiting for channel
        net[k].channel = cli[i].wtjChannels[j]
      ==>
      var
        rec: ChannelRecord;

      begin
        undefine rec;
        rec.joined     := true;
        rec.channel    := cli[i].wtjChannels[j];
        rec.channelKey := net[k].channelKey;

        multisetremove(j, cli[i].wtjChannels);

        multisetadd(rec, cli[i].channelRecords);

        if VERBOSE then
          put " -- NEW_KEY --> "; put i; put "\n";
          put net[k];
          put "Channel joined\n\n";
        end;

        multisetremove(k, net);
      end;
    end;
  end;
end;

/*
 Precondition:
  The new key message is from the client's partner to the client
  and the client is in the channel.

 Action:
  It updates the channel key from the given key.

 Postcondition:
  The client has the most current key for the given channel.  Message
  is removed from network.
 */
ruleset i: ClientId do
  choose j:net do
    choose k:cli[i].channelRecords do
      rule 23 "client receives new key (step 2c.2)"
        -- from client's partner to the client
        net[j].source  = cli[i].partnerServer &
        net[j].dest    = i &
        net[j].intDest = i &
        net[j].cType   = C_NewChannelKey &
        -- client is in the channel
        net[j].channel = cli[i].channelRecords[k].channel
      ==>
      begin
        cli[i].channelRecords[k].channelKey := net[j].channelKey;

        if VERBOSE then
          put " -- NEW_KEY --> "; put i; put "\n";
          put net[j];
          put "Channel key updated\n\n";
        end;

        multisetremove(j, net);
      end;
    end;
  end;
end;

/* 
 Precondition:
   The client is in a channel on the server. The network is empty.  The
   client has messages left to send.

 Action:
   Sends a message for the channel to its partner.
   Stores the message sent in its multiset of sent
   messages. Increments the number of messages sent.

 Postcondition:
   The sent message is saved by the client. A new message is generated in
   the network.
*/

ruleset i: ClientId do
  choose j: cli[i].channelRecords do
    rule 30 "Client sends a message (Step 3a)"
      -- messages left to send
      multisetcount(k:cli[i].messagesSent, true) < NumMessages &
      -- client is joined to channel
      cli[i].channelRecords[j].joined &
      -- network is empty
      multisetcount(k:net, true) = 0
    ==>
    var 
      outC: Command;
      
    begin
      undefine outC;
      outC.source     := i;
      outC.dest       := cli[i].partnerServer;
      outC.intDest    := cli[i].partnerServer;
      outC.cType      := C_Msg;
      outC.channel    := cli[i].channelRecords[j].channel;
      outC.channelKey := cli[i].channelRecords[j].channelKey;
      outC.message    := cli[i].numMsgs;

      cli[i].numMsgs  := cli[i].numMsgs + 1;

      if VERBOSE then
        put i; put " -- MSG -->\n";
        put outC; put "\n";
      end;

      multisetadd(outC, net);
         
      -- adding message to client's sent list
      multisetadd(outC, cli[i].messagesSent);
    end;
  end;
end;  


/* 
 Precondition:
   There is a message for the server from a client on a channel.
   The network has only the msg command.

 Action:
   Sends the message to all clients in the channel (including
   the one that sent the original message).

 Postaction:
   New messages are generated in the net for each client subscribed to
   that channel.
*/
ruleset i: ServerId do
  ruleset j:ChannelId do
    choose k:net do
      rule 31 "server reacts to client's msg command (step 3b)"
	-- message to server from client
        net[k].dest    = i &
        net[k].intDest = i &
        net[k].cType   = C_Msg &
        net[k].channel = j &
	-- client is in the channel
        svr[i].channels[j].clients[net[k].source] &
        -- only command on network
	multisetcount(m:net, true) = 1
      ==>
      var
	outC:       Command;
        message:    MsgId;
        channelKey: ChannelKeyId;

      begin
        if VERBOSE then
          put "-- MSG --> "; put i; put "\n";
          put net[k];
        end;

        message := net[k].message;
        channelKey := net[k].channelKey;
        multisetremove(k, net);
 
        -- sends messages to all subscribed clients
        for l:ClientId do
          if svr[i].channels[j].clients[l] then
  	    undefine outC;
            outC.source     := i;
            outC.dest       := l;
            outC.intDest    := l;
            outC.cType      := C_Msg;
            outC.channel    := j;
            outC.channelKey := channelKey;
            outC.message    := message;
      
            multisetadd(outC, net);

            if VERBOSE then
	      put i; put " -- MSG -->\n";
              put outC; put "\n";
            end;
          end;
        end;
      end;
    end;
  end;
end;


/* 
 Precondition:
   There is a message for the client from the partner for a channel that it
   is in.

 Action:
   If client has the key,
   the client updates its last seen message to this message.

 Postcondition:
   The message is removed from the network and the last seen message by
   this client is set to this message if client had the key.
*/

ruleset i: ClientId do
  choose j: net do
    rule 32 "client receives message (step 3c)"
      -- for client from partner
      net[j].source  = cli[i].partnerServer &
      net[j].dest    = i &
      net[j].intDest = i &
      net[j].cType   = C_Msg &
      -- client in channel
      (multisetcount(k:cli[i].channelRecords,
	               cli[i].channelRecords[k].channel = net[j].channel &
                       cli[i].channelRecords[k].joined) > 0)
    ==>
    begin	
      if multisetcount(k:cli[i].channelRecords,
	       	         cli[i].channelRecords[k].channelKey
			 = net[j].channelKey) > 0 then
        if VERBOSE then
          put " -- MSG --> "; put i; put "\n";
          put net[j]; put "\n";
        end;

        cli[i].lastSeenMsg := net[j];
      end;

      -- remove it from the net no matter what
      multisetremove(j, net);   
    end;
  end;
end;

/*
 Precondition:
  The client is in a channel and the network is empty.

 Action:
  The client sends a part message for the channel to its partner.

  Postcondition:
   The client is not in the channel anymore.  The network
   has a new part message as described above.  lastSeenMsg is nullified.
   (This is necessary to assure that the client cannot read "old" messages)
 */
ruleset i: ClientId do
  choose j: cli[i].channelRecords do
    rule 40 "Client leaves the channel (Step 4a)"
      -- client is in channel
      cli[i].channelRecords[j].joined &
      -- network is empty
      multisetcount(m:net, true) = 0
    ==>
    var 
      outC: Command;
      
    begin
      undefine outC;
      outC.source  := i;
      outC.dest    := cli[i].partnerServer;
      outC.intDest := cli[i].partnerServer;
      outC.cType   := C_Part;
      outC.channel := cli[i].channelRecords[j].channel;

      if VERBOSE then
        put i; put " -- PART -->\n";
        put outC; put "\n";
      end;

      multisetadd(outC, net);
         
      cli[i].channelRecords[j].joined := false;
      undefine cli[i].lastSeenMsg; 
    end;
  end;
end;
      
/*
 Precondition:
  There is a message for the server from a client wishing to part
  a channel, and that channel already exists and the client is subscribed
  to that channel.  The network has just the part command.  Channel key
  is valid.

 Action:
  The message is removed from the network. The client is removed from the 
  channel.  The key is regenerated and
  sent to all the remaining clients in the channel.

 Postcondition:
  The client is removed from the channel. The key has been sent to all
  other clients
  and the message is no longer in the network.
*/
ruleset i: ServerId do
  ruleset j:ChannelId do
  choose k:net do
      rule 41 "server reacts to client's part command (step 4b)"
	-- to server from client
        net[k].dest    = i &
        net[k].intDest = i &
        net[k].cType   = C_Part &
        net[k].channel = j &
	-- client in channel
        svr[i].channels[j].clients[net[k].source] &
	-- network only has this command
	multisetcount(m:net, true) = 1 &
	-- key valid
	validChannelKey(svr[i].channels[j].channelKey)
      ==>
      begin
        if VERBOSE then
          put "-- PART --> "; put i; put "\n";
          put net[k];
        end;

        -- remove client from this channel
        svr[i].channels[j].clients[net[k].source] := false;
   
        -- check if channel is empty
        if channelEmpty(svr[i].channels[j]) then
          if VERBOSE then
            put "resulting channel is empty.";
            put "\n\n";
          end;
        else 
          -- channel not empty --> have to generate new key
 
          -- increments key if we are regenerating keys
          regenerateChannelKey(svr[i].channels[j].channelKey);

          if VERBOSE then
            put "Changing key to ";
            put svr[i].channels[j].channelKey; put "\n\n";
          end;
        end;

        multisetremove(k, net);

        sendChannelKey(i, j);
      end;
    end;
  end;
end;

-- intruder rules

-- intruder can pick a client to work with if MAL_CLIENTS is on
ruleset i: IntruderId do
  ruleset j: ClientId do
    rule 100 "intruder picks a client to work with"
      MAL_CLIENTS &
      isundefined(int[i].partnerClient)
    ==>
    begin
      int[i].partnerClient   := j;
      cli[j].partnerIntruder := i;
    end; 
  end;
end;

-- intruder can pick a server to work with if MAL_SERVERS is on
ruleset i: IntruderId do
  ruleset j: ServerId do
    rule 101 "intruder picks a server to work with"
      MAL_SERVERS &
      isundefined(int[i].partnerServer)
    ==>
    begin
      int[i].partnerServer   := j;
      svr[j].partnerIntruder := i;
    end; 
  end;
end;
		       
-- intruder can intercept and store any command sent between clients and servers
ruleset i: IntruderId do
  choose j: net do
    rule 110 "intruder intercepts command"
      !ismember (net[j].source, IntruderId) &
      multisetcount(k:int[i].messages, true) < NumIntruderMessages &
      (INTERCEPT_ALL |
       ((net[j].cType = C_NewChannelKey | net[j].cType = C_Msg) &
       !ismember(net[j].source, IntruderId) &
       !ismember(net[j].dest, IntruderId) &
       ((isundefined(int[i].partnerClient) |
        (net[j].source != int[i].partnerClient &
         net[j].dest != int[i].partnerClient)) &
        (isundefined(int[i].partnerServer) |
         (net[j].source != int[i].partnerServer &
          net[j].dest != int[i].partnerServer)))))
    ==>
    begin
      if !isundefined(int[i].partnerClient) &
         !isundefined(cli[int[i].partnerClient].partnerServer) then
        net[j].sentWhilePartnerClientJoined :=
          svr[cli[int[i].partnerClient].partnerServer].channels[net[j].channel].
	      clients[int[i].partnerClient]
      end;

      multisetadd(net[j], int[i].messages);

      multisetremove(j, net);
    end;  
  end;
end;

-- intruder can show a message to its partner client (if network is empty)
-- and message was sent after intruder picked partner client
ruleset i: IntruderId do
  choose j: int[i].messages do
    rule 110 "intruder shows a message to its partner client"
      !isundefined(int[i].partnerClient) &
      int[i].messages[j].cType = C_Msg &
      multisetcount(k:net, true) = 0 &
      !isundefined(int[i].messages[j].sentWhilePartnerClientJoined)
    ==>
    var outC: Command;

    begin
      undefine outC;
      outC.source     := i;
      outC.dest       := int[i].partnerClient;
      outC.intDest    := int[i].partnerClient;
      outC.cType      := int[i].messages[j].cType;
      outC.channel    := int[i].messages[j].channel;
      outC.channelKey := int[i].messages[j].channelKey;
      outC.message    := int[i].messages[j].message;
      outC.origSource := int[i].messages[j].source;
      outC.origDest   := int[i].messages[j].dest;

      -- intruder might have intercepted message before picking client
      outC.sentWhilePartnerClientJoined :=
        int[i].messages[j].sentWhilePartnerClientJoined;

      multisetadd(outC, net);
    end;
  end;
end;

ruleset i: ClientId do
  choose j: net do
    rule 111 "malicious client receives message from partner intruder"
      -- from partner intruder
      ismember(net[j].source, IntruderId) &
      cli[i].partnerIntruder = net[j].source &
      net[j].dest    = i &
      net[j].intDest = i &
      net[j].cType   = C_Msg
    ==>
    begin	
      if multisetcount(k:cli[i].channelRecords,
		       cli[i].channelRecords[k].channelKey
		       = net[j].channelKey) > 0 then

        if VERBOSE then
          put " -- (MAL) MSG --> "; put i; put "\n";
          put net[j]; put "\n";
        end;

        cli[i].lastSeenMsg := net[j];
      end;

      multisetremove(j, net);   
    end;
  end;
end;

-- intruder forwards the message to its intended recipient when it's
-- finished with it		       
ruleset i: IntruderId do
  choose j: int[i].messages do
    rule 120 "intruder forwards a message that it saved"
      multisetcount(k:net, true) = 0
    ==>
    begin
      undefine int[i].messages[j].sentWhilePartnerClientJoined;

      multisetadd(int[i].messages[j], net);

      multisetremove(j, int[i].messages);
    end;
  end;
end;
	       
-- invariants
invariant "if client is joined, server thinks its joined"
  forall i: ServerId do
    forall j: ChannelId do
      forall k: ClientId do
        cli[k].partnerServer = i &
        multisetcount(l:cli[k].channelRecords,
                      cli[k].channelRecords[l].channel = j &
                      cli[k].channelRecords[l].joined) > 0
        ->
        svr[i].channels[j].clients[k]
      end
    end
  end;

invariant "if server thinks client is not joined, client is not joined"
  forall i: ServerId do
    forall j: ChannelId do
      forall k: ClientId do
        cli[k].partnerServer = i &
        !svr[i].channels[j].clients[k]
        ->
        multisetcount(l:cli[k].channelRecords,
                      cli[k].channelRecords[l].channel = j &
                      cli[k].channelRecords[l].joined) = 0
      end
    end
  end;

invariant "if client receives a message from a client, this message must be sent by the source of this message"
  forall i: ClientId do
    forall j: ClientId do
      !isundefined(cli[i].lastSeenMsg.source) &
      cli[i].lastSeenMsg.source = j
      ->
      multisetcount(k:cli[j].messagesSent, cli[j].messagesSent[k].message
	            = cli[i].lastSeenMsg.message) > 0
      
    end
  end;

invariant "if client receives a message that it has the channel key for and keys are not regenerated, it must be joined to that channel"
  forall i: ClientId do
    -- is message
    !isundefined(cli[i].lastSeenMsg.cType) &
    cli[i].lastSeenMsg.cType = C_Msg &
    -- has channel key
    multisetcount(k:cli[i].channelRecords,
                  cli[i].channelRecords[k].channel = cli[i].lastSeenMsg.channel &
                  cli[i].channelRecords[k].channelKey =
                  cli[i].lastSeenMsg.channelKey) > 0 &
    !REGENERATE_CHANNEL_KEY
    ->
    multisetcount(k:cli[i].channelRecords,
                  cli[i].channelRecords[k].channel = cli[i].lastSeenMsg.channel &
                  cli[i].channelRecords[k].joined) > 0
  end;

invariant "if client receives a message from a server that it has the channel key for and keys are regenerated, it must be joined to that channel or it must have the most current key"
  forall i: ClientId do
    -- is message
    !isundefined(cli[i].lastSeenMsg.cType) &
    cli[i].lastSeenMsg.cType = C_Msg &
    -- message from server
    !isundefined(cli[i].lastSeenMsg.source) &
    ismember(cli[i].lastSeenMsg.source, ServerId) &
    -- has channel key
    multisetcount(k:cli[i].channelRecords,
                  cli[i].channelRecords[k].channel = cli[i].lastSeenMsg.channel &
                  cli[i].channelRecords[k].channelKey =
                  cli[i].lastSeenMsg.channelKey) > 0 &
    REGENERATE_CHANNEL_KEY
    ->
    -- either it's joined to channel
    multisetcount(k:cli[i].channelRecords,
                  cli[i].channelRecords[k].channel = cli[i].lastSeenMsg.channel &
                  cli[i].channelRecords[k].joined) > 0 |
    -- or it has the most current key
    (ismember(cli[i].lastSeenMsg.source, ServerId) &
     multisetcount(k:cli[i].channelRecords,
                   cli[i].channelRecords[k].channelKey =
                   svr[cli[i].lastSeenMsg.source].channels[cli[i].
                     channelRecords[k].channel].
                   channelKey) > 0)
  end;

invariant "if client receives a message from its partner intruder that it has the channel key for and keys are regenerated, it must be joined to that channel or it must have been sent while client was joined or it has the most current key or it sent the message or was meant to receive it"
  forall i: ClientId do
    -- is message
    !isundefined(cli[i].lastSeenMsg.cType) &
    cli[i].lastSeenMsg.cType = C_Msg &
    -- message from partner intruder
    ismember(cli[i].lastSeenMsg.source, IntruderId) &
    cli[i].partnerIntruder = cli[i].lastSeenMsg.source &
    -- has channel key
    multisetcount(k:cli[i].channelRecords,
                  cli[i].channelRecords[k].channel = cli[i].lastSeenMsg.channel &
                  cli[i].channelRecords[k].channelKey =
                  cli[i].lastSeenMsg.channelKey) > 0 &
    REGENERATE_CHANNEL_KEY
    ->
    -- either it's joined to channel
    multisetcount(k:cli[i].channelRecords,
                  cli[i].channelRecords[k].channel = cli[i].lastSeenMsg.channel &
                  cli[i].channelRecords[k].joined) > 0 |
    -- or sent while client was joined
    cli[i].lastSeenMsg.sentWhilePartnerClientJoined |
    -- or has most current key
    (ismember(cli[i].lastSeenMsg.origSource, ServerId) &
     multisetcount(k:cli[i].channelRecords,
                   cli[i].channelRecords[k].channelKey =
                   svr[cli[i].lastSeenMsg.origSource].channels[cli[i].
                     channelRecords[k].channel].
                   channelKey) > 0) |
    (ismember(cli[i].lastSeenMsg.origDest, ServerId) &
     multisetcount(k:cli[i].channelRecords,
                   cli[i].channelRecords[k].channelKey =
                   svr[cli[i].lastSeenMsg.origDest].channels[cli[i].
                     channelRecords[k].channel].
                   channelKey) > 0) |
    (ismember(cli[i].lastSeenMsg.origSource, ClientId) &
    cli[i].lastSeenMsg.origSource = i) |
    (ismember(cli[i].lastSeenMsg.origDest, ClientId) &
    cli[i].lastSeenMsg.origDest = i)
  end;

-- initialization
startstate
  -- initialize clients
  undefine cli;

  for i: ClientId do
    undefine cli[i].partnerServer;
    cli[i].numMsgs := 0
  end;

  -- initialize servers
  undefine svr;
  for i: ServerId do
    for j: ChannelId do
      -- leave key undefined so it'll be 0 when first initialized if
      -- REGENERATE_CHANNEL_KEY is on.  Otherwise, initialize to 0.
      if !REGENERATE_CHANNEL_KEY then
        svr[i].channels[j].channelKey := 0;
      end;

      for k: AgentId do
        svr[i].channels[j].clients[k] := false
      end
    end
  end;

  -- initialize intruders
  undefine int;

  -- initialize network
  undefine net;
end;
