Please see inline and let me know if I misunderstood something.
On 19.05.26 12:29, John Mattsson wrote:
Thanks for pointing this out. I have added "potential" to address this point. From a formal perspective: until there is a proof, there are risks.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.
Maybe I should have actually cited the original artifacts by Karthik et al. Specifically, the point under discussion in Sec. 2.1 of -00 can be seen exactly in their model [1]. Several years ago I basically started with their model of draft-20 as a baseline and did the following extensions:
* fixed the key schedule * updated to the RFC8446bis * integrated attestation (such as draft-fossati-tls-attestation)I have a hard time convincing myself to attest to "shortcomings" in the proof models. There /may/ be multiple ways to model and they may /all/ be correct. My position is that this is correct modeling. At least I don't see why proof via commutativity is wrong.
Whether this is the /best/ way to model TLS 1.3 is questionable, and probably the best person to provide this justification is Karthik because I /extended/ his models. But then we come back to the point of contacting FATT [2] because he is in FATT.
Anyway, whether it is /correct/ (or not) is probably a separate question. In my view, it still seems to perfectly meet the criteria for FATT review [0].
Thank you. This is very helpful. But IIUC, this shows how X25519 can be implemented as a KEM, but does not fix the commutativity problem highlighted in Sec 2.1. I believe something to replace that commutativity is still required.A perfectly fine implementation of X25519 in TLS 1.3 is: [...]
[...] Therefore, if a re-evaluation of formal proofs is warranted, it should focus on standalone X25519 and standalone P-256.
I would be happy if my artifacts are sent to FATT for re-evaluation. Paper and repo are both cited in the draft. Artifacts are well-commented. I will try my best to answer any questions they may have.
Yes, these are proof artifacts in ProVerif. Please see [0] for other artifacts which are also broken by this change.*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.txtOn 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.
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.
I believe "will show" and actually showing are two different things. If the latter is done and convincingly shown, at least I'll stop objecting to draft-ietf-tls-mlkem.
I am not a cryptographer and I have difficulty understanding how to fold rest of your points into a symbolic proof in ProVerif. Could you please clarify more specific to Sec. 2.1 of -00 as in what change I should make in my proofs at the symbolic level.
Best regards, -Usama[0] https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#name-justification-based-on-fatt
[1] https://github.com/Inria-Prosecco/reftls/blob/634f7da5940f8d1f09cfcd56280b4ef3b533df6b/pv/tls-lib-draft20.pvl#L45-L48
[2] https://www.ietf.org/archive/id/draft-usama-tls-fatt-extension-07.html#section-3.2
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
