Thanks Simon, Bas, and Uri for your inputs. Please see inline:
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?
Unfortunately, it's a very hard question for me and I can't answer that until I have /either/ a security proof /or/ an impossibility proof. I currently have neither of those.
All I can attest to at this moment is that it breaks the current ProVerif proofs. I can add a bunch of nits on top in the draft but I am not sure that is useful right now because the top-level issue of commutativity is unresolved. In particular, I haven't seen anyone proposing a fix to the problem highlighted in Sec. 3 [0].
Is there some hope that an modified formal proof can be developed?
There certainly is.
Substantial contributions to the latter effort seems appropriate here.
Any contribution to new proof is very welcome.
I did not see any rebuttal of the salient point that any such gap would apply to X25519MLKEM768 too.
Addressed in [1].
Thank you for yet another attestation to my point that the existing formal analysis needs to be fixed.This is a fatal problem with your formal analysis - so, the formal analysis here is what requires fixing.
Best regards, -Usama[0] file:///home/usama/gitRepos/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#section-3
[1] https://mailarchive.ietf.org/arch/msg/tls/NTGubqR_wSygwxX4_6_yCAhiw4s/
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
