New release: ProVerif 2.04

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
It is also available via opam (see installation instructions in Section 1.4 of the manual )

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.


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