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

[Simon Josefsson <[e-mail]>]

David Stainton <[e-mail]> writes:

> I support initiating the FATT process here, and I support the work Usama is
> doing to use symbolic models to better understand the protocol's security
> properties. Even where existing proofs give us confidence, having an
> explicit symbolic analysis of the standalone-KEM case is the kind of thing
> that's worth doing rather than assuming, and there are clearly participants
> willing to do it.

+1

The entire idea behind https://github.com/tlswg/tls-fatt seems like a
good thing, and I wonder what would warrant side-step it.

/Simon

> +1 from me.
>
> David
>
> On Sun, May 31, 2026 at 1:15 AM Nathanael Ritz <[e-mail]> wrote:
>
>> Hi Usama,
>>
>> I have some feedback re: "Justification based on FATT Process" (sect. 4)
>> for the -01 draft [0].
>>
>> In sect. 4-6.2.1 you highlight "3 public forks". E.g.,
>>
>> - jupenur/formal-spec-id-crisis
>> - nathanaelritz/formal-spec-id-crisis [1]
>> - telephonicrobotics/formal-id-crisis-spec [2]
>>
>> I wanted to clarify that I control both repos, `telephonicrobotics` and
>> `nathanaelritz`. I.e., `telephonicrobotics` is my GH username and I use
>> `nathanaelritz` for my more front-stage work. Additionally, it appears both
>> links point directly to the original init commit #a25631b [3], [4] instead
>> of hyperlinking to the main branch for either repository -- although that
>> could just be a GH artifact.
>>
>> Truth be told, the cloned repo at
>> `telephonicrobotics/formal-id-crisis-spec` is more of an artifact than
>> anything actively developed. As it's presented, I'm afraid this may cause
>> some readers to accidentally perceive my substantive contributions to this
>> code base as larger than they currently are.
>>
>> Therefore, for the -02 revision of your draft, I propose dropping the
>> citation for `telephonicrobotics/formal-id-crisis-spec` altogether and
>> hyperlinking directly to the main branch of my main fork at
>> `nathanaelritz/formal-spec-id-crisis` [5] for maximum clarity.
>>
>> Thanks,
>> Nathanael
>>
>> [0]
>> https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.html#name-justification-based-on-fatt
>> [1]
>> https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.html#section-4-6.2.2.2.1
>> [2]
>> https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.html#section-4-6.2.2.3.1
>> [3]
>> https://github.com/nathanaelritz/formal-spec-id-crisis/blob/a028cec823b7d9bf13dd5a1dd71ab14c75b1a83d/TLS-a/fix/tls-lib-simple.pvl#L38-L41
>> [4]
>> https://github.com/telephonicrobotics/formal-id-crisis-spec/blob/c1953127ce004e51b888250591ec9971ad50e98c/TLS-a/fix/tls-lib-simple.pvl#L38-L41
>> [5] https://github.com/nathanaelritz/formal-spec-id-crisis/tree/main
>>
>>
>> On Fri, 29 May 2026 at 04:38, Muhammad Usama Sardar <
>> [e-mail]> 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.
>>>
>>> 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]>
>>> <[e-mail]>, Muhammad Usama Sardar
>>> <[e-mail]>
>>> <[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]
>>>
>> _______________________________________________
>> TLS mailing list -- [e-mail]
>> To unsubscribe send an email to [e-mail]
>>
> _______________________________________________
> TLS mailing list -- [e-mail]
> To unsubscribe send an email to [e-mail]
>