Hi Usama, I think there is some possible misunderstanding of the panel's comments from your side. The panel did not discuss using any tool over any other. If someone writes "a Tamarin-like" analysis then this doesn't necessarily mean Tamarin. I think the consensus on the panel was that a more in-depth security argument was definitely needed. Starting from existing analyses that already cover the interaction between the modes seems a plausible option.
Best, Cas On Fri, May 31, 2024 at 10:56 AM Muhammad Usama Sardar < muhammad_usama.sar...@tu-dresden.de> wrote: > Dear chairs, > > I asked before (in this thread) and having received no response, I would > reiterate to understand why it is not possible to do all communication with > the triage panel transparently on the mailing list. I think discussing > directly on the mailing list would give authors an opportunity to get > earlier comments and provide/ask for any possible clarification rather than > having to wait for one month. It will also give an opportunity to formal > analysis enthusiasts to understand the rationale. > > Also, I am curious why are the chairs even hiding which response comes > from whom in the panel? If the authors have some questions/clarifications > (which Russ actually has in this case), will the chairs again go > underground with the triage panel and then bring "anonymous" answers to > these questions. > On 30.05.24 20:26, Russ Housley wrote: > > > On May 20, 2024, at 6:04 PM, Deirdre Connolly <durumcrustu...@gmail.com> > <durumcrustu...@gmail.com> wrote: > > - support for a proper security analysis to shore up the security > arguments: for authentication properties, a Tamarin analysis may do > > Firstly, why Tamarin? Why not ProVerif? > > Secondly, what *exactly* do you mean by "may"? For instance, if the > Tamarin proof is provided, could it be that the chairs/panel then say: hey, > that's great; we would now like some computational analysis to be more > confident. > > I see much more need for analysis when it comes to the authentication > properties of the PSK (psk/cert combination), whereas the secrecy (assuming > authentication is a non-goal) is much more straightforward. > > > Who will perform this analysis? I asked a researcher to perform such an > analysis, and the response was that it is too simple to get a paper. Now > waht? > > Russ, if you absolutely find no one, I will be happy to work on it over > the weekends (so it will be slow). Also to clarify, I prefer to work with > ProVerif because in my initial experiments, ProVerif was always way faster > than Tamarin. > > For the authentication analysis, I think here a Tamarin-like analysis > might be useful for checking undesirable interactions; for example, could > anything go wrong if a single PSK is used both as a traditional PSK but > also as an external PSK? > > Here is why I would like to see at least name of the panelist who wrote > this. If it is Cas, it makes perfect sense to me. If it is someone else, I > would like to know why he would prefer to recommend Tamarin over ProVerif. > What exactly is missing in ProVerif that would make it unsuitable for this > analysis? Or is it some usability issue? > > Best Regards, > > Usama > _______________________________________________ > TLS mailing list -- tls@ietf.org > To unsubscribe send an email to tls-le...@ietf.org >
_______________________________________________ TLS mailing list -- tls@ietf.org To unsubscribe send an email to tls-le...@ietf.org
