Re: [TLS] Proposal: a TLS formal analysis triage panel

[Muhammad Usama Sardar <[e-mail]>]

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.