Download on the ProVerif page.
Changes since the previous release:
– Improved optimisation transforming mess facts into attacker facts when the
channel is a public term and not only a public name.
– Allow nested comments in the input file. All comments must be closed. ProVerif
will raise an error otherwise.
– Allow “let x = t in” construct inside the declarations of reduc and equation.
– Fixed bug in subsumption: removing attacker facts containing ground public
terms was not correct.
– Improved unification modulo to avoid stack overflow.
– Fixed a bug that would cause a type error when using a typeConverter function
and the “let x = t in” construct inside a “not” declaration.
– Fixed bug: make sure clauses coming from <-> or <=> in Horn clause front-ends
have distinct variables.
