Toolchains

There are multiple tools that use Tamarin as a backend, notably SAPIC which translates Applied Pi Calculus specifications to Tamarin, and another tool translating Alice&Bob-specifications to Tamarin.

Alice&Bob input

There exists a tool that translates Alice&Bob-specifications to Tamarin: http://www.infsec.ethz.ch/research/software/anb.html