David Stainton <[email protected]> writes: > 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.
+1 -- if we have a FATT process, let's use it, especially now that there are some results to build on, and then use that to improve the document. I still believe this shouldn't be published through the TLS WG, and that independent submission is more relevant for political crypto. /Simon > 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]
signature.asc
Description: PGP signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
