Risks of Standalone ML-KEM in TLS 1.3

We attest that standalone ML-KEM in TLS 1.3 breaks the existing formal proofs of TLS in state-of-the-art symbolic security analysis tool, ProVerif. We also attest that from a formal analysis perspective, this is a much bigger change than RFC8773bis, which indeed went for FATT review (cf. [TLS-FATT]). We, therefore, kindly ask the chairs to initiate the FATT review of standalone ML-KEM in TLS.