Download

 

Development version : GitHub repository

The program is written in Ocaml. It is recommended to have Ocaml 4.x to compile this program. The current version is still a beta version, hence it is not considered as completely stable. Bugs may occur so do not hesitate to send email to cheval@lsv.ens-cachan.fr or v.f.p.cheval@cs.bham.ac.uk for bug report.

Upcoming features :

  • Optimisation of the strategy on constraint systems by factorising the matrices on the leaves
  • Algorithm that determines the coefficients of the length functions of the cryptographic primitives such that the two given processes are equivalent w.r.t. length.
  • Optimization of the algorithm by allowing matching trace heuristic
  • Completion of the documentation
  • Implementation of a module for distributed computation
  • Allowing input with sets of constraint systems and symbolic equivalence between sets of constraint systems.

Changelog :

0.4beta

  • Correction of a bug in the parser with the tuples.
  • Addition of a module for statistic on the matrices generated by the algorithm
  • New strategies for the algorithm available (see the different new options)
  • An log option have been added that stores the tree of matrices. It should help following the generation of matrices by the algorithm.
  • The help menu have been changed to match all the new options
  • Addition of new examples.

0.3.2.beta

  • Fixing an issue with the Makefile which went into an infinite loop on Linux.
  • Cleaning of the archive of some MACOX files

0.3.1.beta

  • Fix of a stack overflow problem.
  • The parser now handle properly the declared constants
  • Addition of three new examples: Unlinkability of the Passive Authentication protocol of the electronic passport (without considering length, the existing attack when considering the length of messages and lastly the fix)

0.3beta:

  • Major modifications in the source code including the interfaces
  • Optimization of the algorithm. Some examples that took 80 seconds in 0.2alpha to be executed are now executed in less than a second (see the examples corresponding to the private authentication protocol in the archive).
  • Several fixes of bugs
  • First draft of a documentation
  • Improvement of the user interface

0.2alpha:

  • new feature : Trace equivalence w.r.t. length
  • new help display
  • fix few bugs