Vincent Cheval and I are happy to announce a new release of ProVerif, version 2.01, available at http://proverif.inria.fr
It is also available via opam (see installation instructions in Section 1.4 of the manual http://proverif.inria.fr/manual.pdf )
This release includes major extensions implemented by Vincent:
lemmas, proofs by induction, natural numbers. See detailed
list of changes below and Sections 4.1.3, 6.1, and 6.2 of the manual.
Stay at home and enjoy…
Changes in this release:
- The interactive simulator can now simulate the semantics of biprocesses.
- Addition of lemmas and axioms (see Section 6.2 of the manual).
- Fixed bug in the verification that injective events are correctly set in the
- Display of a summary of the results at the end of the computation.
- Removal of restrictions on events when proving injectivity: an injective
event can now occur in several processes in parallel and not necessarily
in the scope of a replication.
- Improved verification of correspondence queries by better handling
disequalities in queries.
- Improved verification of nested queries.
- Improved display of variables and names
- Improved elimination of redundant hypotheses (significant speedup on some
- Introduction of natural numbers:
- The builtin type for natural numbers is ‘nat’.
- Allow 0, 1, 2 … to be used in terms.
- Allow the operators + and - but only between a variable and a number or
between two numbers. It cannot be used to sum two variables.
- Allow 5 built-in predicates: is_nat, <, >, <=, >=. The predicate is_nat(t)
is true iff t is a natural number. The predicate t1 < t2 is true iff t1
and t2 are natural numbers and if t1 is strictly less than t2. Similar
for the remaining predicates.
- These predicates can be used in ‘if-then-else’ processes, in
‘let-suchthat-in-else’ processes and also in queries, lemmas, and axioms.
- These predicates can also be used for observational equivalence proofs but
only with ‘if-then-else’ processes.
- Name and constructor function symbols cannot have ‘nat’ as resulting type.
Destructor function symbols can have ‘nat’ as resulting type. Finally, all
functions can have arguments of type ‘nat’.
- Option [induction] to prove a query by induction.
- Option [proveAll] to prove all queries of a group. Especially useful for
proofs by mutual induction.
- Added options hypothesis, conclusion, ignoreOnce and inductionOn to
- Changed the display of operator <> into its mathematical representation.
- Allow to add the option [precise] after an input, let suchthat and
get. This improves the precision of ProVerif. Also allow to define
‘set preciseActions = true’ in input file. Defining ‘preciseActions’
to true is equivalent to adding [precise] to every input, let
suchthat and get.
- Bug fix: added clauses for phase change to the clauses used for proving
- Bug fix: by default, deactivate the optimization of mess(c,M) into
attacker(M) when we try to prove attacker(.). The setting
privateCommOnPublicFreeNames = false recovers the previous behavior,
with the semantics that all communications on public free names go
through the adversary.
- Bug fix: in elimination of redundant clauses, do not perform resolution
on predicates that we are trying to prove in a query or to apply a lemma.
- Fixed bug in the display of names in “secret” queries and in “public_vars”.
- Fixed bug triggered by HTML directories containing strings \0, …, \9.