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.