On Sun, Apr 26, 2026 at 3:17 AM Muhammad Usama Sardar <
[email protected]> wrote:

> Dear Joe and Sean,
>
> Following up with the request below with:
>
>    1. the observation that there has been no objection from the WG yet on
>    this specific request
>    2. some inspiration from our next-door neighbors who have actually
>    already done the formal analysis for EDHOC-PSK with KEM [6]. So it seems
>    justified to get a confirmation via formal analysis for TLS protocol, too,
>    especially given that we claim "high cryptographic assurance."
>
> Thank you for your kind consideration!
>
> Best regards,
>
> -Usama
>
> On 21.04.26 02:25, Muhammad Usama Sardar wrote:
>
> Dear Joe and Sean,
>
> As someone who has been doing the formal analysis of the following drafts
> for the WG:
>
>    1. draft-fossati-tls-attestation
>    2. draft-ietf-tls-extended-key-update
>    3. draft-ietf-tls-pake
>
> and doing some preliminary working for some other drafts, I would like to
> formally request initiation of the FATT process for draft-ietf-tls-mlkem.
> The rationale is that I believe formal methods can provide additional value
> for security considerations of this draft. As an example, it can help
> justify design choices, such as the preference for hybrids.
>
>
The draft does not express a preference either way. Even if it did, I don't
see how the FATT process could help there. I don't see value in applying
the FATT process to dratft-ietf-tls-mlkem.


> I have shared further rationale and a summary of my work-in-progress in
> [5]. Notably:
>
> Approach: *symbolic* security analysis so far (and planned *computational*
> security analysis)
>
> Tool: *ProVerif* so far (and planned *CryptoVerif*)
>
> Please do not hesitate to ask if any further details would be helpful.
>
> Thank you for your kind consideration!
>
> Best regards,
>
> -Usama
>
> [1] https://github.com/tlswg/tls-fatt/pull/16/ <-ready to merge
> [2] https://github.com/tlswg/tls-fatt/issues/19
> [3] https://mailarchive.ietf.org/arch/msg/tls/RupKEHeJdAzxpNEZnRgerk4en1c/
>
> [4]
> https://www.ietf.org/archive/id/draft-usama-tls-fatt-extension-05.html#section-3.2
>
> [5]
> https://www.ietf.org/archive/id/draft-usama-tls-fatt-extension-05.html#section-3.3
>
> [6]
> https://mailarchive.ietf.org/arch/msg/lake/2XGOI9OCwylJUfSCasvvwM2FXmw/
> _______________________________________________
> 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]

Reply via email to