My only problem is why force TLS when we have better protocols nowadays. We did some research on using noise (in addition to TLS) but I’m not sure anyone really pushed for this to be considered officially (cf nQUIC)
Of course such proofs come with caveats - in particular the proofs assume your cryptographic primitives work as intended (e.g. that AES isn't broken) and that you've implemented the specification and not something else - but our experience has been that it's valuable to get those proofs, and where proof turns out to be difficult it's a valuable pointer to weaknesses in your design.
As far as I know nobody has done such a proof for the Noise design, and so we only have our intuition that it looks safe.
Also I may be wrong again, but it is for TLS, that even with all the simplifications and major changes on TLS 1.3, that we only have proofs of correctness for certain subsets of the spec, and specific modes of operation (theres a version of the protocol targeting IoT for which this work has been done, but I can't remember the name)
There are legitimate use cases for "running naked", but now we're doomed to jerry-rigging some BS ephemeral self-signed certificates in order to use any QUIC client that follows the official spec.
FWIW though, TLS 1.3 (the only currently supported TLS in QUIC, AFAIK) is a lot less hairy than TLS 1.2 and earlier; and most of the primitives are the same as you would use for noise (i.e. standard AEADs like ChaCha20-Poly1305).
Sure support is good but so is PGP’s
Also TLS was selected because of regulations. Which is damning to say the least.
I would like to read more about this. Link?