Hi, Thank you David, Simon, Nadim, and Jacob for the attestations.
Thank you Ilari for the feedback. You are making good points which I have tried to address in the editor's copy.
In general, there seems to be high momentum right now with at least 2 other WG participants conducting the formal analysis. Typically, finding volunteers is the hardest part of this process. Given the interest, initiating the FATT review feels like a constructive next step.
Could you also please share your perspective on why 8773bis needed to go to FATT but not a paradigm change like standalone ML-KEM?
It is worth noting that FATT review is harmless: 1. 'Nothing required' is a perfectly valid outcome. 2. WG is /not/ obliged to follow the recommendation of FATT. I have added it in the draft [3] anyway for those who may be worried.If there is any ambiguity, I can explain it further when I take the floor in Vienna.
I have added a few justifications [0] in the draft. Could you please share the specific issues you see in [0]? That may not be very satisfying for a cryptographer, but I don't see anything wrong from a /symbolic/ perspective. If we put in all details of cryptography in the model, the /symbolic/ analysis may become redundant with the /computational/ model, and hence may become a duplicate effort losing the real complementary benefit /symbolic/ analysis could bring.I do not think there is any justification for doing FATT process for stand-alone ML-KEM, but not for X25519MLKEM768.
Sure, if we find a flaw which applies to hybrid, then [1] applies, e.g., chairs may do a quick WGLC and IETF LC requesting to keep its place in publication queue.Any flaw in integration of the former is highly likely to directly translate into a flaw in the latter — due to the hybrid property.
One of the motivations of formal analysis is to test things we assume to be highly likely. There are so many examples from history here.However, I think it is extremely unlikely that any such flaws exist.
You are right. That was admittedly very informal and with sincere apologies, I revoke the quoted attestation, and have tried to make it more precise. What I meant was DHKE part remains symmetric as before -- at least from symbolic analysis perspective, which is what I am currently interested in.The arguments about "some level of symmetry" are unsound.
Additional PQ component is concatenated to it.
From such soundness, doesn't it naturally follow that hybrids are at least as strong as the stronger of the two components?If such a statement is added, I believe that addresses the concerns of some.Moreover, I do not think it is possible to prove soundness of X25519MLKEM768 without proving soundness of stand-alone ML-KEM — as soundness of X25519MLKEM768 includes it having hybrid property, meaning it is still secure if ML-KEM is secure, no matter how throughly X25519 is destroyed.
Anyone in the IETF community -- and more broadly in the world -- who will do ProVerif confirmation for the minimal viable modeling [2] that we have collectively found on the list and will answer any questions I may have. IIUC, at least two other WG participants are already working on it.And who in the IETF community do you trust to determine that?
I support initiating the FATT process here, and I support the work Usama is doing to use symbolic models to better understand the protocol's security properties. Even where existing proofs give us confidence, having an explicit symbolic analysis of the standalone-KEM case is the kind of thing that's worth doing rather than assuming, and there are clearly participants willing to do it.+1 from me.
Thank you for your attestation.
+1 The entire idea behindhttps://github.com/tlswg/tls-fatt seems like a good thing, and I wonder what would warrant side-step it.
Thank you for your attestation.
In particular, I am curious to see how the FATT process will reconcile NIST's requirements with TLS's choices.For example, does TLS with ML-KEM now require a NIST certified DRBG?
I have added it in [2] for WG discussion. /Computational/ analysis may be helpful here. I think it will be good to state it clearly in the security considerations of draft-ietf-tls-mlkem.
I don't see any mention of patents in your draft. This seems concerning when the world-wide patent waiver license applies only to the exact specification which I understand imposes using a NIST certified DRBG.It was unintentional miss as I am not a patent expert to do a proper analysis but I have mentioned it in [4].Hopefully you will also include at least a basic analysis of these matters.
Best regards, -Usama[0] https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#name-fatt-review-for-hybrid-key-
[1] https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#name-what-if-issue-is-found
[2] https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#name-minimum-viable-modeling
[3] https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#name-fatt-review-is-harmless
[4] https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#name-patents
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
