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

[Muhammad Usama Sardar]

Thanks all for the comments. Some thoughts inline:

- This concerns KEMs in general and is independent of draft-ietf-tls-mlkem, ML-KEM, and PQ. [...]

I don’t think a formal FATT process should be started. I want X25519MLKEM758 published as soon as possible. Can you explain why the synmmetric argument in your draft does not hold for hybrid key exchange?

FWIW, I tried to address the concern on hybrid/X25519MLKEM758 already in Sec. 4.1 [0].

I would like to clarify that I am not at all proposing to block X25519MLKEM758. Please let me know exactly where there is this ambiguity in Sec. 4.1. Happy to rephrase it or clarify it.

 An academic paper, together with discussion on the TLS WG mailing list, seems more appropriate.

The research work for paper will proceed in parallel. Paper publication -- at good venues -- is a long process. I think it is better to start FATT process now to avoid unnecessary delay at the end.

- A proof in the symbolic model would be valuable, but not required, as there are already other proofs supporting the security of KEM use in TLS 1.3.

FWIW, I believe /symbolic/ and /computational/ models are complementary and not a substitute of each other.

Based on the results of the idealized KEM model variant (that I remain open to collaborate further on), I found nothing from the verification output that gives me any reason for concern compared to the DH model evaluating the same properties.

FWIW, from a quick look, ISTM that it simply replaces ideal DHKE by ideal ML-KEM but IMHO we instead need to focus on the more security-critical questions about integration, as Nadim has mentioned. I'll submit a thorough review of nits later off-list but a few high-level observations to consider for security considerations of draft-ietf-tls-mlkem:

1. ISTM that Yaakov's point quoted below does not seem to be addressed
   because client and server are assigned static roles in the model.
   When it will be modeled as non-static, I would be interested to see
   whether the asymmetry issue becomes visible in at least a couple of
   properties. I consider it very critical for security considerations
   of draft-ietf-tls-mlkem and this is the key point of my draft.

    So, you are not really using the fact that either side could have initiated 
the TLS [...]

2. ISTM that the failure modes proposed by Yaakov and Nadim are also
   not modeled.
3. A large part of the problem is the careful investigation of what to
   model, under what threat model, under what system model, under what
   implementation scenarios etc. I believe all of that needs to be
   clearly fleshed out in the repo. I think some of this is important
   for security considerations of draft-ietf-tls-mlkem. I was not able
   to find much about any of those in readme of repo.
4. I would have liked to see some analysis about any subtle cases where
   hybrid ML-KEM in TLS is /not better/ than standalone ML-KEM in TLS.
   My understanding is that some participants would like to see some
   statement.
5. I believe brainstorming about some robustness (vs. security)
   properties would also be useful. Even if the security properties
   hold, does it make side-channel leakage easier?

I stated clearly that “I am interested in collaborating on new ProVerif models that explore PQ crypto as well.” I did not share any opinion on whether a proof was required for anything.

Sure, and just to clarify: there were two separate paragraphs in my email and mention of your name was in the 2nd paragraph, which seems correct to me, as you /are/ indeed already doing analysis.

Also please note "As I understand" in my sentence. So this is what I understood.

I expect any surprise to come from the integration details (transcript binding, key schedule, agreement), not from a headline about ML-KEM itself.

Please note that by "Standalone ML-KEM /in TLS 1.3/," I mean exactly the former. Please also note that the draft explicitly talks about the former in Sec. 1.1.1, e.g., see [1,2]. I'll emphasize it even more in the next version.

"I expect nothing crazy" is exactly when symbolic re-analysis has historically paid off in TLS 1.3: Selfie on external PSK, the post-handshake authentication and agreement subtleties, the 0-RTT replay framing, all surfaced by someone keeping a current model around and poking the new feature, even when the primitives were boring.

I would actually add /remote attestation/ to it. When we started back then, people thought it's just a small addition as in just a nonce and some extension of Certificate and we'll be done in something like a few months. It's been 3+ years and what ProVerif has shown is attacks after attacks: replay attacks, relay attacks, high-severity CVE of score 7.8, ...

A maintained, KEM-capable reftls-style model is infrastructure that pays off on the *next* handshake change too, regardless of whether ML-KEM produces a headline.

Exactly.


Best regards,

-Usama

[0] https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.html#section-4.1

[1] https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.html#section-1.1.1-3

[2] https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.html#section-1.1.1-4.3.1

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
TLS mailing list -- tls@ietf.org
To unsubscribe send an email to tls-le...@ietf.org