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: [email protected]
To: Muhammad Sardar <[email protected]>,
Muhammad Usama Sardar <[email protected]>
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 --
[email protected] To unsubscribe send an email to [email protected]
_______________________________________________
TLS mailing list -- [email protected]
To unsubscribe send an email to [email protected]
