Vincent Cheval and I are happy to announce a new release of ProVerif, version 2.04.
ProVerif is an automatic security protocol verifier that relies on the symbolic model of cryptography.
ProVerif is 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 )
Version 2.04 is mainly a bugfix release but it also contains a change that may require minor changes in your input files: nested comments are supported, so if you open a comment several times and close it once, this is now an error.
Changes:
- 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.
Enjoy!
Bruno