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

Reply via email to