[TLS] Re: FATT Process Updates: FATT process for draft-ietf-tls-mlkem

[David Benjamin <[e-mail]>]

On Sun, Apr 26, 2026, 04:05 Bas Westerbaan <bas=
[e-mail]> wrote:

>
>> The draft does not express a preference either way.
>>
>> Right, but I and at least some others have asked that it should. Some
>> have used the wording 'guidance' and some have used some other wording. But
>> I think that's the crux of it.
>>
> I think there is support for more explicit guidance. There doesn't seem to
> be consensus on which guidance to give.
>
> Even if it did, I don't see how the FATT process could help there.
>>
>> Just to understand better, did you check [0]?
>>
> Yes.
>

I agree with Bas. I see nothing in [0] that would resolve the debate, or
add new information to the discussion. Formal methods are extremely
valuable because they can provide very, very firm answers. But they can
only answer very specific questions. Here, they can tell us whether the
hybrid property is *achieved*, so statements like:

- If you model ML-KEM as broken, then relying on ML-KEM does not work.
- If you model ML-KEM as broken and ECDH as fine, or vice versa, the hybrid
is still fine because of the one you assumed was fine in your model

Neither of these (near tautological) statements is in question. While
formal confirmation of verifiable assumptions is great, I don't think the
WG needs to block on them at this point. (Unless you're suggesting we block
the hybrid draft publication on this work? I wouldn't support that.)

Rather, the debates here relate to trade-offs around how valuable the
hybrid property is, what the costs are, whether the outcome of those
trade-offs is universal, and what to do with the document given the state
of affairs. Those are not formal methods questions. I see [0] tries to
answer those by making claims about security improvements, security
regressions, and a lack of "authentic references" for competing concerns.
These are not formal methods results, but one point of view on these
subjective questions. Framing them as formal methods won't settle the
debate.

I agree with the chairs' original decision here. Sending this through FATT
seems unnecessary, and not a good use of the WG's or the FATT's time.

David