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

Bertie is such a reference implementation of TLS in the hacspec language.
https://github.com/cryspen/bertie
When combined with the libcrux high assurance cryptographic library, I
understand it is efficient.

A Proverif backend for hax/hacspec (https://hacspec.org/) is under construction.
It may be possible to make a Tamarin backend in a similar way. This
would provide the requested interoperability.

Bas

On Wed, Mar 20, 2024 at 6:15 PM Marc Petit-Huguenin
<marc@petit-huguenin.org> wrote:
>
> [+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 interoperability between the models used by different tools, so a model can be translated between tools.
>
> >> 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
>
> --
> Marc Petit-Huguenin
> Email: marc@petit-huguenin.org
> Blog: https://marc.petit-huguenin.org
> Profile: https://www.linkedin.com/in/petithug
>
> --
> Ufmrg mailing list
> Ufmrg@irtf.org
> https://mailman.irtf.org/mailman/listinfo/ufmrg