Dear all,

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…

Best wishes,

-Bruno

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

queries. - 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

examples) - 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

nounif declarations. - 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

inside queries. - 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.