> Interestingly, despite the availability of scientific methods to identify the best path forward, as proven by Dr. Kobeissi in this thread, there was no interest in treading this path prior to making dangerous recommendations to the populace.
[NR] There is a difference between a peer-reviewed study vs the good faith input of a handful of individual contributors. There is also a difference between availability of results between the good faith input of contributors vs the constraints an author puts themselves under for publication at a top tier security symposium.
From example, the IETF has been notified plenty of times that there are “missing attacks” on the TLS key schedule from existing formal analysis that reportedly affects the security of Remote Attestation over secure channels like TLS depending on the timing of the attempted binding. However, because the study is under presumably double-blind review, the authors are not in a position to disclose exactly what those attacks look like, so the community is left guessing at what mitigations may or may not be possible. This isn’t nefarious — there are plenty of good (scientific) reasons why double-blind review is the way it is. But there is a distinct trade-off.
In contrast, when individuals like myself or others such as Nadim can move quickly to explore an open question like the impact of a KEM on the TLS key schedule vs classical DHE, certain disclosures on List or such related efforts may be treated more seriously than another, even if the outcome between both of them is effectively equivalent (or so one may hope). But who judges that? Prior presence, publication history and visible credentials absolutely affect optics. It just so happens that the “quick” turnaround of the results can be corroborated by separate individuals in this case.That’s all well and good, but it doesn’t necessarily have the same “scientific” standing that a peer-reviewed paper may have. Again, a significant trade-off.
That doesn’t mean a published paper is perfect or that individual good-faith self-publications are totally unreliable. I am just saying that formal analysis isn’t a commodity resource.
> It would be a strong signal should the WG adopt this new custom as a standard, go forward, requiring formal/symbolic analysis prior to making any recommendations.
[NR] And this moves towards the FATT process. While Usama, Nadim and I all expressed interest or “energy” to do independent symbolic analysis to evaluate the impact of PQ-KEM on TLS, none of the above are named members of the FATT team. And the even then, FATT is specifically organized so that it cannot act as an impediment to the normal progress of a draft. Specifically, the TLSWG repo states clearly in part that, “
the working group is under no obligation to follow the FATT recommendations. If the FATT fails to provide output within a reasonable time frame as determined by the working group chairs the processing of the document should continue as normal.” https://github.com/tlswg/tls-fatt
The point is that the TLS FATT team is designed to be a helpful resource — but by design is meant to be *helpful*, not uniquely bindingly authoritative on TLSWG output.
Access to formal analysis is scarce for a reason. It’s complex, the results often appear opaque to non-experts and I would personally expect those who have developed their career around the skill are perhaps less likely to commit to volunteering their time sufficient enough to avoid considerable delays. Of course, I think the community should be very grateful to folks like Nadim who is willing to modernize previously published models and take the results and recommendations seriously. And Usama’s call for new models and soliciting for help in producing them is admirable on its own.
But I guess it is just entirely unrealistic to expect the IETF to demand such work from anyone, either from individuals or TLS FATT team members to the point of declaring deep suspicion if such a scarce resource is not available or called upon.
Further, the UFMRG exists for a reason (also identified by the specified FATT process on the TLSWG GH repo), but if you take a look at that list, it appears there are few souls regularly participating in that space as of late. And I feel like that reinforces my point about how scarce access to formal analysis actually is and why the chairs may hesistate to call for it on one draft or another.
(I have not been part of this particular List long enough yet for me to feel comfortable making any remarks regarding recent debates regarding consensus at all, btw).
Cheers,
Nathanael
