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