Initial comments on spec
This is the thread's initial revision.
Here are a few initial comments; I'll try to write better ones soon:
You have some TeX in the formula for step 6 of Algorithm 1.
Bigger comments on presentation:
1. If you're hoping to get multiple correct implementations of this protocol, there should really be a more formal writeup of the data formats. Ideally, the data formats should be specified in some format that is both human- and machine-readable, and it should be used to generate the encoding-decoding code. If a parser is not generated from your grammar, that parser will probably be wrong.
2. Likewise, you should probably explicitly list all of the states that a participant in this protocol can be in, which messages and which user-operations are accepted/sent in each state, and which state transitions those cause. There is enough complexity here that without an explicit spec of this kind, some implementor will accept a corner-case that others won't.
3. I assume that the elliptic curve you're using for TDH is Curve25519, but I don't think you actually say so? (You do say that the signature format is Ed25519.)
4. You don't specify when and if group membership checks are required. If someone tries to instantiate this protocol using a curve that represents points in an (x,y) format, or a curve without a secure twist, they will need to figure when to do these checks. (It's okay IMO to require a "Safecurves" curve in compressed format, but you've got to say so if you do.)
Initial superficial protocol comments:
A. Why sign-then-encrypt rather than the more usual encrypt-then-sign? Sign-then-encrypt has some pretty well-known implementation pitfalls.
B. Do you need to verify that you don't require contributory behavior on the DH handshakes? Curve25519 requires a post-handshake check if you require contributory behavior.
C. What's the rationale for AES-256 rather than AES-128? Everything else you're using (SHA-512, Ed25519) seems to be at a 128-bit security level.
D. Broadcasting the user identities U in cleartext would be best avoided for many applications, as would having identities remain consistent in third-parties' view across different discussions and forums.
E. I notice a version number in the message format. That's great, but it's important to specify what implementations must do if they see a version number they don't recognize.
I. What happens if somebody wants to join a chat, and the participants can't agree on whether they are a legit participant?
II. Where does access control fit in here?
III. What UI can work for verifying others' keys? Making key verification is a major design feature for OTR.
IV. IMO, it makes sense to specify the information that must flow from the protocol implementation to the UI, and from the UI to the protocol implementation, to be explicit about what abilities the user needs to have and what information they need to be presented.