On Fri, May 31, 2024 at 7:55 AM Cas Cremers <cas.crem...@gmail.com> wrote:
> 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. > FWIW, this was clear to me from the report. As Usama indicates the summary did say "Tamarin analysis" but I took this to mean "symbolic analysis". -Ekr > 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 >
_______________________________________________ TLS mailing list -- tls@ietf.org To unsubscribe send an email to tls-le...@ietf.org
