I think both solutions are fine, but 2 might be the best usability?

I think those docs are typically called white papers.

Its hard to get past those biases, but its a valuable skill to critically review your own work. And it feels better on your wallet to find bugs before paying for a third party review :)

I’m not an expert in this field, so I have never heard of ProVerif, it definitely looks interesting though, and wouldn’t hurt to try?

I am not really sure what the real solution is beyond creating the out of band method of validating the public key. Historically, this would be done by publishing your public gpg key to a 3rd party key server. Most modern apps use a qr code (I don’t know how this works, may require research) you can scan when you physically meet, or scan over a different medium (email, SMS etc).

The problem with relying on the random number is that E can decrypt the message from A, and then reencrypt it and send it to B. B won’t know it has been inspected enroute. So B could call A and tell them the random number, but it wouldnt actually be secure. Also, if later in the chat A were to tell B, “My public key is XYZ”, E could detect that and alter it to " My public key is ABC" before sending it on to B.

If A can generate a hash of the B’s public key, and B also makes a hash, they can call each other and compare, and if the hashes don’t match, E is listening. I think that is all you need, a way to present the public key to the users so they can validate it manually.

Aside, but I don’t think it is a good idea for you to spend money on an audit yet. Spend some time trying to break your own system, by creating the malicious E server. You can then tweak and adjust your scheme until E is either impossible or trivially detectable. Unless this become a large scale venture, an audit isn’t worth it, and I get the impression this is more of a learning exercise for yourself? Also, once you are finalised, write up a paper on your scheme. Something like: https://signal.org/docs/specifications/x3dh/. Crypto experts will be able to easily validate that your scheme based on the paper. Crypto people can easily validate your scheme based on the paper…

Okay, that is not a way to validate the other users public key, all that does is validate the other ends public key. The other end and the other user are not the same thing.

If this was a malicious server (or a MitM server), the way it would work is:

A wants to speak to B. The server lies, and instead of giving B’s public key, gives E. The server has the public and private keys for E.

A generates the hash, and encrypts it with what it thinks is B’s public key. The server completes the rest of your “handshake”. A has no idea that A is handshaking with E instead of B. B will also handshake with E. The server can then decrypt everything between A and B, and A and B have no idea they are using the wrong keys.

Unless A and B meet and compare public keys, they can’t know that something is up.

I wasn’t planning on reusing that ID, it was an incognito tab.

Without a way for users to validate each others public keys, at most I think you can claim is that your chat has encryption. To be properly e2ee, users need a way to validate each others public keys via a side channel, so they can be sure there is no MitM.

Also, I notice that you claim your app is decentralised, but I don’t think that is true? There is no federation or similar, so if two users want to talk, they must use the same server?

Less code/complexity is less chance for bugs, which is why I suggest it might not be wise to add more layers.

The extra layer of encryption may give you something if the webrtc connection is assumed to be mitm’d, but you still need a way the ensure that your internal crypt is appropriately mitm resistant. On signal, this is achieved with the safety numbers that you must verify in a separate channel (IRL/email/other).

Do you have a way to do that? Is the last part of the invite URL the public key? - https://chat.positive-intentions.com/#/login/60c01cecb60530e79c0f9d90cee6642d

If not, the malicious server can simply do the handshake to both clients separately and decrypt/log/reencrypt the messages. If I am not explaining it clearly, let me know and I’ll try again.

I am not an expert either (anyone claiming to be so is knee-deep in dunning-kruger), but here are some thoughts:

Why are you adding an additional layer of complexity to webrtc? It has e2ee already?

How does a user validate that they are actually e2ee? Could a malicious server pretend to support your protocol and decrypt everything?