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

[Muhammad Usama Sardar <[e-mail]>]

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