--------------------------------------------------------------------------------
--
--  Murphi Model of the OTRv4 Draft Protocol State Machine
--
--------------------------------------------------------------------------------
--
--  Written by Nik Unger 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
  NumParticipants: 2;   -- number of participants in the system
  NetworkSize:     1;   -- max. number of outstanding messages in network
  MaxKnowledge:   10;   -- max. number of messages intruder can remember

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

type
  ParticipantId: scalarset (NumParticipants);
  
  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_DAKEData,            -- Mandatory encrypted message reply to an Auth-I
    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
    src, dst: ParticipantId;
    msgType:  MessageType;
    -- TODO
  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_WaitingDAKEData,     -- Waiting for M_DAKEData
    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
  };

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

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

-- The global state of the system
var
  net:    multiset[NetworkSize] of Message;    -- In-flight messages
  agents: array[ParticipantId] of Participant; -- Honest clients
  
  -- Adversarial knowledge:
  -- TODO

--------------------------------------------------------------------------------
-- Rules
--------------------------------------------------------------------------------