Initial comments on spec
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.
1. "more formal writeup": Sure, we have published the protocol for now for security review. We are implementing it currently for libpurple. We have plan to add all implementation detail after we finished an implementation (this include the detail of receive handler).
2. "explicitly list all of the states": Yes, the implementation of the session class has a finite state machine. We'll publish that automaton as well in the final version after we are happy with the implementation.
3. "elliptic curve you're using for TDH": We are going to use Ed25519 for both signature and encryption (not Curve25519). We like Edward curve, they are faster and have one addition formula so less prune to timing side channel.
4. "You don't specify when and if group membership checks are required."
I don't get this exactly could you explain more the problem.
"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."
I think we just treat "y" as a point on Ed25519, when the use sends its ephemeral key. If it doesn't compute then we reject and halt the join.
Initial superficial protocol comments:
A. "Why sign-then-encrypt"
We added the nonce partially to protocol it from the pitfalls, plus we have the sender name in the message. We studied the argument for both sides. And we think this offers some advantage. For one, outsider, can not obtain any proof of association and origin authenticity which goes along the way of deniability, specially for an outsider.
B. "Do you need to verify that you don't require contributory" The protocol is not provable contributary. As the result there is a attack which makes TDH undeniable against off-line cooperative judge. It needs one extra round and some of the reviewers had strongly believe that contributiveness is not useful to sacrifice one round for it. We might change this once we check the performance effect of one extra round in practical conditions.
C. "What's the rationale for AES-256 rather than AES-128?" I believe it was partly because it was already being used by Cryptocat. On the other hand, it is true if the only option is exhaustive search, then strengthening AES only doesn't make sense. However, potentially one can carry out attack against the symmetric key, which is not available the signature and TDH, like the known plain-text attacks. The overhead of using AES-256 perceived minimal and as such, gaining some safety margin doesn't seem too bad of an idea.
D. "Broadcasting the user identities U in cleartext" They should use ssl and tor to connect to the server (Their ip is also probably reveal their identity). It is part of deniability that anybody should be able to impersonate you. The only person which can detect if your are the real you is the person who run a TDH with you.
E. "version number" Actually we don't have a version number. We should add it during join process. Good point, I'll work on it.
I. "What happens if somebody wants to join a chat, and the participants can't agree on whether they are a legit participant?"
It halts. Only when everybody in the room agree, you can join. This is the trust model we designed based on it. However, we are planning to offer some side protocol to deal with denial of service, dealing with such situations. But normally if you don't agree, you should start room with those who agree.
II. "Where does access control fit in here? Could you explain more?
III. "What UI can work for verifying others' keys?" We probably adopt the socialist millionaire as a side protocol but it is really another problem and we didn't want to make a the main protocol more complicated than necessary.
IV. "it makes sense to specify the information that must flow from the protocol implementation to the UI, and from the UI to the protocol" Sure, we will add this after we finish the implementation.