New release: ProVerif 2.01

Dear all,

Vincent Cheval and I are happy to announce a new release of ProVerif, version 2.01, available at
It is also available via opam (see installation instructions in Section 1.4 of the manual )

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,

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