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

[Nathanael Ritz <[e-mail]>]

On Sat, Jun 6, 2026 at 6:10 PM Salz, Rich <[e-mail]> wrote:

>
>    - “Machine-checked symbolic analysis [REF] supports preferring hybrid
>    deployment over standalone key establishment, confirming that hybrid key
>    establishment remains secure under compromise of either individual
>    component.”
>
>
> This would only be accurate if we added something like
> If the security of the key exchange is the only consideration in
> development and deployment, …
>

I can see one error in my suggestion is the use of “confirms” over perhaps
“demonstrates”.


> And even then, we’d have to say “A machine-checked symbolic analysis done
> by an individual”
>
> By the time you make it accurate, it’s pointless to say anything.
>

I think it would be accurate enough to say machine-checked symbolic
analysis exists, and such analysis has demonstrated a specific outcome.

I understand the devil is the many detailed caveats left unaddressed by any
such hedged statement.

Cheers,

Nathanael