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

[Songbo Bu <[e-mail]>]

Hi all,

Following up on the implementation-test point, I think the artifact would
be most useful if kept small and explicitly non-blocking: a list of
negative cases implementers can run against hybrid key exchange code, not a
condition for progressing the draft.

The cases I would start with are:

   - the negotiated group is hybrid, but one component is missing,
   malformed, or associated with a different group;
   - ECDHE and KEM values are individually valid, but assembled from
   different handshakes or transcript contexts;
   - a peer attempts to continue as standalone ECDHE or standalone ML-KEM
   after a hybrid group was negotiated;
   - the implementation derives application traffic secrets before both
   components have been validated and accepted under the negotiated hybrid
   group;
   - the implementation accepts a hybrid share while logging or exporting
   enough state to make it look like only one component was used.

This would not be a formal analysis result. It is just a practical bridge
from the model’s intended binding property to things that are easy for
implementations to accidentally get wrong.

If others think this is worth capturing, I’d be happy to help turn the list
into a GitHub issue or small PR once the cases are clearer.

Best,
Songbo Bu

On Fri, 5 Jun 2026 09:31:27 +0800, Songbo Bu [e-mail] wrote:

Hi Usama, all,

Thanks. I agree this should not make the draft depend on a full new test
suite before progressing. The useful near-term thing may just be to collect
a small set of negative cases that implementers can run against the
existing artifacts.

The cases I would start with are roughly:

   -

   negotiated hybrid group differs from the group encoded/bound in either
   component;
   -

   one component is omitted, malformed, or fails decapsulation/validation;
   -

   KEM and ECDHE values are individually valid but assembled from different
   handshakes/transcripts;
   -

   a peer attempts to continue as standalone ML-KEM or standalone ECDHE
   after a hybrid group was negotiated;
   -

   application traffic secrets are derived only after both components have
   been accepted under the negotiated hybrid group.

That is not a formal proof obligation, but it would make the intended “both
components are bound and accepted” property easier to check in
implementations. If there is a preferred place for such cases – draft text,
a GitHub issue, or a separate test-artifact note – I can help shape it
there.

Best,

Songbo Bu

On Thu, 4 Jun 2026 21:48:32 +0200, Muhammad Usama Sardar
[e-mail] wrote:

Hi Nadim,

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

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

that:

-

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.

-

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