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