Hi, I'd like to voice my support for including:
1. FATT "assessment" of formal analysis artifacts: A proper assessment framework for the formal analysis work that has been conducted. 2. Inclusion of results of formal analysis: The community should have visibility into the formal analysis results to make informed choices about this proposal. PR#20 provides a solid foundation for this. I believe these additions strengthen the proposal by providing the technical rigor and transparency needed for proper evaluation. Best regards, David Stainton On Tue, Jun 9, 2026 at 3:19 AM Muhammad Usama Sardar <[email protected]> wrote: > > [concluding email proposing the way forward; sorry for the length] > > Hi John, all, > > I took a few hours to read the whole thread again and carefully put this > together. Thanks for taking the time to read it and sharing your opinion. > > On 08.06.26 08:28, John Mattsson wrote: > > I don’t think the proposed PR is technically correct. The quantum-vulnerable > algorithms secp256r1, secp384r1, X25519, and X448 are also marked > RECOMMENDED=Y. Moreover, the fact that TLS currently recommends standalone > quantum-vulnerable key exchange more strongly than standalone > quantum-resistant key exchange is probably not something we want to codify in > an RFC. > > You are right. I first updated it to scope it to PQ-secure algorithms but > your next point is still valid. > > The purpose of the IANA RECOMMENDED column is precisely to avoid embedding > such these kind of policy decisions in RFC text. > > Fair point, that resolves my point. I have closed that PR. > > # My proposed next steps > > My remaining objections are: > > FATT review of artifacts as per FATT process [0]: FWIW, having missed initial > FATT review may not necessarily imply that we also miss the final FATT review > too. I suspect not many WG participants actually know (as I see from the > email from Rich) about this and that is perfectly fine because since the > start of FATT, no draft has yet reached that stage with artifacts -- recall I > pushed back on the ask for a proof for 8773bis (hence emphasis on with) -- > but "assessment" of analysis is part of the process (please see [0]): > > "If some formal analysis has been done then the chairs will request that the > FATT point person for the document take the analysis that has been done for > review by the FATT during WGLC. This request will contain a link to the > current document, a link to the analysis, and WGLC time frame. The FATT will > be requested to provide an assessment of whether the document meets the > claimed security properties." > > As I understand, during WGLC is due to process reasons. In any case, the > sooner the FATT review is requested the better. Artifacts are available; if > author of draft is fine, these can probably be sent now to FATT with say 2 > weeks period that they can assess it at their convenience. As delta to reftls > is quite small, it would likely be easy to assess. As other debates on ML-KEM > are still happening and these debates do not seem to me to be moving towards > convergence and I don't expect things to magically settle in 2 weeks, there > is absolutely no "delay" added by FATT review by any means. > > > PR#20 or #22 or something on these lines on symbolic analysis of integration > of KEMs in TLS with citation of paper or artifacts is added. I believe it is > important to have this for the readers -- particularly non-cryptographers -- > in the security considerations to make informed decisions. I believe citation > of paper should be conditional on revising the paper to make it more > scientific and professional -- as mentioned in Yaakov's review [2]. I had > actually skipped the introduction and background and focused on model and > properties. I saw introduction after his review and respectfully, > introduction needs a serious revision. > > Please note that contrary to what someone said, my PR#22 is not "competing" > with any other PR. It is just offering one potential alternative for PR#20, > because I saw some people opposed it. In particular, PR#20 works perfectly > for me, and I'll happily close PR#22 if people agree to PR#20. Choose > whichever you like as a starting point for wordsmithing. > > Hopefully, none of the above two are difficult and people can agree on > something to move things forward rather than looping repeatedly. > > # My personal position > > I am not sure if any of the above two points would help any of other ca. 24 > opposing. At least with these two, I would stop opposing and move to 'no > opinion' for the draft. The crypto involved in ML-KEM is too complex for me > to check and more secure alternatives like X25519MLKEM768 are available. I > think non-cryptographers like me can just wait to see whether ML-KEM or > X25519 breaks first. But whichever breaks first, X25519MLKEM768 will still be > secure. This hampers my support for standalone ML-KEM. > > This is my personal position. WG is free to ignore one or both of above > items, in which case I will stay opposed (but not strongly), as these are > important considerations to me, and I am fine to be in the rough if others do > not share this opinion. I believe one reason of formal analysis is to get > assurance ourselves, and another IMHO equally important reason is to get it > evaluated by experts and put it in security considerations for the community, > so that community can make reasonable decisions. > > Key reuse vulnerability is fixed via 8446bis; thanks to John for substantial > technical guidance in modeling this and to all who offered attestation for > the change. Moreover, integration of ML-KEM in TLS is checked in symbolic > model. That's almost as far as I could envision and help. Explaining why > ML-KEM itself is secure is up to cryptographers. Symbolic analysis can only > take that as an assumption and check the integration in TLS, and thanks to > Nadim, that is done and that is sufficient for me. There are some nits and > more details can be added but the central concerns we discussed are resolved. > As I point out in the draft [1] for anyone interested, CFRG is starting > something on cryptographic analysis. I will remain curious of what they would > have to offer us. > > I would note that in the process, I may have offended several people, in > particular where I questioned things regarded "obvious" or "intuitive." I > sincerely apologize for that. Intuition and actually doing formal proof are > two different things. Anyway, I would like to thank Yaakov for providing me > substantial technical guidance for the formal modeling. Thanks to Nadim for > doing it way faster than I could have. > > One request I have is: Perhaps people -- both sides -- could be nice to bring > in novel arguments on list and not repeat arguments already captured in [3]. > If there are novel arguments not already captured in [3], I would be > interested in hearing them to proceed further with the ISE path. > > This concludes my intervention. > > Best regards, > > -Usama > > [0] https://github.com/tlswg/tls-fatt#working-group-last-call-wglc > > [1] > https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-02.html#section-6.7-2 > > [2] https://mailarchive.ietf.org/arch/msg/tls/FHnv98ny7QH4-3n2KvML6pE4tBc/ > > [3] > https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-02.html#section-6 > > _______________________________________________ > TLS mailing list -- [email protected] > To unsubscribe send an email to [email protected] _______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
