--------------------------------------------------------------------------------
--
--  Murphi Model of the OTRv4 Draft Protocol State Machine and SMP State Machine
--
--------------------------------------------------------------------------------
--
--  Written by Nik Unger and Sofía Celi in 2018
--
--  This is free and unencumbered software released into the public domain.
--  See the UNLICENSE file for the full license / public domain declaration.
--
--  The structure of this Murphi description is heavily inspired by the
--  Needham-Schroeder description by Ulrich Stern, 1998 (bundled with CMurphi),
--  and the OTRv2 description by Andrew Morrison and Joe Bonneau, 2006.
--
--------------------------------------------------------------------------------


--------------------------------------------------------------------------------
-- Declarations
--------------------------------------------------------------------------------

const
  NumClients:      2;   -- number of clients in the system
  NetworkSize:     1;   -- maximum number of in-flight messages in network
  MaxMessages:    10;   -- maximum number of messages sent in a conversation
  MaxKnowledge:   10;   -- maximum number of messages intruder can remember

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

type
  InstanceTag: scalarset (NumClients);

  MessageType : enum {   -- Types of messages that can be sent
    M_Plaintext,           -- Ordinary plaintext without special values
    M_WSpTaggedPlaintext,  -- Plaintext with a whitespace tag
    M_QueryMessage,        -- OTR query message
    M_ErrorMessage,        -- OTR error message
    M_IdentityMessage,     -- Identity message (DAKEZ flow 1)
    M_AuthR,               -- Auth-R message (DAKEZ flow 2)
    M_AuthI,               -- Auth-I message (DAKEZ flow 3)
    M_NonInteractiveAuth,  -- Non-Interactive-Auth message (XZDH flow 2)
    M_DataMessage          -- Encrypted message with text and optionally TLV(s)
  };

  TLVType : enum { -- Types of encoded TLVs inside data messages
    T_Padding,             -- Data to ignore (to hide message lengths)
    T_Disconnected,        -- States that the conversation is over
    T_SMP1,                -- SMP flow 1
    T_SMP2,                -- SMP flow 2
    T_SMP3,                -- SMP flow 3
    T_SMP4,                -- SMP flow 4
    T_SMPAbort,            -- States that the SMP has failed
    T_ExtraSymmetric       -- Request for an extra symmetric key
  };

  Message : record
    msgType:  MessageType;

    src, dst: InstanceTag; -- The actual sender & receiver clients
    -- TODO
  endrecord;

  ClientProfile : record
    owner: InstanceTag;  -- Instance tag of creating client
    -- TODO

    expired: boolean;
  endrecord;

  -- Not modeled: fragmented messages
  -- Not modeled: OTRv3 transitions

  ProtocolState : enum { -- Main protocol states for OTRv4 clients
    S_Start,               -- Initial client state
    S_WaitingAuthR,        -- Waiting for M_AuthR
    S_WaitingAuthI,        -- Waiting for M_AuthI
    S_EncryptedMessages,   -- DAKE is finished, ready for encrypted messages
    S_Finished             -- Received a disconnected message
  };

  SMPState : enum { -- SMP state, which expects an S_EncryptedMessages state
    SMP_Expect1, -- Initial SMP state, waiting for a T_SMP1 TLV
    SMP_Expect2, -- Waiting for a T_SMP2 TLV
    SMP_Expect3, -- Waiting for a T_SMP3 TLV
    SMP_Expect4  -- Waiting for a T_SMP4 TLV
  };

  Conversation : record
    protoState: ProtocolState;  -- Overall protocol state machine
    smpState: SMPState;         -- SMP state machine
    -- TODO
  endrecord;

  msgCount: 0 .. MaxMessages;

  Client : record
    conv:     array[InstanceTag] of Conversation;
    msgCount: msgCount
  endrecord;

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

-- The global state of the system
var
  net:    multiset[NetworkSize] of Message; -- In-flight messages
  clients: array[InstanceTag] of Client;    -- Honest clients

  -- Adversarial knowledge:
  -- TODO


--------------------------------------------------------------------------------
-- Helper procedures and functions
--------------------------------------------------------------------------------

function transmittable(src, dst: InstanceTag) : boolean;
begin
  return   src != dst
         & multisetcount(l:net, true) < NetworkSize
         & clients[src].msgCount < MaxMessages;
endfunction;

procedure transmitMessage(src, dst: InstanceTag; var msg: Message);
begin
  msg.src := src;
  msg.dst := dst;
  multisetadd(msg, net);
  clients[src].msgCount := clients[src].msgCount + 1
endprocedure;

procedure receiveMessage(src, dst: InstanceTag; var msg: Message);
begin
  msg.src := src;
  msg.dst := dst;
  multisetadd(msg, net);
  clients[src].msgCount := clients[src].msgCount + 1
endprocedure;


--------------------------------------------------------------------------------
-- Client and user rules
--------------------------------------------------------------------------------

ruleset a : InstanceTag; b : InstanceTag do
  rule "User requests a new OTR conversation with a query message"
      transmittable(a, b)
      & clients[a].conv[b].protoState != S_EncryptedMessages
    ==>
    var msg: Message;
    begin
      undefine msg;
      msg.msgType := M_QueryMessage;
      transmitMessage(a, b, msg)
  endrule;
endruleset;

ruleset a : InstanceTag; b : InstanceTag do
  rule "User requests a new OTR conversation with a whitespace tag"
      transmittable(a, b)
      & clients[a].conv[b].protoState != S_EncryptedMessages
    ==>
    var msg: Message;
    begin
      undefine msg;
      msg.msgType := M_WSpTaggedPlaintext;
      transmitMessage(a, b, msg)
  endrule;
endruleset;

ruleset a : InstanceTag; b : InstanceTag do
  rule "User reacts to a Query message and sends Identity message"
      transmittable(a, b)
      & (clients[a].conv[b].protoState = S_Start
      | clients[a].conv[b].protoState = S_WaitingAuthR
      | clients[a].conv[b].protoState = S_WaitingAuthI
      | clients[a].conv[b].protoState = S_EncryptedMessages
      | clients[a].conv[b].protoState = S_Finished)
    ==>
    var msg: Message;
    begin
      undefine msg;
      msg.msgType := M_QueryMessage;
      receiveMessage(a, b, msg)
  endrule;
endruleset;

--------------------------------------------------------------------------------
-- Starting state
--------------------------------------------------------------------------------

startstate
  undefine net;

  undefine clients;

  for i : InstanceTag do
    clients[i].msgCount := 0;

    for j : InstanceTag do
      alias
        c : clients[i].conv[j]
      do
        c.protoState := S_Start;
        c.smpState := SMP_Expect1
      endalias;
    endfor;
  endfor;
endstartstate;