The Tamarin Prover, a protocol analyzer tool for security protocols with cryptographic primitives, accepts protocols including cryptographic primitives such as encryption, signatures, and hash functions. More advanced primitives are also possible, such as Diffie–Hellman exponentiation, bilinear pairings, and multisets, but using a more elaborate implementation makes primitive combination more difficult. A more user-definable syntax for cryptographic primitives is also possible, but it uses subterm convergent equational theories, which can encode some primitives such as cancellation of encryption and decryption, but cannot encode other primitives such as exclusive-or, blind signatures, or trapdoor commitment. This paper provides new reasoning capabilities for the Tamarin Prover.

This paper represents a step forward in expanding the user-definable cryptographic primitives allowed by the Tamarin Prover by relying on equational theories satisfying the finite variant property, called finite variant theories. This class of theories can encode exclusive-or, blind signatures, or trapdoor commitment. However, the results in the paper are preliminary because not all of the finite variant theories are accepted. Those accepted are only a subset useful for encoding blind signatures or trapdoor commitment, but not exclusive-or.

Dreier et al. describe how both intruder reasoning and the normal dependency graphs of the Tamarin Prover are extended to the subclass of finite variant theories. Intruder reasoning uses K-up and K-down inference rules, whereas the normal dependency graphs use term simplification properties. The paper also provides several case studies, that is, protocols using cryptographic primitives encoded into the subclass of finite variant theories. It shows how several security properties, including secrecy, authentication, and indistinguishability, can be verified for those case studies.

This paper is useful to understand how the Tamarin Prover works and to understand how different cryptographic primitives are encoded into equational theories.