[TLS] Re: FATT Chance: On the Robustness of Standalone and Hybrid ML-KEM Key Exchange in TLS 1.3

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

Hi Nadim,

Awesome work. Thanks a lot. That resolves my concern.

Before we put this discussion behind us, I would like to suggest that:

 1. we put artifacts in front of FATT for evaluation: It would be good
    to have the artifacts evaluated once, so that we can keep using them
    in the future for all PQ extensions.
 2. we add a statement on preference of hybrids and refer to the paper
    in the security considerations of draft-ietf-tls-mlkem.

1 would be nice -- the earlier the better. But IMHO 2 is essential.

One small note: I noticed that in your paper, you cite link to editor's 
copy [0]. I have published -02 [1] -- in the state it was -- for you to 
have a permanent citation, because the editor's copy will keep changing 
-- and has already moved to the next steps -- and it might be confusing 
for the reviewers/readers to find a mismatch in the paper and the 
reference. -02 is just for you; others don't need to worry about it and 
there is nothing new to read in it.


> One implementation-facing angle that may be worth spelling out, even 
> if it is outside what the symbolic model can prove, is which negative 
> tests would best catch hybrid-specific integration mistakes.
I think this is very valuable and practically useful suggestion to craft 
tests and folks are welcome to work on it. But I am more than happy with 
what has been achieved. Thanks Nadim.

> Any kind of Undefined Behavior in implementation would compromise both.
I believe one can actually do formal verification on the real code to 
have high assurance that there is no Undefined Behavior.

> I think some of the informal claims are stronger than what
> this paper proves. This does not matter for ML-KEM or ECC hybrids
> thereof — but could matter for another KEM.
Could you please explicitly share those differences?

> Note that once a CRQC emerges, which some people say may happen very 
> soon, [...]
and some people have argued it may never occur [2]
> I think formal analysis in the not so distant future should focus on 
> quantum attackers and treat ECC and RSA as not providing any security.
Once the WG agrees on setting them to 'N' or 'D' probably that will be 
the appropriate time to update the formal models.
> Many TLS libraries enforce handshake timeouts, so unless the key 
> exchange algorithm is completely broken, an attacker cannot 
> practically keep a connection open long enough to forge the Finished 
> message.
Is the handshake timeout typically pre-configured or dynamically 
selected? Does anyone have datapoints on handshake timeout in common TLS 
libraries?

Actually, some people propose remote attestation within the handshake, 
which requires significantly increasing the timeout. In particular, it 
adds the time for generation and appraisal of Evidence within the 
handshake, which gives the adversary plenty of time to do a lot of 
interesting things.

> It is great that TLS WG have clarified that static keys MUST NOT be 
> used for key exchange. This significantly lower the risk for these 
> kind of attacks.
Agree. It would have been beneficial to do it long time ago, but better 
late than never.


Best regards,

-Usama


[0] 
https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html

[1] https://datatracker.ietf.org/doc/draft-usama-tls-risks-of-mlkem/02/

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