Initial commit

Makefile

@@ -0,0 +1,47 @@
+INCLUDE = ${MDIR}/include/
+
+MDIR = /usr/local/src/cmurphi5.4.9.1
+MURPHI = ${MDIR}/src/cmake-build-debug/mu
+INCLUDEPATH = ${MDIR}/include
+
+CXX = g++
+
+CFLAGS = 
+
+OFLAGS = -O2
+
+#Murphi options
+MURPHIOPTS = -b -c
+
+all: otrv4 otrv4.cache otrv4.disk
+splitfile: otrv4.cache.splitfile otrv4.disk.splitfile
+
+# rules for compiling
+otrv4: otrv4.cpp
+	${CXX} ${CFLAGS} ${OFLAGS} -o otrv4 otrv4.cpp -I${INCLUDEPATH} -lm
+
+otrv4.cache: otrv4.cache.cpp
+	${CXX} ${CFLAGS} ${OFLAGS} -o otrv4.cache otrv4.cache.cpp -I${INCLUDEPATH} -lm
+
+otrv4.cache.splitfile: otrv4.cache.cpp
+	${CXX} ${CFLAGS} ${OFLAGS} -o otrv4.cache.splitfile otrv4.cache.cpp -I${INCLUDEPATH} -lm -DSPLITFILE
+
+otrv4.disk.splitfile: otrv4.disk.cpp
+	${CXX} ${CFLAGS} ${OFLAGS} -o otrv4.disk.splitfile otrv4.disk.cpp -I${INCLUDEPATH} -lm -DSPLITFILE
+
+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
+
+otrv4.cache.cpp: otrv4.m
+	${SRCPATH}mu --cache -b -c otrv4.m
+	mv otrv4.cpp otrv4.cache.cpp
+
+otrv4.disk.cpp: otrv4.m
+	${SRCPATH}mu --disk otrv4.m
+	mv otrv4.cpp otrv4.disk.cpp
+
+clean:
+	rm -f *.cpp otrv4 otrv4.cache otrv4.disk otrv4.cache.splitfile otrv4.disk.splitfile

UNLICENSE

@@ -0,0 +1,24 @@
+This is free and unencumbered software released into the public domain.
+
+Anyone is free to copy, modify, publish, use, compile, sell, or
+distribute this software, either in source code form or as a compiled
+binary, for any purpose, commercial or non-commercial, and by any
+means.
+
+In jurisdictions that recognize copyright laws, the author or authors
+of this software dedicate any and all copyright interest in the
+software to the public domain. We make this dedication for the benefit
+of the public at large and to the detriment of our heirs and
+successors. We intend this dedication to be an overt act of
+relinquishment in perpetuity of all present and future rights to this
+software under copyright law.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR
+OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
+ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+OTHER DEALINGS IN THE SOFTWARE.
+
+For more information, please refer to <http://unlicense.org>

otrv4.m

@@ -0,0 +1,99 @@
+--------------------------------------------------------------------------------
+--
+--  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
+--------------------------------------------------------------------------------