move protocol to website

2 files changed, 96 insertions, 0 deletions

diff --git a/doc/index.mdwn b/doc/index.mdwn
index 883a825..6c62fe5 100644
--- a/doc/index.mdwn
+++ b/doc/index.mdwn
@@ -3,6 +3,7 @@
 * [[news]]
 * [[bugs]]
 * [[todo]]
+* [[protocol]]
 * [[servers]]
 """]]
 
diff --git a/doc/protocol.mdwn b/doc/protocol.mdwn
new file mode 100644
index 0000000..d290be7
--- /dev/null
+++ b/doc/protocol.mdwn
@@ -0,0 +1,95 @@
+The debug-me protocol is a series of messages, exchanged between
+the two participants, known as the user and the developer. 
+
+The messages are serialized as JSON in debug-me log files, and protocol
+buffers are used when sending the messages over the wire. We won't go into
+the full details here. See Types.hs for the data types that JSON
+serialization instances are derived from, and ProocolBuffers.hs for the
+protocol buffers format. There is also a simple framing protocol used for
+communicating over websockets; see WebSockets.hs.
+
+The Activity type is the main message type. The user sends Activity
+Seen messages, and the developer responds with Activity Entered.
+There are also Control messages, which can be sent by either
+party at any time, and do not affect IO to the console.
+
+The first message in a debug-me session is a Control sent by the
+user, which establishes a session key (see below for details). The second
+message is an Activity Seen.
+
+Activity Seen and Activity Entered messages have a prevActivity,
+which points to the Hash of a previous Activity. (And is Nothing for the
+first Activity Seen.) So a chain of messages is built up.
+
+(The exact details about how objects are hashed is not described here;
+see Hash.hs for the implementation. Note that the JSON strings are *not*
+directly hashed (to avoid tying hashing to JSON serialization details),
+instead the values in the data types are hashed.)
+
+The user and developer have different points of view. For example,
+the developer could send an Activity Entered at the same time the user
+is sending an Activity Seen. It's not clear in which order these two
+Activities occurred -- in fact they occurred in different orders in
+different places -- and so the user and developer will disagree
+about it.
+
+Since the goal of debug-me is to produce a proof of the sequence of events
+that occurred in a session, that is a problem. Perhaps the developer was
+entering "y" in response to "Display detailed reactor logs?" at the same time
+that a new "Vent core to atmosphere?" question was being displayed!
+The debug-me protocol is designed to prevent such conflicts of opinion.
+
+The user only processes a new Activity Entered when it meets one of these
+requirements:
+
+1. The Activity Entered has as its prevActivity the last Activity
+   (Entered or Seen) that the user processed.
+2. The Activity Entered has as its prevActivity an older Activity
+   that the user processed, and its echoData matches the concacenation
+   of every Activity Seen after the prevActivity, up to the most recent
+   Activity Seen.
+
+   (This allows the developer to enter a command quickly without waiting
+   for each letter to echo back to them.)
+
+When an Activity Entered does not meet these rules, the user sends
+it back in a Rejected message to let the developer know the input was not
+allowed.
+
+The developer also checks the prevActivity of Activity Seen messages it
+receives from the user, to make sure that it's receiving a valid chain of
+messages. The developer accepts a new Activity Seen when either:
+
+1. The Activity Seen has a prevActivity that points to the last
+   Activity Seen that the developer accepted.
+2. The Activity Seen has as its prevActivity an Activity Entered
+   that the developer generated, after the last Activity Seen
+   that the developer accepted.
+
+At the start of the debug-me session, Ed25519 session key pairs are
+generated by both the user and the developer. The first message
+in the protocol is the user sending their session pubic key
+in a Control message containing a SessionKey.
+
+Before the developer can enter anything, they must send a SessionKey message
+with their session key, and it must be accepted by the user. The developer
+must have a gpg private key, which is used to sign their session key. 
+(The user may have a gpg private key, which may sign their session key
+if available, but this is optional.) The user will reject session keys
+that are not signed by a gpg key or when the gpg key is not one they
+trust. The user sends a SessionKeyAccepted/SessionKeyRejected control
+message to indicate if they accepted the developer's key or not.
+
+Each message in the debug-me session is signed by the party that sends it,
+using their session key. The hash of a message includes its signature, so
+the activity chain proves who sent a message, and who sent the message
+before it, etc.
+
+Note that there could be multiple developers, in which case each will
+send their session key before being able to do anything except observe
+the debug-me session.
+
+The prevActivity hash is actually not included in the data sent across the
+wire. It's left out to save space, and gets added back in by the receiver.
+The receiver uses the signature of the message to tell when it's found
+the right prevActivity hash to add back in.