Initial protocol model work

.gitignore

@@ -0,0 +1,4 @@
+*.cpp
+*.cache
+*.disk
+otrv4

Makefile

@@ -1,7 +1,7 @@
 INCLUDE = ${MDIR}/include/
 
-MDIR = /usr/local/src/cmurphi5.4.9.1
-MURPHI = ${MDIR}/src/cmake-build-debug/mu
+MDIR = /usr/local/src/cmurphi
+MURPHI = mu
 INCLUDEPATH = ${MDIR}/include
 
 CXX = g++
@@ -33,14 +33,14 @@ otrv4.disk: otrv4.disk.cpp
 	${CXX} ${CFLAGS} ${OFLAGS} -o otrv4.disk otrv4.disk.cpp -I${INCLUDEPATH} -lm
 
 otrv4.cpp: otrv4.m
-	${SRCPATH}mu otrv4.m
+	${MURPHI} otrv4.m
 
 otrv4.cache.cpp: otrv4.m
-	${SRCPATH}mu --cache -b -c otrv4.m
+	${MURPHI} --cache -b -c otrv4.m
 	mv otrv4.cpp otrv4.cache.cpp
 
 otrv4.disk.cpp: otrv4.m
-	${SRCPATH}mu --disk otrv4.m
+	${MURPHI} --disk otrv4.m
 	mv otrv4.cpp otrv4.disk.cpp
 
 clean:

notes.txt

@@ -0,0 +1 @@
+- Whitespace tags should not be sent in ENCRYPTED_MESSAGES

otrv4.m

@@ -15,19 +15,21 @@
 --
 --------------------------------------------------------------------------------
 
+
 --------------------------------------------------------------------------------
 -- 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
+  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
-  ParticipantId: scalarset (NumParticipants);
+  InstanceTag: scalarset (NumClients);
   
   MessageType : enum {   -- Types of messages that can be sent
     M_Plaintext,           -- Ordinary plaintext without special values
@@ -54,9 +56,17 @@ type
   };
   
   Message : record
-    src, dst: ParticipantId;
     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
@@ -78,22 +88,102 @@ type
     SMP_Expect4  -- Waiting for a T_SMP4 TLV
   };
 
-  Participant : record
+  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
-  agents: array[ParticipantId] of Participant; -- Honest clients
+  net:    multiset[NetworkSize] of Message; -- In-flight messages
+  clients: array[InstanceTag] of Client;    -- Honest clients
   
   -- Adversarial knowledge:
   -- TODO
 
+
 --------------------------------------------------------------------------------
--- Rules
+-- 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;