Rust Implementation Request for Comments

[Kevin Milner]

Hi all,

The last while I have been working on (with the help of LLMs) a rust port of tamarin. It is obviously not ready for any adoption but I'd like to submit it for anyone interested to evaluate. It is stable but does not currently implement accountability or diff equivalence modes. However, almost every other feature should work correctly.

Why try it: it is much much faster and lighter than the Haskell code, even after the Haskell optimisations I've implemented over the last couple months, and generates identical proofs across every applicable example in the tamarin repository. You can for example try autoproving or using the interface in the rust and then validate the proof with the Haskell version. If you find a mismatch please send me the file so I can investigate!

You can find the code and build instructions here: https://github.com/kmilner/tamarin-prover/tree/rust-port/rust

Some performance numbers for comparison are included in the README at that link. In general it is at least ~4x faster (ranging from about 2-37x, yes that's 37x, depending on the theory and core count) and typically uses about a quarter as much memory (ranging from about 2-26x less, and again 26x is not a typo, depending on the theory and core count). It generally scales better across multiple cores as well.

This is a work in progress, and absolutely nowhere close to supplanting the Haskell, not the least because far far too much of this code was written and reviewed by LLMs (albeit with a very extensive grounding framework against the exact proof system of the Haskell at each step). But I believe it's now in a state where it is close enough that some folks working on larger theories might find it useful to try out, on the basis that it will be faster in many cases to prove on the rust and validate the proof with the Haskell than it is to prove on the Haskell directly, or to (for example) use the rust locally to try their tactics etc and then hand off to a server with much more memory to generate the real proofs.

This comes with two minor caveats:
- Tamarin has two outstanding issues preventing proofs from being revalidated in certain limited cases, https://github.com/tamarin-prover/tamarin-prover/pull/872 and https://github.com/tamarin-prover/tamarin-prover/pull/882, so nothing can be done in those cases at the moment. However the proofs for affected files are identical in rust to what they would be if those fixes were in place in Haskell.

- Some variable numberings are slightly different, because of the way queries are submitted to Maude. This *should* never affect a proof, the only time you should ever see it is if you look at the full proof system (e.g. in interactive mode) and compare it between the rust and the Haskell, you will sometimes find that variables are numbered slightly differently.

Do let me know your thoughts and suggestions! This started as a small hobby project, and the process of getting it working and grounding the development against real tamarin helped me find a wide variety of optimisations and minor bugs in real tamarin, which I think of as arguably the main output of the project. But the result did end up being much faster and lighter as well, so it might be useful on its own to people. I'll look at moving it out into its own repository with extensive notes in the future if it is.

Cheers,

Kevin

[Kevin Milner]

Hello again!

Thanks so much for the interest so far from everyone who has emailed me. Just some quick updates:

- I've split this out now into a separate repository, https://github.com/kmilner/tamarin-rs so it is more obvious where it lives and how to build it etc.

- Accountability is now implemented! And we fixed a latent bug in the Haskell, which is exactly the sort of thing I hoped would come out of this project, so I'm quite happy with that. 

- More usefully, I've added a `prove_and_reverify.sh` script, which generates the proof using the Rust implementation and then checks it for you with tamarin-prover. In many/most cases, this is faster than generating the proof with the Haskell implementation directly, and more importantly means you do not have to trust the Rust implementation at all (and, again, you really should not!) [note 0]

Whether prove + reverify is actually faster for you will depend a lot on your theory. Some scattershot examples that seem to be towards the extremes: CCITT_X509_3.spthy is 91/93/96% faster to proof + reverify at 1/4/16 cores (for context, at 16 cores that's 140s to proof in Tamarin Haskell versus 5.7s combined to prove in Rust and then reverify in Haskell), but in contrast stateverif_left_right.spthy is ~11% faster at 1 core but slower by about ~30% at 16 (16s Haskell, vs 20s prove + reverify) [note 1]. Specifically, verification cost scales with the end proof size, while --prove cost scales with the search space, so this is very fast on things like exists-trace lemmas or finding attack traces but will be much less helpful in proofs that have a lot of cases across different levels.

Again, I want to stress, you should not trust this project on it's own, you should always reverify your final proofs by loading them in the real canonical tamarin-prover instead of the knockoff! But with that said, the Rust implementation does currently produce exactly equivalent proofs across all applicable example files I have to test against (419 of them)[note 0 again], so you may find it useful for 'prototyping' proofs, or for working on smaller machines, and that would be a great way to test it. In the (hopefully small) chance you do find a mismatch that doesn't reverify, that would be hugely helpful for me, please report it on github or email me.

I've also tried my best to clarify the licensing situation to the best of my ability to divine, which is to say it is currently a mix of MIT and GPL 3.0 (and therefore very firmly GPL 3.0 for any and all practical purposes). 

Hopefully this is useful, and please do continue getting in touch if you have any questions/suggestions. I'm not currently building binaries for this so you will have to have rust to build it yourself; if having prebuilt binaries would make a big difference for your usecase get in touch and I can prioritise getting some github workflows set up.

Cheers,
Kevin

[note 0] Within the repo I have a patch for the issues mentioned in the first email about reverification, and there's a little setup script for building a patched version of Tamarin if you want with `./setup.sh testing`. That said both of those issues with reverification only apply in certain limited scenarios, so you may or may not need it.

[note 1] Note this is the performance after several recent optimisations to the Haskell, so if you're comparing against the release version then prove+reverify is much more likely to be generally faster.