[TLS] Re: Fwd: New Version Notification for draft-usama-tls-risks-of-mlkem-00.txt

[Muhammad Usama Sardar <[e-mail]>]

Thanks John and Ilari for your valuable feedback. Substantial change is 
the addition of a new section [0] further clarifying my position in the 
light of the FATT process.

Please see inline and let me know if I misunderstood something.

On 19.05.26 12:29, John Mattsson wrote:
> I find the draft title extremely misleading.
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.
> 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].

> A perfectly fine implementation of X25519 in TLS 1.3 is:
>
> [...]
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.
> [...] 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.


>
> *From: *Ilari Liusvaara <[e-mail]>
> *Date: *Tuesday, 19 May 2026 at 11:42
> *To: *[e-mail] <[e-mail]>
> *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.
Yes, these are proof artifacts in ProVerif. Please see [0] for other 
artifacts which are also broken by this change.
> 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