Hi Rich,Respectfully, what you are asking does not seem consistent with the FATT process to me. WG participants doing formal verification are quite limited. Let's warmly welcome their contributions rather than discouraging them.
Nadim's language isn't professional either.I am collecting my thoughts on the next steps and would propose to the WG very soon for consideration in a separate email. I kindly ask you both to please stop this debate in the mean time.
I am not qualified to review your work. Nor am I qualified to review most of what Karthik or Cas writes about. Instead I depend on peer review and I do not want a solo effort put into an RFC without other reviews.
FATT is more than qualified to review Nadim's artifacts, as per process [0], as I already mentioned in [1]. In particular, Karthik -- FATT member -- is ProVerif expert and was one of the authors in S&P paper on the artifacts which Nadim has extended. So he knows all the technical details.
Vincent -- another FATT member -- is the current /main/ maintainer of the tool ProVerif that Nadim has used.
So let's follow the FATT process, please. The WG can then decide based on the outcome. As you say, you are not qualified to review, so please wait for that outcome.
Frankly, do you /seriously/ believe that an /opponent/ of standalone ML-KEM has put in some backdoor in the proof to show that standalone ML-KEM is /secure/? If I were not an expert of ProVerif, I would still have a hard time believing that.
This gives too much credit to one individual’s work that is not in a peer-reviewed journal or conference.Nowhere in the FATT process [2] I see any requirement for "peer-reviewed journal or conference." Let's not make the process more complicated than it actually is.
I am particularly worried about adding this requirement because some WG participants -- like Nathanael -- may not be willing to spend all the time and energies that it takes to write a paper for a peer-reviewed journal or conference but still willing to contribute to formal analysis. We should still welcome all such contributions. Please don't limit the already very limited number of participants doing the verification.
I am also worried that having peer-reviewed journal or conference may significantly delay the standardization process. Remote attestation is a /very/ controversial topic but that's the only reference point I currently have: it took us 2 years to publish analysis of draft-fossati-tls-attestation [3].
Best regards, -Usama [0] https://github.com/tlswg/tls-fatt#working-group-last-call-wglc [1] https://mailarchive.ietf.org/arch/msg/tls/h9NxvOgsGgAHDExGp9pJKABQl_o/ [2] https://github.com/tlswg/tls-fatt [3] https://dl.acm.org/doi/10.1145/3779208.3785387
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
