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

[Jacob Appelbaum <[e-mail]>]

Hi Usama,

On 5/29/26 12:31, Muhammad Usama Sardar wrote:
> 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.

Agreed.

> 
> 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.
> 

I would like to see the FATT process completed for the issues that you 
have raised.

In particular, I am curious to see how the FATT process will reconcile 
NIST's requirements with TLS's choices.

For example, does TLS with ML-KEM now require a NIST certified DRBG?

If so, I don't see that requirement written down in any draft or RFC. 
Did I miss it?

If not, then how can certain design changes imposed by NIST on Kyber be 
considered to have the same requirements and constraints as the 
resulting ML-KEM NIST standard?

> 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
> 

I don't see any mention of patents in your draft. This seems concerning 
when the world-wide patent waiver license applies only to the exact 
specification which I understand imposes using a NIST certified DRBG.

Hopefully you will also include at least a basic analysis of these matters.

> 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.
> 

I will contact you off-list for discussion of modeling and independent 
verification of modeling results.

Kind regards,
Jacob Appelbaum

> 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
> 
> 
> 
> _______________________________________________ TLS mailing list --
> [e-mail] To unsubscribe send an email to [e-mail]