--------------------------------------------------------------------------------
--
--  Murphi Model of the octopus protocol
--
--------------------------------------------------------------------------------
--
--------------------------------------------------------------------------------
--
--  Here, we model the case where we assume that the diffie-hellman
--  key exchange works and analyze the interactions between 1 core
--  member and its connected peer(s).
--  Authentication information is supposed to be present before the
--  start of this protocol, but it does not provide a method to use
--  this information. We would like to see what way this information
--  can be intergrated into the messages to ensure security.
--
--   A: core-member, B: connecting peer
--
--------------------------------------------------------------------------------

--  We assume
--  * standard (Dolev-Yao) attacker model for this analysis
--  * there has been a round of authentication before the start of this key 
--  exchange, and also a round to decide who will be a part of the core.
--  * each peer knows exactly which core member it should talk to.

--  * Later on we would like to analyze the methods of forming cores.

--  Attacks and revisions:
--
--  1. Since there is no identity information, the first attack is simple,
--  in which the attacker can pose as a peer and participate in the protocol
--  on behalf of another protocol. So the first step is to put in the identity
--  information in the messages.
--
--  2. Only putting in identity information obviously did not work. We need to
--  be able to prove that the person who is sending the information is the 
--  person he claims to be. To do this let us add some authentication information
--  that we have to assume. Since the protocol assumes everyone knows who the
--  peers are, we can assume that they have some kind of public key, known to
--  all the other peers. So lets add secure messages from the peer side.
--
--  3. This is still a problem, because the intruder can still masquerade as a core
--  member as there is no way for the core to prove to the peer that the message
--  really a message from the core. To handle this let us assume that the core
--  also sends along with the reply the actual DH element that the peer had sent 
--  it. Also we must assume that the peer DH is sent encrypted over the secure
--  channel built earlier.
-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
const

  NumPeers:	   2;   -- number of connecting peers
  NumCore:	   1;   -- number of members in the core

-- standard parameters for a Dolev Yao intruder

  NumIntruders:    1;   -- number of intruders
  NetworkSize:     1;   -- max. number of outstanding messages in network
  MaxKnowledge:   10;   -- max. number of messages intruder can remember


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

type
  PeerId:  	scalarset (NumPeers);
  CoreId:  	scalarset (NumCore);
  IntruderId:   scalarset (NumIntruders);
  AgentId:      union {PeerId, CoreId, IntruderId};
  ValidAgentId: union {PeerId, CoreId};
  keyType:	array[ValidAgentId] of AgentId;
  keyType_V:	array[ValidAgentId] of boolean;

  MessageType : enum {           -- different types of messages
    M_PeerKeyPart,		 -- the part of the DH key from the peer
    M_CoreKeyPart		 -- the part of the DH key after core-exchange
  };

  Message : record
    source:   AgentId;           -- source of message
    dest:     AgentId;           -- intended destination of message
    mType:    MessageType;       -- type of message
    key_1:    ValidAgentId;	 -- key used to encrypt the message
    fromId:   ValidAgentId;	 -- sender information
    fromId_E: ValidAgentId;	 -- sender information encrypted
    useKey:   ValidAgentId;	 -- sender key to use
    toId:     AgentId;		 -- recepient
    DH_Key_V: keyType_V;         --array[ValidAgentId] of boolean;
    DH_Key:   keyType;           --array[ValidAgentId] of AgentId;
    DH_Key_P: AgentId;           -- key generated ny peer;
    replayedAs : array[ValidAgentId] of boolean;
  end;

  -- the core member will return the DH_1 part in the return message to
  -- identify what it thinks the whole key is

  PeerStates : enum {
    P_READY,                     -- intially (ready to send DH part1)
    P_WAIT,                      -- waiting for key from core
    P_GOTKEY                     -- got some message containing the key
  };

  Peer : record
    state: PeerStates;
    keyMaterial_V: keyType_V;    --array[ValidAgentId] of boolean;
    keyMaterial: keyType;        --array[ValidAgentId] of AgentId;
  end;

  CoreMainStates: enum {
    C_RECEIVING,
    C_SENDING,
    C_MAINDONE
  };
  
  CoreStates : enum {
    C_WAIT,			 -- waiting for key material from peer
    C_GOTKEY,			 -- sending the key material back to peer
    C_DONE			 -- done sending
  };

  Core : record
    mainState: CoreMainStates;
    state: array[ValidAgentId] of CoreStates;
    keyMaterial_V: keyType_V;    --array[ValidAgentId] of boolean;
    keyMaterial: keyType;        --array[ValidAgentId] of AgentId;
  end;
 
  Intruder : record
    messages: multiset[MaxKnowledge] of Message;   -- known messages
  end;

  -- Note that it is fairly obvious in this scenario that the intruder
  -- would not be able to guess the secret from the network messages.
  -- Hence we will not check that case in the intruder model, nor will we 
  -- put in actions that are specifically meant to passively decipher the
  -- shared secret.

-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
var                                         -- state variables for
  net: multiset[NetworkSize] of Message;    --  network
  peer: array[PeerId] of Peer;              --  peers
  core: array[CoreId] of Core;              --  core members
  int: array[IntruderId] of Intruder;       --  intruders



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

--------------------------------------------------------------------------------
-- behavior of peers 
--------------------------------------------------------------------------------

-- peer i starts protocol with core member j

ruleset i: PeerId do
  ruleset j: CoreId do
    rule 20 "peer sends DH key material"

      peer[i].state = P_READY &
      multisetcount (l:net, true) < NetworkSize

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

    begin
      undefine outM;
      peer[i].keyMaterial_V[i] := true;
      peer[i].keyMaterial[i] := i;
      outM.source  := i;
      outM.dest    := j;
      outM.mType   := M_PeerKeyPart;
      outM.key_1 := j;    -- use the core's public key.
      outM.DH_Key_P := peer[i].keyMaterial[i];
      outM.fromId := i;
      outM.fromId_E := i;
      outM.toId := j;
      multisetadd (outM,net);

      peer[i].state     := P_WAIT;
    end;
  end;
end;

-- peer receives key material from core member

ruleset i: PeerId do
  choose j: net do
    rule 20 "peer receives key material"

      peer[i].state = P_WAIT &
      net[j].dest = i &
      ismember(net[j].source, IntruderId) &	 -- valid optimization as the attacker is a powerful Dolev Yao attacker
      ismember(net[j].fromId, CoreId) &          -- must be a message from a known core
      net[j].mType = M_CoreKeyPart               -- must be a message from a known core
    ==>

    var
      inM:  Message;   -- incoming message

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

      if inM.mType = M_CoreKeyPart then   -- correct message type
        for k: ValidAgentId do
          if inM.DH_Key_V[k] = true then
            peer[i].keyMaterial_V[k] := true;
            peer[i].keyMaterial[k] := inM.DH_Key[k];
	  endif;
	endfor;
        peer[i].state := P_GOTKEY;
      end;
    end;
  end;
end;


--------------------------------------------------------------------------------
-- behavior of core

-- core member i receives key material

ruleset i: CoreId do
  choose j: net do
    rule 120 "core receives key material"

      core[i].mainState = C_RECEIVING &
      ismember(net[j].fromId, PeerId) &       -- ensure this message is from a valid peer
      core[i].state[net[j].fromId] = C_WAIT & -- hasnt seen this message before
      net[j].dest = i &                       -- is destined for the core
      ismember(net[j].source,IntruderId) &    -- is replayed
      net[j].key_1 = i &			      -- is encrypted using core's key
      net[j].mType = M_PeerKeyPart &
      true
    ==>

    var
      inM:  Message;   -- incoming message

    begin
      inM := net[j];
      if inM.toId = i then
        if inM.fromId = inM.fromId_E then
          multisetremove (j,net);

          core[i].keyMaterial_V[inM.fromId] := true;
          core[i].keyMaterial[inM.fromId] := inM.DH_Key_P;
	  core[i].state[inM.fromId] := C_GOTKEY;
	endif
      endif;
    end;
  endchoose;
endruleset;

-----------------------
-- core got messages from all the nodes and can now exchange keys
-----------------------

ruleset i: CoreId do
  rule 90 "core switches state to send all keys"
  forall k:PeerId do
    core[i].state[k] = C_GOTKEY
  endforall &
  true

  ==>
  begin
    core[i].mainState := C_SENDING
  end
endruleset;

-----------------------
  -- send message to all peers about the shared key
-----------------------

ruleset i: CoreId do
  ruleset j: PeerId do
    rule 90 "Core sending out keys"
    core[i].mainState = C_SENDING &
    core[i].state[j] = C_GOTKEY &
    multisetcount (l:net, true) < NetworkSize

    ==>
    
    var
      outM: Message;

    begin
      outM.source  := i;
      outM.dest    := j;
      outM.mType   := M_CoreKeyPart;
      outM.key_1 := j;  -- no key
      for k:ValidAgentId do
	outM.DH_Key_V[k] := false;
	if k != j then
          if core[i].keyMaterial_V[k] = true then
            outM.DH_Key_V[k]  := true;
            outM.DH_Key[k]  := core[i].keyMaterial[k];
	  endif;
	endif;
      endfor;
      outM.fromId := i;
      outM.toId := j;
      multisetadd (outM,net);
      core[i].state[j]     := C_DONE;
    end;
  endruleset;
endruleset;

-- if all messages sent, set the main state to C_MAINDONE

ruleset i:CoreId do
  rule 90 "Core done sending all messages"
  
  core[i].mainState = C_SENDING &
  
  forall k:PeerId do
    core[i].state[k] = C_DONE
  endforall

  ==>
  begin
    core[i].mainState := C_MAINDONE
  end;
endruleset;

--------------------------------------------------------------------------------
-- behavior of intruder

-- intruder i intercepts messages
-- let us make the intruder remember the whole message that it
-- intercepted and then later send all the messages that the
-- intruder can generate from this message.

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

    !ismember (net[j].source, IntruderId) &   -- not an intruder's message
    --ismember(net[j].toId, PeerId)
    true
      ==>
      var
        temp: Message;
      begin
        temp := net[j];
	temp.source := i;
	for k:ValidAgentId do
	  temp.replayedAs[k] := false;
	endfor;
	multisetadd(temp, int[i].messages);
        multisetremove (j,net);
      end;
  endchoose;
endruleset;
--end;


-- intruder replays messages that it knows

ruleset i: IntruderId do
  choose j: int[i].messages do
    ruleset k: ValidAgentId do
    rule 90 "intruder replays learnt message"
    
      multisetcount (l:net, true) < NetworkSize &
      int[i].messages[j].replayedAs[k] = false &
      true
      ==>
      var
        temp: Message;
	outM: Message;

      begin
  	undefine outM;
	outM := int[i].messages[j];
	if outM.mType = M_PeerKeyPart then
          outM.fromId := k;
	endif;
	if outM.mType = M_CoreKeyPart then
	   -- nothing is visible so only replay
	endif;
	multisetadd(outM, net);
	int[i].messages[j].replayedAs[k] := true;
      end;
    endruleset; 
  endchoose;
endruleset;

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

startstate
  -- initialize peers
  undefine peer;
  for i: PeerId do
    peer[i].state     := P_READY;
    for j: ValidAgentId do
      peer[i].keyMaterial_V[j] := false;
    endfor;
    peer[i].keyMaterial_V[i] := true;
    peer[i].keyMaterial[i] := i;
  end;

  -- initialize core members
  undefine core;
  for i: CoreId do
    core[i].mainState := C_RECEIVING;
    for j: PeerId do
      core[i].state[j]     := C_WAIT;
    endfor;
    for j: ValidAgentId do
      core[i].keyMaterial_V[j] := false;
    endfor;
    core[i].keyMaterial_V[i] := true;
    core[i].keyMaterial[i] := 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 "key agreement"
  forall i: CoreId do
    core[i].mainState = C_MAINDONE 
    ->
    forall j: PeerId do
      forall k:PeerId do
        (peer[j].state = P_GOTKEY & peer[k].state = P_GOTKEY)
        ->
        forall l:ValidAgentId do
          peer[j].keyMaterial_V[l] = peer[j].keyMaterial_V[l] &
	  (peer[j].keyMaterial_V[l] = true ->
            peer[j].keyMaterial[l] = peer[k].keyMaterial[l] )
	endforall
      endforall
    endforall
  endforall;


