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
signature.asc
Description: PGP signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
