Check the design with ProVerif (or was it CryptoVerif?)

[LoupVaillant]

Check the design with ProVerif (or was it CryptoVerif?)

[LoupVaillant]

OK, ProVerif looks like a nightmare that cannot handle XOR, has difficulty with Diffie Hellman, whose results are difficult to interpret, and assumptions tricky to get right. I'm almost more likely to screw up a ProVerif proof than a manual analysis.

I think I'll analyse the stuff by hand. The protocols are very simple anyway, there should be very little room for error.

[LoupVaillant]

I am told analysis has been done by third parties (paper upcoming). Feedback so far didn't uncover any problem (except with the Chacha20 KDF thing, but that's now out).

This part is done.