Tamarin (<->? Lean) / Security Protocol Verification

Stream: Program verification

[Julian Berman]

Has anyone here heard of Tamarin? In an unrelated conversation with a friend I just was linked https://tamarin-prover.com/book/ which is a pre-release book on using it to verify security protocols. I have not even glanced at it yet, but perhaps it's interesting to think about for this audience.

[Shreyas Srinivas]

Tamarin is a state machine based theorem proved

[Shreyas Srinivas]

One or more authors works at my institute. It is written in Haskell

[Shreyas Srinivas]

I actually wonder how it would be built if it were written in lean. Theoretically it should be possible

[Henrik Böving]

Julian Berman said:

Has anyone here heard of Tamarin? In an unrelated conversation with a friend I just was linked https://tamarin-prover.com/book/ which is a pre-release book on using it to verify security protocols. I have not even glanced at it yet, but perhaps it's interesting to think about for this audience.

Tamarin is pretty good, it's rather Isabelle/HOL than Lean inspired though. It's been used for some cool real world stuff like verifying (post quantum extensions of) the IKEv2 key exchange protocol by people that I used to work with: https://www.mnm-team.org/pub/Publikationen/gggh21b/PDF-Version/gggh21b.pdf. I think it'd be pretty cool if we had something like Tamarin in Lean.

[Shreyas Srinivas]

Tamarin is written in Haskell afaik

[Shreyas Srinivas]

And it has been developed over almost a decade at this point?

[Shreyas Srinivas]

I wonder how feasible it would be to develop the relevant parts in lean.

[Henrik Böving]

Shreyas Srinivas said:

Tamarin is written in Haskell afaik

yes but it is very obviously of isabelle descent in spirit

[Shreyas Srinivas]

I don’t see how. It encodes cryptographic protocol state machines as some sort of an equational theory

[Henrik Böving]

It is an obvious syntactic copy of Isabelle in parts, its files have .thy as their ending and they have literal ports of Isabelle files in their repository

[Shreyas Srinivas]

I just informed Cas Cremers about this channel and discussion. He might respond to the questions here. So @Julian Berman and @Henrik Böving : if you have some more questions, we could collect them in this thread.

[Julian Berman]

(I'm at the extremely early stage of "oh this looks interesting I'll play with it at some point", so no intelligent questions to ask of them quite yet!)

[Henrik Böving]

Similarly for me, my main connection point with Tamarin was the 4 sheets of A1 paper at the wall in our office that showed a protocol level exploit in the early IKEv2 PQC spec proposals.

[Shreyas Srinivas]

I asked Cas about implementing tamarin into lean

[Shreyas Srinivas]

He said they tried something on a very early stage (“sub part of a predecessor”) and ran into some issues

[Henrik Böving]

Well it would be great if they could point out these issues^^

[Shreyas Srinivas]

Looking at the timeline of Tamarin's development and the phrasing, I can't imagine they used lean4. Further lean has come a long way since then

[Bas Spitters]

As a first step, one may want to implement a Dolev-Yao model. In the style of DY* https://reprosec.org/dystar/. Years ago there were even discussions on making a lean backend for F*.
There is also early work by Larry Paulson formalizing DY in Isabelle.

[Shreyas Srinivas]

Whether we implement a subset of Tamarin or Dolev Yao, we need to in-house some of the tricks we used for equational theories into lean itself

[Shreyas Srinivas]

lean-egg is a nice tool in this direction (guided rewriting chains).

[fabricandink]

I am also interested. I spent some effort on a Rust+Egg implementation of Verifpal some time ago which is also meant for protocol verification. (Not sure what people think of it but I found the syntax easier to read. I ran into soundness issues with my rule set and gave up. I have some ideas on how to resolve them but didn't get to it yet.) Looking at the upcoming grind tactic, I wonder if it directly or its infrastructure could help since it seems to be an egraph framework as well.

[Wrenna Robson]

I am at HACS this next two days and in fact am looking at a whiteboard with "Tamarin" written on it right now.

[Wrenna Robson]

It would be good to make closer links between the high-assurance cryptography community and the Lean community, though I know we already have a few people in both worlds.

[Bas Spitters]

Cas Cremers mentioned over coffee that they have done experience in this direction, but that he has not had to time to react to this thread. In short, I understand there are some known, but unpublished, issues with embedding Tamarin into proof assistants. You could consider reaching out to Cas or David Basin by email, but both are extremely busy...