Cryptographic Messages

Tamarin analyzes protocols with respect to a symbolic model of cryptography. This means cryptographic messages are modeled as terms rather than bit strings.

The properties of the employed cryptographic algorithms are modeled by equations. More concretely, a cryptographic message is either a constant c or a message f(m1,...,mn) corresponding to the application of the n-ary function symbol f to n cryptographic messages m1, ..., mn. When specifying equations, we also allow for variables in addition to constants.

Constants

We distinguish between two types of constants:

Function Symbols

Tamarin supports a fixed set of built-in function symbols and additional user-defined function symbols. The only function symbols available in every Tamarin file are for pairing and projection. The binary function symbol pair models the pair of two messages and the function symbols fst and snd model the projections of the first and second argument. The properties of projection are captured by the following equations:

fst(pair(x,y)) = x
snd(pair(x,y)) = y

Tamarin also supports <x,y> as syntactic sugar for pair(x,y) and <x1,x2,...,xn-1,xn> as syntactic sugar for <x1,<x2,..,<xn-1,xn>...>.

Additional built-in function symbols can be activated by including one of the following message theories: hashing, asymmetric-encryption, signing, symmetric-encryption, diffie-hellman, bilinear-pairing, and multiset.

To activate message theories t1, ..., tn, include the line builtins: t1, ..., tn in your file. The definitions of the built-in message theories are given in Section Built-in message theories.

To define function symbols f1, ..., fn with arity a1,...,an include the following line in your file:

functions: f1/a1, ..., fn/an

Tamarin also supports private function symbols. In contrast to regular function symbols, Tamarin assumes that private function symbols cannot be applied by the adversary. Private functions can be used to model functions that implicitly use some secret that is shared between all (honest) users. To make a function private, simply add the attribute [private] after the function declaration. For example, the line

functions: f/3, g/2 [private], h/1

defines the private function g and the public functions f and h. We will describe in the next section how you can define equations that formalize properties of functions.

Equational theories

Equational theories can be used to model properties of functions, e.g., that symmetric decryption is the inverse of symmetric encryption whenever both use the same key. The syntax for adding equations to the context is:

equations: lhs1 = rhs1, ..., lhsn = rhsn

Both lhs and rhs can contain variables, but all variables on the right hand side must also appear on the left hand side. The symbolic proof search used by Tamarin supports a certain class of user-defined equations, namely convergent equational theories that have the finite variant property (Comon-Lundh and Delaune 2005). Note that Tamarin does not check whether the given equations belong to this class, so writing equations outside this class can cause non-termination or incorrect results without any warning.

Also note that Tamarin's reasoning is particularly efficient when considering only subterm-convergent equations, i.e., if the right-hand-side is either a ground term (i.e., it does not contain any variables) or a proper subterm of the left-hand-side. These equations are thus preferred if they are sufficient to model the required properties. However, for example the equations modeled by the built-in message theories diffie-hellman, bilinear-pairing, and multiset do not belong to this restricted class since they include for example associativity and commutativity. All other built-in message theories can be equivalently defined by using functions: ... and equations: ... and we will see some examples of allowed equations in the next section.

Built-in message theories

In the following, we write f/n to denote that the function symbol f is n-ary.

hashing:

This theory models a hash function. It defines the function symbol h/1 and no equations.

asymmetric-encryption:

This theory models a public key encryption scheme. It defines the function symbols aenc/2, adec/2, and pk/1, which are related by the equation adec(aenc(m, pk(sk)), sk) = m. Note that as described in Syntax Description, aenc{x,y}pkB is syntactic sugar for aenc(<x,y>, pkB).

signing:

This theory models a signature scheme. It defines the function symbols sign/2, verify/3, pk/1, and true, which are related by the equation verify(sign(m,sk),m,pk(sk)) = true.

symmetric-encryption:

This theory models a symmetric encryption scheme. It defines the function symbols senc/2 and sdec/2, which are related by the equation sdec(senc(m,k),k) = m.

diffie-hellman:

This theory models Diffie-Hellman groups. It defines the function symbols inv/1, 1/0, and the symbols ^ and *. We use g ^ a to denote exponentiation in the group and *, inv and 1 to model the (multiplicative) abelian group of exponents (the integers modulo the group order). The set of defined equations is:

(x^y)^z  = x^(y*z)
x^1      = x
x*y      = y*x
x*1      = x
x*inv(x) = 1
bilinear-pairing:

This theory models bilinear groups. It extends the diffie-hellman theory with the function symbols pmult/2 and em/2. Here, pmult(x,p) denotes the multiplication of the point p by the scalar x and em(p,q) denotes the application of the bilinear map to the points p and q. The additional equations are:

pmult(x,(pmult(y,p)) = pmult(x*y,p)
pmult(1,p)           = p
em(p,q)              = em(q,p)
em(pmult(x,p),q)     = pmult(x,em(q,p))
multiset:

This theory introduces the associative-commutative operator + which is usually used to model multisets.

Comon-Lundh, Hubert, and Stéphanie Delaune. 2005. “The Finite Variant Property: How to Get Rid of Some Algebraic Properties.” In RTA, 294–307.