Hi all, Comments in-line with [NR] below.
On Sat, 6 Jun 2026 at 01:48, Jacob Appelbaum <[email protected]> wrote: >> On 6/6/26 08:25, Nadim Kobeissi wrote: >> Hi Nathaniel, >> [...] >> I don’t appreciate your implying that just because I’m not targeting a venue that my results are somehow less comprehensive or reliable. [...] if you want to question the reliability of the results, I suggest you do so by finding concrete issues. > I read the emails the same way. I am glad to see that it appears to be a misunderstanding. You do not deserve any shade or mistreatment. > [NR] To start, I regret not quoting Nadim's entire email [0] earlier, as that omission displaced the substantive context of Nadim's original message. The entire email is quoted below in full for reference. Second, I am sorry that Jacob expressed sharing a similar negative read. In the hope of avoiding further misunderstandings, I would like to directly address Nadim's earlier concerns with my earlier email to Andrew [1] more directly. I want to re-iterate that the email to Andrew on-list was intended to address concerns related to the IETF process and was not meant to be understood as "shade," "mistreatment," or any critique of Nadim's work in any way. On Sat, 6 Jun 2026 at 00:25, Nadim Kobeissi <[email protected]> wrote: > I don’t appreciate your implying that just because I’m not targeting a venue that my results are somehow less comprehensive or reliable. > [NR] In my email to Andrew on-list, I shared my understanding that "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." [emphasis added]. Additionally, I noted my understanding that "the authors are not in a position to disclose exactly what those attacks look like." In that regard, I was referring to the upcoming artifacts, not the CVE disclosure. Usama has since stated clearly on the authors' behalf that "A promise to release artifacts under Apache-2.0 license was already made."[2]. I also indicated my understanding for the position Usama and collaborators may be in, which makes sense to me why those specific artifacts are not ready to share with the IETF yet. In contrast, the actual amount of time between when Nadim indicating he would produce his own models on May 28th [3] and the start of this thread on June 4th [4] was well under even 10 days. My comments highlighting Nadim's high priority and "quick turnaround" of available artifacts—including updates to the reflts models, the hybrid analysis and the paper—were not meant to imply anything negative about the quality or effort of the work! Of course, I did speak of a "significant trade-off" in my email to Andrew, and it's a trade-off that Usama himself implicitly raised when he initially suggested on-list that perhaps the WG would put Nadim's new artifacts "in front of FATT for evaluation." Usama justified this further by stating, "it would be good to have the artifacts evaluated once, so that we can keep using them in the future for all PQ extensions."[5] Usama's call for the TLSWG to review Nadim's work so the group can "keep using [the artifacts] in the future" does not appear to be an established process for this WG. Nevertheless, I believe Usama's suggestion highlights the implicit "trade-offs" I was trying to point to in my email to Andrew when I rhetorically asked "But who judges [...]?" On Sat, 6 Jun 2026 at 00:25, Nadim Kobeissi <[email protected]> wrote: > [...] if you want to question the reliability of the results, I suggest you do so by finding concrete issues. > [NR] Nadim, I hope my position is clearer now: I had no intent to question the reliability of your results. FWIW, my own efforts with ProVerif aim to evaluate constructive mitigations for naive binders with TLS+RA [6, 7], a subject well outside the scope of the TLSWG (and in-scope with SEAT). On Sat, 6 Jun 2026 at 01:48, Jacob Appelbaum <[email protected]> wrote: > [...] Furthermore, your work here is excellent and the new models are extremely useful. [...] > > Thank you Nadim! Thank you also to Usama for making this discussion happen! > [NR] +1 Cheers, Nathanael [0] https://mailarchive.ietf.org/arch/msg/tls/MEfHMVi--SCaD-g0RdVP22UHZbw/ [1] https://mailarchive.ietf.org/arch/msg/tls/YHkwqaDfeEE0ArDD7o1E5o2f_J8/ [2] https://mailarchive.ietf.org/arch/msg/tls/RIvIlgV7yt_8esPOgbzklDT71LA/ [3] https://mailarchive.ietf.org/arch/msg/tls/pZe6luYQeT4GhbOc1FE1xi-Lmzc/ [4] https://mailarchive.ietf.org/arch/msg/tls/yDET33KZbtU85IqrZ0kuZG4nUMw/ [5] https://mailarchive.ietf.org/arch/msg/tls/zsIwd8a_gclKVit7rwXft6kckUA/ [6] https://github.com/ultravioletrs/cocos/security/advisories/GHSA-vfgg-mvxx-mgg7 [7] https://github.com/nathanaelritz/formal-spec-id-crisis/blob/main/TLS-a/README.md On Sat, 6 Jun 2026 at 00:25, Nadim Kobeissi <[email protected]> wrote: > Hi Nathaniel, > > The reasons why I wouldn’t submit my analysis to top-tier conferences are: > > 1) The paper’s too short, > 2) The findings aren’t novel or surprising. > > When we submitted our previous analyses, we addressed 1) by adding > CryptoVerif models and a reference implementation, and 2) by finding > attacks. > > I don’t appreciate your implying that just because I’m not targeting a > venue that my results are somehow less comprehensive or reliable. I wrote > my latest analysis with serious effort, having done my PhD mostly on > ProVerif and having more than a decade of ProVerif experience. and if you > want to question the reliability of the results, I suggest you do so by > finding concrete issues. I found your email very annoying. > > Nadim Kobeissi > Symbolic Software • https://symbolic.software > On Sat, 6 Jun 2026 at 01:48, Jacob Appelbaum <[email protected]> wrote: > Hello Nadim, > > On 6/6/26 08:25, Nadim Kobeissi wrote: > > Hi Nathaniel, > > > > The reasons why I wouldn’t submit my analysis to top-tier conferences > are: > > > > 1) The paper’s too short, > > 2) The findings aren’t novel or surprising. > > > > When we submitted our previous analyses, we addressed 1) by adding > CryptoVerif > > models and a reference implementation, and 2) by finding attacks. > > > > I want to push back here and say that you are underselling your work. I > would not reject this kind of paper as a PC member of a conference. > > There are several additional modeling improvements for related drafts > that could be made where it would probably be great at a conference. I > stress, could, but not must. > > Part of the finding that is novel is that the IETF didn't require this > work, that important people in the IETF are discouraging the use of the > FATT, and maybe the IETF will continue to push for pq only constructions > against the scientific results. > > I hope that the latter is not true, but your work has put that very > point to the test. Thank you for advancing the discussion with your > contributions. > > > I don’t appreciate your implying that just because I’m not targeting a > venue > > that my results are somehow less comprehensive or reliable. I wrote my > latest > > analysis with serious effort, having done my PhD mostly on ProVerif and > having > > more than a decade of ProVerif experience. and if you want to question > the > > reliability of the results, I suggest you do so by finding concrete > issues. I > > found your email very annoying. > > > > I read the emails the same way. I am glad to see that it appears to be a > misunderstanding. You do not deserve any shade or mistreatment. > > Furthermore, your work here is excellent and the new models are > extremely useful. I have run the verification of the new pq models and > the results appear to match what is claimed in your paper. I have not > had time to check carefully but so far everything looks great. I will > think about all of the resulting verification runs more carefully and > than I will send feedback off-list. > > Thank you Nadim! Thank you also to Usama for making this discussion happen! > > Kind regards, > Jacob Appelbaum > > > Nadim Kobeissi > > Symbolic Software • https://symbolic.software > > > >> On 5 Jun 2026, at 9:14 PM, Nathanael Ritz <[email protected]> wrote: > >> > >> > >> Hi Andrew, > >> > >> Comments inline with [NR]. > >> > >> On Fri, Jun 5, 2026 at 11:58 AM Andrew Lee <[email protected] > >> <mailto:[email protected]>> wrote: > >> > >> > >>> > 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. > >> > >> > >> > [snip] > >> > >> *> 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 > >> <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 > >> _______________________________________________ > >> 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] > > _______________________________________________ > 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]
