Remove DAKE data message

otrv4.m

@@ -30,7 +30,7 @@ const
 
 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
@@ -40,10 +40,9 @@ type
     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
@@ -54,33 +53,32 @@ type
     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
@@ -93,9 +91,9 @@ type
     smpState: SMPState;         -- SMP state machine
     -- TODO
   endrecord;
-  
+
   msgCount: 0 .. MaxMessages;
-  
+
   Client : record
     conv:     array[InstanceTag] of Conversation;
     msgCount: msgCount
@@ -107,7 +105,7 @@ type
 var
   net:    multiset[NetworkSize] of Message; -- In-flight messages
   clients: array[InstanceTag] of Client;    -- Honest clients
-  
+
   -- Adversarial knowledge:
   -- TODO
 
@@ -171,12 +169,12 @@ endruleset;
 
 startstate
   undefine net;
-  
+
   undefine clients;
-  
+
   for i : InstanceTag do
     clients[i].msgCount := 0;
-    
+
     for j : InstanceTag do
       alias
         c : clients[i].conv[j]