There are quite a few other tools for protocol verification (ProVerif, Maude-NPA, etc.) and I haven't used all of them myself, but I think Tamarin is particular

There are quite a few other tools for protocol verification (ProVerif, Maude-NPA, etc.) and I haven't used all of them myself, but I think Tamarin is particularly easy to read and understand even when starting out. The rules are roughly written in terms of inputs to outputs along with some labels to refer to what happened, and the properties are essentially just plain first-order logic. (Disclaimer: I'm biased, I've worked with Tamarin more than other tools and also contributed some to its codebase.) Also I think part of the power in using Tamarin is that if it's having trouble proving something automatically, it's easy to jump in and try to prove it manually with a relatively straightforward graphical representation of the trace sets. That also helps you spot any potential interim properties you might need to prove as helper lemmas, etc. It's gotten some recent popularity for the work on TLS 1.3 as well [0], and with that an effort to improve the materials available for people to pick it up themselves [1, 2]. Some of the things we did to nudge Tamarin's heuristic in the right direction when autoproving the WireGuard model (documented in the .m4 file) are getting baked in to Tamarin soon. (For what it's worth, you don't actually have to deal with any Haskell unless you're planning on modifying the prover, the protocol models are in their own language.) [0] https://tls13tamarin.github.io/TLS13Tamarin/ https://tls13tamarin.github.io/TLS13Tamarin/ [1] https://github.com/tamarin-prover/teaching https://github.com/tamarin-prover/teaching [2] https://tamarin-prover.github.io/manual/book/001_introduction.html https://tamarin-prover.github.io/manual/book/001_introductio...