[shengtongzhang]

Shengtong chiming in here. We are working on a rigorous security proof here https://anysphere.co/anysphere-security-definition.pdf. Included in it is a definition of metadata, a definition of exactly what we are defending against, as well as a rigorous proof of defense against adversaries that can manipulate packets. It is still work in progress, so there may be a lot of typos, but I believe it is a correct proof.

Let us know if there is anything else you want to be proved, or if the adversary in the paper is not strong enough :).