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

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

Dear Joe and Sean,

I believe I have collected sufficient attestations from the WG that a 
new proof is required for draft-ietf-tls-mlkem.

As I understand, apart from me, there are at least 2 other WG 
participants (Nadim [0] and Nathanael [1]) who are /already/ doing or 
have /volunteered/ to do independent formal analysis in ProVerif. I take 
that as a strong attestation that there is enough WG energy to do the work.

So with these attestations, I would like to request the initiation of 
the FATT process for draft-ietf-tls-mlkem. I believe it would be good to 
have FATT's evaluation of the artifacts that would be eventually 
developed by these efforts. Thank you for your kind consideration.

In addition, I believe all concerns have been addressed in this version. 
Summary of major changes is:

  * Added justification based on the FATT process: Section 4
  * Reorganization, specially in motivation (Section 1.1)
  * Added some common arguments: Section 6
  * Comparison with hybrid ML-KEM in Section 4.1
  * Clarification of what "breaking" means in Section 3

For those who haven't had a chance to check the draft yet, more feedback 
on Sec. 3 and 4 is very welcome. For discussion of details of modeling, 
please contact me off-list.

Best regards,

-Usama

[0] https://mailarchive.ietf.org/arch/msg/tls/pZe6luYQeT4GhbOc1FE1xi-Lmzc/

[1] https://mailarchive.ietf.org/arch/msg/tls/S5QioGFa3T3AFWIAjsNg8BFy5Co/



-------- Forwarded Message --------
Subject: 	New Version Notification for 
draft-usama-tls-risks-of-mlkem-01.txt
Date: 	Fri, 29 May 2026 03:02:54 -0700
From: 	[e-mail]
To: 	Muhammad Sardar <[e-mail]>, Muhammad 
Usama Sardar <[e-mail]>



A new version of Internet-Draft draft-usama-tls-risks-of-mlkem-01.txt 
has been
successfully submitted by Muhammad Usama Sardar and posted to the
IETF repository.

Name: draft-usama-tls-risks-of-mlkem
Revision: 01
Title: Potential Risks of Standalone ML-KEM in TLS 1.3
Date: 2026-05-29
Group: Individual Submission
Pages: 16
URL: https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.txt
Status: https://datatracker.ietf.org/doc/draft-usama-tls-risks-of-mlkem/
HTML: https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.html
HTMLized: 
https://datatracker.ietf.org/doc/html/draft-usama-tls-risks-of-mlkem
Diff: 
https://author-tools.ietf.org/iddiff?url2=draft-usama-tls-risks-of-mlkem-01

Abstract:

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. In this draft, we show *exactly* where the ProVerif
proofs break, namely transition from symmetric DHKE to asymmetric
KEM. More specifically, the existing proofs of TLS in ProVerif are
based on commutativity property, whereas commutativity does not apply
to standalone ML-KEM in TLS.

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, formally request the chairs to
initiate the FATT review of standalone ML-KEM in TLS. A few WG
participants have already volunteered to do formal analysis in
ProVerif.

This draft also offers some preliminary discussion to help the
developers and policy makers make informed choices. Finally, the
draft also aims to reduce the endless repitition of arguments from
both sides presented on several lists by documenting these arguments
so they can simply be referred to.



The IETF Secretariat