[+ufmrg]
On 3/18/24 9:30 AM, Muhammad Usama Sardar wrote:
> On 18.03.24 16:56, Deirdre Connolly wrote:
>> I do think a 'reference' Tamarin model would be useful.
> Why should it be a Tamarin model? Why not a ProVerif model?
Maybe it would be a good use of UFMRG resources to work on the interopera
On 18.03.24 16:56, Deirdre Connolly wrote:
I do think a 'reference' Tamarin model would be useful.
Why should it be a Tamarin model? Why not a ProVerif model?
It would of course only model part of TLS (1.3, for example) and only
through a particular symbolic model/tool. And would require
maint
I do think a 'reference' Tamarin model would be useful. It would of course
only model part of TLS (1.3, for example) and only through a particular
symbolic model/tool. And would require maintenance by...someone.
For the triage panel, I do think the preliminary triage is key: we'd ask a
group of ex
Hi Deirdre,
Just in case I miss the meeting (which is unfortunately after midnight
for me), I would like to mention that this is great idea and I would be
happy to contribute to this.
In our recent research on integrating attestation in Inria's ProVerif
artifacts [1] for TLS 1.3, we faced se
I'd be happy to help work on something like this, but it might make more
sense to come present at UFMRG.
One of the goals of the Research Group is to try and bring together experts
and IETFers.
Rather than adding formal process, having a low stakes way of engaging with
the formal methods communit
> it's unclear to me whether this review would be a hard requirement to
pass WGLC. Let's say a document makes it to that stage, and it is sent to
the triage panel, but the panel never produces a formal analysis of it.
(This could happen for example if the researchers don't find the extension
at han
Hi Deirdre,
Thanks for this, I think this is a great plan. From the perspective of
standards work, more formal analysis is always better, and this seems like
a great way to motivate such work.
That said, it's unclear to me whether this review would be a hard
requirement to pass WGLC. Let's say a
