3.1. MODELING PROTOCOLS 17
the type of x is inferred from M; users may also write let x : t = M in P else Q where t is the type of
M, ProVerif will produce an error if there is a type mismatch.)
Scope and binding.
Bracketing must be used to avoid ambiguities in the way processes are written down. For example,
the process ! P | Q might be interpreted as !(P | Q), or as (!P ) | Q. These processes are different.
To avoid too much bracketing, we adopt conventions about the precedence of process operators. The
binary parallel process P | Q binds most closely; followed by the binary processes if M then P else Q,
let x = M in P else Q; finally, unary processes bind least closely. It follows that ! P | Q is interpreted
as !(P | Q). Users should pay particular attention to ProVerif warning messages since these typically
arise from misunderstanding ProVerif’s binding conventions. For example, consider the process
new n : t ; out ( c , n ) | new n : t ; in ( c , x : t ) ; 0 | i f x = n then 0 | out ( c , n )
which produces the message “Warning: identifier n rebound.” Moreover, the process will never perform
the final out(c,n) because the process is bracketed as follows:
new n : t ; ( out ( c , n) | new n : t ; ( in ( c , x : t ) ; 0 | i f x = n then (0 | out ( c , n ) ) ) )
and hence the final output is guarded by a conditional which can never be satisfied. The authors
recommend the distinct naming of names and variables to avoid confusion. New users may like to
refer to the output produced by ProVerif to ensure that they have defined processes correctly (see also
Section 3.3). Another possible ambiguity arises because of the convention of omitting else 0 in the
if-then-else construct (and similarly for let-in-else): it is not clear which if the else applies to in the
expression:
i f M = M
′
then i f N = N
′
then P els e Q
In this instance, we adopt the convention that the else branch belongs to the closest if and hence the
statement should be interpreted as if M = M
′
then (if N = N
′
then P else Q). The convention is
similar for let-in-else.
Remarks about syntax
The restrictions on identifiers (Figure 3.2) for constructors/destructors h, names a, b, c, k, m, n, s, types
t, and variables x, y, z are completely relaxed. Formally, we do not distinguish between identifiers and
let identifiers range over an unlimited sequence of letters (a-z, A-Z), digits (0-9), underscores (
), single-
quotes (’), and accented letters from the ISO Latin 1 character set where the first character of the
identifier is a letter and the identifier is distinct from the reserved words. Note that identifiers are case
sensitive. Comments can be included in input files and are surrounded by (* and *). Nested comments
are supported.
Reserved words. The following is a list of keywords in the ProVerif language; accordingly, they cannot
be used as identifiers.
among, axiom, channel, choice, clauses, const, def, diff, do, elimtrue, else, equation, equiva-
lence, event, expand, fail, for, forall, foreach, free, fun, get, if, implementation, in, inj-event,
insert, lemma, let, letfun, letproba, new, noninterf, noselect, not, nounif, or, otherwise, out,
param, phase, pred, proba, process, proof, public vars, putbegin, query, reduc, restriction,
secret, select, set, suchthat, sync, table, then, type, weaksecret, yield.
ProVerif also has built-in types any type, bitstring , bool, nat, sid, time, constants true, false of type
bool, destructor is nat , predicates attacker, mess, subterm; although these identifiers can be reused
as identifiers, the authors strongly discourage this practice.