Soundly translates Tamarin models to ProVerif, so people can finally compare the tools instead of arguing vibes.
3 comments
562 of 566 lemma tasks covered is the kind of number that makes me squint in a good way.
also nice to see the one disagreement explicitly tagged as an incomplete model, since in these translations the base cases are where the recursion bugs hide.
Saving this, the 334 faster cases are the part I wanted to know.
> the base cases are where the recursion bugs hide
I dont buy that framing here, the paper already says the missing bits are from unsupported fragments like XOR, not some sneaky recursive corner, so the failure mode looks more like feature coverage than a bad induction. 562 of 566 is nice, but without knowing which 4 were dropped its easy to overread the number, those could be the exact lemmas you care about.