


-- ------------------------------------------------------------------------------
type
  InitiatorId:  scalarset (NumInitiators);   -- identifiers
  ResponderId:  scalarset (NumResponders);
  IntruderId:   scalarset (NumIntruders);
  
  AgentId:      union {InitiatorId, ResponderId, IntruderId};

  MessageType : enum {
    M_Hello,
    M_HashCommit,
    M_DH,
    M_SAS,
    M_INIT_CONVERSATION,
    M_RESP_CONVERSATION
  };

  Message : record
    source:    AgentId;            -- source of message
    dest:      AgentId;            -- intended destination of message
    zid:       AgentId;            -- sender identifier or voice
    mType:     MessageType;        -- type of message
    hash:      AgentId;         -- hash commitment OR hash of shared secret or voice text
    publicDH:  AgentId;         -- a DH public value
    privateDH: AgentId;         -- the pair of publicDH and privateDH specify who can decrypt the message
    responseTo: AgentId;        -- for M_{INIT,RESP}_CONVERSATION, refers to who generated the text this is a response to.
  end;

  InitiatorStates : enum {
    I_SLEEP,                     -- state after initialization, or after first run of protocol is complete
    I_WAIT,                      -- waiting for hash commit from responder
    I_SENT_DH,                   -- waiting for DH response
    I_COMMIT,                    -- initiator commits to session
    I_READYTOTALK,               -- initiator is ready to talk
    I_DONE                       -- initiator has said "yo, what's up?" and heard a response.
  };                            

  Initiator : record
    state:          InitiatorStates;
    responder:      AgentId;          -- agent with whom the initiator starts the protocol
    responderDH:    AgentId;          -- public DH value of other side
    responderSASVoice:  AgentId;   -- the voice of the responder in SAS
    responderConvVoice: array[AgentId] of AgentId;   -- the voice of the responder in conversation
    responderConvTextSender: array[AgentId] of AgentId;   -- the text generator of the responder in conversation
    resSharedSecret:    array[AgentId] of AgentId;   -- the secret we share with the responder

    connectedBefore:    boolean;          -- only used to prevent the state space from exploding
  end;                          

  ResponderStates : enum {
    R_SLEEP,                      -- state after initialization, or after first run of protocol is complete
    R_HASH_COMMITTED,             -- committed to hash value waiting for DH
    R_COMMIT,                     -- received DH message and sent off own DH
    R_READYTOTALK,                -- responder is ready to talk
    R_DONE                        -- responder has heard "yo, what's up?" and responded.
  };

  Responder : record
    state:          ResponderStates;
    initiator:      AgentId;
    initiatorDH:    AgentId;

    initiatorSASVoice:  AgentId;   -- the voice of the initiator in SAS
    initiatorConvVoice: array[AgentId] of AgentId;   -- the voice of the initiator in conversation
    initiatorConvTextSender: array[AgentId] of AgentId;   -- the text generator of the initiator in conversation
    iniSharedSecret:    array[AgentId] of AgentId;   -- the secret we share with the responder

    connectedBefore:    boolean;          -- only used to prevent the state space from exploding
  end;

  Intruder : record
    conversationtext: array[AgentId] of array[AgentId] of AgentId;
  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 "initiator starts protocol"

      ini[i].state = I_SLEEP &
      !ismember(j,InitiatorId) &               -- only responders and intruders
      multisetcount (l:net, true) < NetworkSize

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

    begin
      undefine outM;
      outM.source  := i;
      outM.dest    := j;
      outM.zid     := i;
      outM.mType   := M_Hello;

      multisetadd (outM,net);

      ini[i].state     := I_WAIT;
      ini[i].responder := j;
    end;
  end;
end;

ruleset i: InitiatorId do
  choose j: net do
    rule "initiator reacts to M_HashCommit received"

      ini[i].state = I_WAIT &
      net[j].dest = i &
      !ismember(net[j].source,InitiatorId)    -- talk to everyone but initiators
    ==>

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

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

      if inM.mType = M_HashCommit then        -- correct message type
        if inM.zid = ini[i].responder then   -- correct zid

          undefine outM;
          outM.source   := i;
          outM.dest     := ini[i].responder;
          outM.mType    := M_DH;
          outM.publicDH := i;
          outM.hash      := i;                 -- we put our id in as the shared secret

          multisetadd (outM,net);

          ini[i].state := I_SENT_DH;
        end;
      end;

    end;
  end;
end;

ruleset i: InitiatorId do
  choose j: net do
    rule "initiator reacts to M_DH"

      ini[i].state = I_SENT_DH &
      net[j].dest = i &
      !ismember(net[j].source,InitiatorId)    -- talk to everyone but initiators
    ==>

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

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

      if inM.mType = M_DH then        -- correct message type
        ini[i].responderDH := inM.publicDH;

        undefine outM;

        -- if we share a secret with the responer, go straight to voice traffic
        -- the hash holds the secret that we supposedly share
        if ini[i].resSharedSecret[ini[i].responder] = inM.hash then
          outM.source    := i;
          outM.dest      := ini[i].responder;
          outM.mType     := M_INIT_CONVERSATION;
          outM.publicDH  := ini[i].responderDH;
          outM.privateDH := i;
          outM.zid       := i; -- voice
          outM.hash      := i; -- text of conversation
          outM.responseTo := ini[i].responder;

          multisetadd (outM,net);

          ini[i].state := I_READYTOTALK;

        else
          outM.source    := i;
          outM.dest      := ini[i].responder;
          outM.mType     := M_SAS;
          outM.publicDH  := ini[i].responderDH;
          outM.privateDH := i;
          outM.zid       := i;
          outM.hash      := i;                 -- we put our id in as the shared secret

          multisetadd (outM,net);

          ini[i].state := I_COMMIT;
        end;
      end;

    end;
  end;
end;

ruleset i: InitiatorId do
  choose j: net do
    rule "initiator reacts to M_SAS"

      ini[i].state = I_COMMIT &
      net[j].dest = i &
      !ismember(net[j].source,InitiatorId)    -- talk to everyone but initiators

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

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

        if  inM.mType = M_SAS
          & inM.publicDH = i
          & inM.privateDH = ini[i].responderDH
          & (InitiatorUnawareOfRespondersVoiceInAdvance | ini[i].responder = inM.zid) then

          undefine outM;
          outM.source    := i;
          outM.dest      := ini[i].responder;
          outM.mType     := M_INIT_CONVERSATION;
          outM.publicDH  := ini[i].responderDH;
          outM.privateDH := i;
          outM.zid       := i; -- voice
          outM.hash      := i; -- text of conversation
          outM.responseTo := ini[i].responder;

          ini[i].state := I_READYTOTALK;
          ini[i].responderSASVoice := inM.zid;
          ini[i].resSharedSecret[ini[i].responder] := inM.hash;

          multisetremove (j,net);
          multisetadd (outM,net);
        else
          multisetremove (j,net);
        end;
      end;
    end;
  end;
end;


ruleset i: InitiatorId do
  choose j: net do
    rule "initiator reacts to M_RESP_CONVERSATION"

      ini[i].state = I_READYTOTALK &
      net[j].dest = i &
      !ismember(net[j].source,InitiatorId)    -- talk to everyone but initiators

    ==>

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

        if  inM.mType = M_RESP_CONVERSATION
          & inM.publicDH = i
          & inM.privateDH = ini[i].responderDH 
          & inM.responseTo = i
          & (inM.zid = ini[i].responderSASVoice | 
                 (isUndefined(ini[i].responderSASVoice) & (InitiatorForgetsVoiceBetweenSessions | inM.zid = ini[i].responderConvVoice[ini[i].responder])))
          & (InitiatorUnawareOfRespondersVoiceInAdvance | (ini[i].responder = inM.zid & ini[i].responder = inM.hash)) then

          ini[i].responderConvVoice[ini[i].responder] := inM.zid;
          ini[i].responderConvTextSender[ini[i].responder] := inM.hash;

          -- if we haven't connected before, then set it and go back to beginning
          if !ini[i].connectedBefore then

            ini[i].connectedBefore := true;
            ini[i].state := I_SLEEP;
            undefine ini[i].responderSASVoice;

          else 
            ini[i].state := I_DONE;
          end;
        end;

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





-- ------------------------------------------------------------------------------
-- behavior of responders
-- ------------------------------------------------------------------------------

ruleset i: ResponderId do
  choose j: net do
    rule "responder reacts to initiator's M_Hello"

      res[i].state = R_SLEEP &
      net[j].dest = i &
      !ismember(net[j].source, ResponderId)

    ==>

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

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

      if inM.mType = M_Hello then   -- correct message type
        undefine outM;
        outM.source  := i;
        outM.dest    := inM.zid;   -- just respond to whoever spoke to you
        outM.mType   := M_HashCommit;
        outM.zid     := i;

        multisetadd (outM,net);

        res[i].state := R_HASH_COMMITTED;
        res[i].initiator := inM.zid;
      end;

    end;
  end;
end;

ruleset i: ResponderId do
  choose j: net do
    rule "responder reacts to M_DH received"

      res[i].state = R_HASH_COMMITTED &
      net[j].dest = i &
      !ismember(net[j].source,ResponderId)    -- talk to everyone but responders
    ==>

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

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

      if inM.mType = M_DH then      -- correct message type

        -- store the public value
        res[i].initiatorDH := inM.publicDH;

        undefine outM;
        
        -- if we recognize the hash, we are ready to converse, otherwise we 
        -- commit and wait for SAS
        if res[i].iniSharedSecret[res[i].initiator] = inM.hash then
          res[i].state := R_READYTOTALK;
        else
          res[i].state := R_COMMIT;
        end;
          
        outM.source   := i;
        outM.dest     := res[i].initiator;
        outM.mType    := M_DH;
        outM.publicDH := i;
        outM.hash      := i;

        multisetadd (outM,net);

      end;

    end;
  end;
end;


ruleset i: ResponderId do
  choose j: net do
    rule "responder reacts to M_SAS received"

      res[i].state = R_COMMIT &
      net[j].dest = i &
      !ismember(net[j].source,ResponderId)    -- talk to everyone but responders
    ==>

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

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

      if  inM.mType = M_SAS
        & inM.publicDH = i
        & inM.privateDH = res[i].initiatorDH 
        & (ResponderUnawareOfInitiatorsVoiceInAdvance | inM.zid = res[i].initiator) then

        undefine outM;
        outM.source    := i;
        outM.dest      := res[i].initiator;
        outM.mType     := M_SAS;
        outM.publicDH  := res[i].initiatorDH;
        outM.privateDH := i;
        outM.zid       := i;
        outM.hash      := i;                 -- we put our id in as the shared secret

        multisetadd (outM,net);

        res[i].state := R_READYTOTALK;
        res[i].initiatorSASVoice := inM.zid;
        res[i].iniSharedSecret[res[i].initiator] := inM.hash;
      end;
    end;
  end;
end;


ruleset i: ResponderId do
  choose j: net do
    rule "responder reacts to M_INIT_CONVERSATION received"

      res[i].state = R_READYTOTALK &
      net[j].dest = i &
      !ismember(net[j].source,ResponderId)    -- talk to everyone but responders
    ==>

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

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

      if  inM.mType = M_INIT_CONVERSATION
        & inM.publicDH = i
        & inM.privateDH = res[i].initiatorDH
          & (inM.zid = res[i].initiatorSASVoice | 
                 (isUndefined(res[i].initiatorSASVoice) & (ResponderForgetsVoiceBetweenSessions | inM.zid = res[i].initiatorConvVoice[res[i].initiator]))) 
          & (ResponderUnawareOfInitiatorsVoiceInAdvance | (inM.zid = res[i].initiator & inM.hash = res[i].initiator)) then

        undefine outM;
        outM.source    := i;
        outM.dest      := res[i].initiator;
        outM.mType     := M_RESP_CONVERSATION;
        outM.publicDH  := res[i].initiatorDH;
        outM.privateDH := i;
        outM.zid       := i;  -- voice
        outM.hash       := i; -- text of conversation
        outM.responseTo := inM.hash; -- text of conversation

        multisetadd (outM,net);

        res[i].initiatorConvVoice[res[i].initiator] := inM.zid;
        res[i].initiatorConvTextSender[res[i].initiator] := inM.hash;

        -- if we haven't connected before, then set it and go back to beginning
        if !res[i].connectedBefore then

          res[i].connectedBefore := true;
          res[i].state := R_SLEEP;
          undefine res[i].initiatorSASVoice;

        else
          res[i].state := R_DONE;
        end;
      end;
    end;
  end;
end;


-- ------------------------------------------------------------------------------
-- behavior of intruders
-- ------------------------------------------------------------------------------

ruleset i: IntruderId do
  choose j: net do
      rule "intruder intercepts"

      !ismember (net[j].source, IntruderId)    -- not for intruders' messages

      ==>

      begin
        alias msg: net[j] do   -- message to intercept

          switch msg.mType
          case M_RESP_CONVERSATION:
            if msg.publicDH = i then
              int[i].conversationtext[net[j].hash][net[j].responseTo] := net[j].zid;
            end;
          case M_INIT_CONVERSATION:
            if msg.publicDH = i then
              int[i].conversationtext[net[j].hash][net[j].responseTo] := net[j].zid;
            end;
          end;

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

ruleset i: IntruderId do
 ruleset k: AgentId do -- destination
  choose j: net do
      rule "intruder intercepts and forwards M_{INIT,RESP}_CONVERSATION"

      !ismember (net[j].source, IntruderId)    -- not for intruders' messages
      & !ismember(k, IntruderId)               -- not to intruders
      & (net[j].mType = M_INIT_CONVERSATION | net[j].mType = M_RESP_CONVERSATION)
      & net[j].publicDH = i
      
      ==>
      var
        outM: Message;

      begin
        alias inM: net[j] do   -- message to intercept

          int[i].conversationtext[net[j].hash][net[j].responseTo] := net[j].zid;

          undefine outM;
          outM.source := i;
          outM.dest   := k;
          outM.mType  := inM.mType;

          outM.publicDH  := k;
          outM.privateDH := i;
          outM.zid       := inM.zid;   -- voice
          outM.hash      := inM.hash; -- text of conversation
          outM.responseTo := inM.responseTo;

          multisetremove (j,net);
          multisetadd (outM,net);


        end;
      end;

    end;
  end;
end;


ruleset i: IntruderId do       -- arbitrary choice of
 ruleset j: AgentId do         --  destination
  ruleset l: MessageType do    --  message type
   ruleset z: AgentId do       --  zid
    ruleset p: AgentId do      --  publicDH
      rule "intruder generates M_Hello or M_HashCommit message"

        !ismember(j, IntruderId) &         -- not to intruders
        (l = M_Hello | l = M_HashCommit) & -- only these cases are handled by this ruleset
        multisetcount (t:net, true) < NetworkSize

      ==>

      var
        outM: Message;

      begin
        undefine outM;
        outM.source := i;
        outM.dest   := j;
        outM.mType  := l;
        outM.zid  := z;

        multisetadd (outM,net);
      end;

    end;
   end;
  end;
 end;
end; 

ruleset i: IntruderId do       -- arbitrary choice of
 ruleset j: AgentId do         -- destination
   ruleset p: AgentId do       -- publicDH
    rule "intruder generates M_DH message"
      !ismember(j, IntruderId) &   -- not to intruders
      multisetcount (t:net, true) < NetworkSize

     ==>

      var
      outM: Message;

      begin
        undefine outM;
        outM.source := i;
        outM.dest   := j;
        outM.mType  := M_DH;
        outM.publicDH := p;
        outM.hash := i;

        multisetadd (outM,net);
      end;

  end;
 end;
end;

ruleset i: IntruderId do       -- arbitrary choice of
 ruleset j: AgentId do         -- destination
  ruleset p: AgentId do        -- publicDH
   ruleset v: AgentId do       -- voice
    rule "intruder generates M_SAS message for his own conversations"

      !ismember(j, IntruderId) &   -- not to intruders
      multisetcount (t:net, true) < NetworkSize &
      (ismember(v, IntruderId) | (ismember(v, InitiatorId) & IntruderCanForgeInitiatorVoice) | (ismember(v, ResponderId) & IntruderCanForgeResponderVoice))

     ==>

      var
      outM: Message;

      begin
        undefine outM;
        outM.source := i;
        outM.dest   := j;
        outM.mType  := M_SAS;
        outM.publicDH := p;

        outM.zid := v;
        outM.privateDH := i;
        outM.hash := i;

        multisetadd (outM,net);
      end;

   end;
  end;
 end;
end; 

ruleset i: IntruderId do       -- arbitrary choice of
 ruleset j: AgentId do         -- destination
  rule "intruder generates M_INIT_CONVERSATION message with own voice and own text"

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

     ==>

      var
      outM: Message;

      begin
        undefine outM;
        outM.source := i;
        outM.dest   := j;
        outM.mType  := M_INIT_CONVERSATION;
        outM.privateDH := i;
        outM.publicDH := j;
        outM.zid := i;
        outM.hash := i;
        outM.responseTo := j;

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

ruleset i: IntruderId do
  choose j: net do
    rule "intruder generates message of type M_RESP_CONVERSATION in response to M_INIT_CONVERSATION"

      !ismember (net[j].source, IntruderId)    -- not for intruders' messages
      & net[j].mType = M_INIT_CONVERSATION
      & net[j].publicDH = i
     
      ==>
      var
        outM: Message;

      begin
        alias inM: net[j] do   -- message to intercept

          undefine outM;
          outM.source := i;
          outM.dest   := inM.source;
          outM.mType  := M_RESP_CONVERSATION;

          outM.publicDH  := inM.source;
          outM.privateDH := i;
          outM.zid       := i;   -- voice
          outM.hash      := i; -- text of conversation
          outM.responseTo := inM.hash;

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

ruleset i: IntruderId do       -- arbitrary choice of
 ruleset j: AgentId do         -- destination
  ruleset p: AgentId do        -- text of conversation
    rule "intruder i generates message of type M_INIT_CONVERSATION with the information it knows, using the INTRUDER's voice"

      IntruderHasCourtReporters &
      !ismember(j, IntruderId) &   -- not to intruders
      multisetcount (t:net, true) < NetworkSize &
      !isundefined(int[i].conversationtext[p][j])

     ==>

      var
      outM: Message;

      begin
        undefine outM;
        outM.source := i;
        outM.dest   := j;
        outM.mType  := M_INIT_CONVERSATION;
        outM.privateDH := i;
        outM.publicDH := j;
        outM.zid := i;
        outM.hash := p;
        outM.responseTo := j;

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

ruleset i: IntruderId do       -- arbitrary choice of
 ruleset j: AgentId do         -- destination
  ruleset p: AgentId do        -- text of conversation
    rule "intruder i generates message of type M_RESP_CONVERSATION with the information it knows, using the INTRUDER's voice"

      IntruderHasCourtReporters &
      !ismember(j, IntruderId) &   -- not to intruders
      multisetcount (t:net, true) < NetworkSize &
      !isundefined(int[i].conversationtext[p][j])

     ==>

      var
      outM: Message;

      begin
        undefine outM;
        outM.source := i;
        outM.dest   := j;
        outM.mType  := M_RESP_CONVERSATION;
        outM.privateDH := i;
        outM.publicDH := j;
        outM.zid := i;
        outM.hash := p;
        outM.responseTo := j;

        multisetadd (outM,net);
      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].responderDH := i;
    ini[i].connectedBefore := false;

    for j: AgentId do
      ini[i].resSharedSecret[j] := i;
      ini[i].responderConvVoice[j] := i;
    end;
  end;

  -- initialize responders
  undefine res;
  for i: ResponderId do
    res[i].state     := R_SLEEP;
    res[i].initiator := i;
    res[i].initiatorDH := i;
    res[i].connectedBefore := false;

    for j: AgentId do
      res[i].iniSharedSecret[j] := i;
      res[i].initiatorConvVoice[j] := i;
    end;
  end;

  -- initialize intruders
  undefine int;
  for i: IntruderId do
    for j: AgentId do
      int[i].conversationtext[i][j] := i;
    end;
  end;

  -- initialize network 
  undefine net;
end;



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

invariant "no man in the middle attack"
  forall i: InitiatorId do
    forall j: ResponderId do
      forall k: IntruderId do

        -- if two people have initiated conversation
        (ini[i].state = I_DONE | (ini[i].state = I_SLEEP & ini[i].connectedBefore = true)) &
        (res[j].state = R_DONE | (res[j].state = R_SLEEP & res[j].connectedBefore = true)) &
        ini[i].responder = j &
        res[j].initiator = i &
        res[j].initiatorConvTextSender[i] = i &
        ini[i].responderConvTextSender[j] = j
        ->
        isundefined(int[k].conversationtext[i][j]) & isundefined(int[k].conversationtext[j][i])
      end
    end
  end;
