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
maintenance by...someone.
Are you expecting any major changes in TLS 1.3? If not, then I think the
baseline formal model will not change a lot. So probably there is not
much maintenance required. I think it is just a one-time effort to
create well-understood and well-reviewed formal artifacts as a baseline,
and then most extensions (for which formal analysis is signaled by the
panel) can use this baseline.
Also, TLS WG can work together with UFMRG to achieve this.
For the triage panel, I do think the preliminary triage is key: we'd
ask a group of experts /if/ formal analysis (new or updated) is
warranted /at all/, and if warranted, of what kind, what scope, if it
needs novel modeling work, if it can build on existing work, or even
if pen and paper analysis would suffice. I do not think there are any
prerequisites to standing such a triage panel up.
Agree. However, the baseline for each "kind" (e.g., one for symbolic and
one for computational and within symbolic, one for ProVerif and one for
Tamarin) will still be helpful to avoid repetitive work.
_______________________________________________
TLS mailing list
TLS@ietf.org
https://www.ietf.org/mailman/listinfo/tls
