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(\langle x,y \rangle, 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:
  • revealing-signing: This theory models a message-revealing signature scheme.
    It defines the function symbols $revealSign/2$, $revealVerify/3$, $getMessage/1$, $pk/1$, and $true$, which are related by the equations: and
  • 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:
  • diffie-hellman: This theory models Diffie-Hellman groups.
    It defines the function symbols $inv/1$, $1/0$, and the symbols ^ and $ \ast $. We use $g $^$ a$ to denote exponentiation in the group and $ \ast $, $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 \ast z); x$^$1 = x; x \ast y = y \ast x; (x \ast y) \ast z = x \ast (y \ast z); x \ast 1 = x; x \ast inv(x) = 1.$
  • xor: This theory models the exclusive-or operation.
    It adds the function symbols $ \oplus /2 $(also written as $XOR/2$) and $zero/0$. $\oplus$ is associative and commutative and satisfies the cancellation equations:
    $x \oplus y = y \oplus x; (x \oplus y) \oplus z = x \oplus (y \oplus z); x \oplus zero = x; x \oplus x = zero$
  • multiset: This theory introduces the associative-commutative operator $+$ which is usually used to model multisets.

Reserved function symbol names

Due to their use in built-in message theories, the following function names cannot be user-defined: $mun, one, exp, mult, inv, pmult, em.$
If a theory contains any of these as user-defined function symbol the parser will reject the file, stating which reserved name was redeclared.