README.md

ProVerif 2.00 modifications

Notes

• As ProVerif modification itself was not the core part of the project - we only modified ProVerif to resolve issues as we went on, we did not conduct any systematic review of the entirety of ProVerif's source code. Thus we make no claims that these modifications are completely safe.

• However, we have taken care to ensure these modifications do not impact the original functionality of ProVerif, that is, if you invoke the modified ProVerif in a non-exporting mode, it should behave the same as the original version. Again, however, we cannot claim with full certainty this is the case - if you absolutely need the exact behaviour provided by the original version of ProVerif, we recommend you to use the original version directly.

• We also note that the modifications right now assume the encoding uses only bitstring type, but the modifications should be extendable to accomodate other combinations of types.

List

• Added missing equation export

• Disabled equation checking when output is TPTP or SPASS

• Added TPTP export module

  • Also added inequality declaration between constants/free variables in the module, documented in the same file

• Automatic abstract syntax tree modifications in export mode

  • Output tagging

  • Let binding flattening

  • Replace let binding with equality checks with predicate

  • Introduction of extra constants

  • Replace if with equality checks with predicate (implemented, but later dropped)

• Added a pretty printer for typed pi-calculus abstract syntax tree