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 <m...@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: m...@petit-huguenin.org > Blog: https://marc.petit-huguenin.org > Profile: https://www.linkedin.com/in/petithug > > -- > Ufmrg mailing list > uf...@irtf.org > https://mailman.irtf.org/mailman/listinfo/ufmrg _______________________________________________ TLS mailing list TLS@ietf.org https://www.ietf.org/mailman/listinfo/tls
