New release: ProVerif 2.01

Community
1

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