On Mon, May 25, 2026 at 3:19 PM Simon Josefsson <simon= [email protected]> wrote:
> Muhammad Usama Sardar <[email protected]> writes: > > > FWIW, my point is simply: > > > > 1. Existing proofs of TLS in ProVerif are based on commutativity > > (verifiable directly by several links of repos provided) > > 2. Commutativity does not apply to ML-KEM in TLS > > > > and hence, a new proof is required. > > I find the above a good summary of the situation, and I worry that this > concern get lost in this thread. > > Introducing ML-KEM in a way that breaks our formal analysis of TLS seems > like a serious problem to me. > I did not see any rebuttal of the salient point that any such gap would apply to X25519MLKEM768 too. I'm a proponent of formal analysis, and would like to see more of it. The way it's being wielded here though, makes me question my position. Best, Bas
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
