tamarin expressiveness and its usefulness stems, in part, from the wide range of operators that it supports. tamarin has built-in support for common operators and users may additionally define their own operators. We describe the built-in operators in this section. By default, tamarin always includes the definitions of several basic operators for constructing and decomposing tuples of terms. Syntactic built-ins constitute shorthands: they are simply replaced by predefined functions and equational theories. Hence the user could alternatively just include this replacement directly in their input file, or arbitrarily rename the functions. This is intended to model a perfect one-way and collision resistant hash function, for which there is no way to recover the pre-image or find a collision.