New release ProVerif 2.03

Download on the ProVerif page.

Changes since the previous release:

– Events that occur in the conclusion of a lemma and also as an injective event
in the main query are not ignored anymore when applying the lemma.
– Replace attacker(fail-any,x) or attacker(x,fail-any) with bad in the
conclusion of clauses. This allows more clauses to be subsumed.
– Attacker facts containing ground public terms are now directly removed from
the hypotheses of the Horn clause.
– Improved subsumption: attacker facts containing ground public terms are not
being matched but directly removed.
– Added declaration “select” to encourage ProVerif to resolve upon certain
facts, and “noselect” as a synonym to “nounif”.
– Added the setting “simpEqAll” that controls whether ProVerif checks that all
terms in Horn clauses are in normal form or not.
– Added the setting “verboseDestructors” to display information about
destructors in the terminal.
– Removing unnecessary variants of rewrite rules for destructors in presence
of an equational theory. Speeds up the generation of clauses and produces
significantly fewer Horn clauses on some examples.
– Removed unnecessary Horn clauses that contained the term “caught-fail”.
– Extended the “proba” declaration and added the “letproba” declaration
for compatibility with CryptoVerif; they are just ignored by ProVerif.
– Fixed bug that could cause an internal error (assertion failure when
reconstructing the trace of a biprocess).
– Fixed bug that could cause an internal error instead of a normal error
(variable x not defined at restriction n in a query containing new n[x = …]);
reported by Nicola Vitacolonna.
– Fixed bug that could cause a stack overflow when applying lemmas.
– Fixed bug that prevented declaring nounif of the form *i + 1.
– Fixed bug: ordering constraints were sometimes not taken into account
even though the query needed them.
– Fixed bug in attack reconstruction, in else case of let … suchthat.
– Fixed bug that could cause an internal error due to duplicate variables
in processes obtained by simplification (reported by Alexandre Debant).
– Fixed bug that could cause an internal error in copy_binder (reported
by Jose Moreira).
– Fixed bug in simplification of disequalities.

Comments are closed.