draft TLA+ model of the server as a message queue with clients

[cfm]

Per #26 (comment), we are on the right track for modeling this protocol's security properties. However, I have a feeling that we will also want to model this server's correctness properties, such as:

1. Does the wheat+chaff message queue work as we expect?
2. What are the CAP bounds on the pool of journalist keys?
3. How should we choose an expiration interval for different rates of submission and retrieval?
4. How does (3) influence whether we use the message queue for in-band synchronization (link TK)

My intuitions are that:

1. This isn't a job for Tamarin, which cares about protocols, not systems.
2. It could be done in Coq or Isabelle, which as generic proof assistants can do both protocols and systems. But since we're not already using either one of them...
3. We might as well just start with TLA+, much like docs(Reply): model unified Reply object securedrop-client#1632.