Thanks Ilari, I find the draft title extremely misleading. This has nothing to do with either ML-KEM or standalone KEMs. Since X25519 is already used as a KEM in TLS, any issues with existing formal proofs would instead point to shortcomings in the proof models themselves.
A perfectly fine implementation of X25519 in TLS 1.3 is: X25519.KeyGen() dk = a = 32 random bytes ek = X25519(a, 9) return (ek, dk) X25519.Encaps(ek) b = 32 random bytes c = X25519(b, 9) K = X25519(b, ek) return (K, c) X25519.Decaps(dk, c) K = X25519(dk, c) return K What the draft appears to be claiming is that existing formal proofs rely on assumptions about how TLS 1.3 is implemented. ML-KEM provides stronger security properties than X25519-based KEM constructions. Therefore, if a re-evaluation of formal proofs is warranted, it should focus on standalone X25519 and standalone P-256. Cheers, John Preuß Mattsson From: Ilari Liusvaara <[email protected]> Date: Tuesday, 19 May 2026 at 11:42 To: [email protected] <[email protected]> Subject: [TLS] Re: Fwd: New Version Notification for draft-usama-tls-risks-of-mlkem-00.txt On Fri, May 15, 2026 at 02:01:02PM +0200, Muhammad Usama Sardar wrote: > Hi all, > > On popular demand, I've moved around ML-KEM from > draft-usama-tls-fatt-extension [0] to a draft of its own. > > If you have read my FATT draft [0], there is only one new -- just > two-minutes read -- section (Sec. 2.1), but it is the most important one, > where I show precisely where my [1] (and Karthik et al.'s [2]) existing TLS > 1.3 proofs in ProVerif break and why FATT review is necessary. I believe > this is sufficient justification for FATT review. This looks like proof artifact. Furthermore, the hybrids would break those proofs just the same. One can not assume that "just add stuff" works properly, for example, naive combination of two IND-CCA KEMs might be insecure[1]. And what the proofs will show is already known: The way ML-KEM (and hybrids) is integrated into TLS 1.3 is secure, tracing back all the way to core cryptographic assumptions. Proving those is far beyond reach. This is based on what is known: - One-wayness under plaintext checking and validity oracle is sufficient for KEM to be secure in TLS. - If keys are not reused, or if attacker is passive, one-wayness under confirmation[2][3] is sufficient. - Composites are either of the above if any component is. - IND-CCA implies One-wayness under plaintext checking and validity oracle. - ML-KEM is proven to be IND-CCA if some lattice cryptographic assumptions hold. - Diffie-Hellman is one-way under plaintext checking and validity oracle if computational Diffie-Hellman is still hard given decisional Diffie-Hellman oracle. - Proving that the lattice cryptographic assumptions underlying ML-KEM hold or that CDH^DDH is classically hard is far beyond reach. [1] The problem is that attacker might be able to come up with ciphertext second preimage for a broken KEM. The attacker is then able to use this ciphertext to trivally break IND-CCA. Fortunately, it turns out there are no other non-trivial attacks against composite IND-CCA. And then beyond-IND-CCA properties applications might rely on are whole another kettle of fish. [2] Any KEM that fails to be one-way under confirmation is totally broken and unusable for anything. [3] The reason why key reuse with active attacker has higher requirements is that the attacker might be able to probe the private KEM key using malformed ciphertexts (that either fail to decrypt or decrypt to known values depending on the private key). And recovering the private KEM key trivailly breaks security. -Ilari _______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
