otrv4mu/otrv4.m

--------------------------------------------------------------------------------
--
--  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
  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_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
    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_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
  };

  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;




--------------------------------------------------------------------------------
-- 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;


--------------------------------------------------------------------------------
-- 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;