This is a fatal problem with your formal analysis - so, the formal analysis here is what requires fixing. — Regards, Uri
Secure Resilient Systems and Technologies MIT Lincoln Laboratory > On May 25, 2026, at 09:20, Simon Josefsson > <[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. > > Is this a fatal problem with the ML-KEM proposal? Is there some hope > that an modified formal proof can be developed? Substantial > contributions to the latter effort seems appropriate here. > > /Simon > _______________________________________________ > TLS mailing list -- [email protected] > To unsubscribe send an email to [email protected] > <signature.asc>
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
