LySatool Version 2.01

Changes in Version 2.01

This version is updated with minor bug-fixes as detailed below.
HTML output: empty sets in annotations are now printed correctly
HTML output: minor layout issues fixed
LaTeX output: empty sets in annotations are now printed correctly
LaTeX output: no longer use \mathbb i.e. it runs on standard LaTeX without including any packages.
Numbers in indexes can only be non negative

The name of this software has officially changed to "LySatool" from the cumbersome "LySa - Analysis of origin and destination authentication"
The main technical novelty is the addition of a meta-level analysis, which caters for analysis of infinite scenarios. The analysis now works directly on indexing meta-level constructs. Indexing constructs now range over infinite sets rather than being a syntactic shorthand for finitely many processes.
The meta-level of version 2.0 has a new syntax, which is not compatible with the syntax of version 1.x! (Changes are rather minor, though.)
Efficiency: non-terminals used in tree grammar and variables used in input can be merged to give smaller (but equivalent) results analysis. Computing smaller solutions is more efficient.
Efficiency: ALFP formula now contain an explicitly reachability predicate, RC, which makes the computation of the solution faster.
The constraint generation now takes parameters. The analysis can e.g. be carried out with/without the attacker, with/without optimisations for efficiency.
HTML documents can be automatically generated to show the LySa process, which is analysed, along with its analysis results.
LaTeX formated version of processes can be automatically generated. Formatting uses the LaTeX package in "io/lysa.sty".
An Emacs mode is now part of the distribution in "io/lysa-mode.el".

A parser of (Meta) LySa processes from ASCII text has been added in the directory io/
Example protocols (written in ASCII text format) has been added in the directory protocols/ (hopefully more will come)
The directory experiments1/ is considered deprecated and has been removed from the distribution
Lysa2LLysa.l2llProc now translates sequences of indices into unique strings (which before was a problem e.g. when unfolding to more than 9 instances)
Constraint generation in analysis1.sml now produces a correct ALFP formula when an encryption is empty
Constraint generation in analysis1.sml now produces a correct ALFP formula when the list in ORIG or DEST is empty
Emacs Time-stamps have been added to all source files. Dates are as of now - though many files have not been modified since last release

Annotations with NONE are expanded to the set of all crypto-points by Lysa2LLysa.l2llProc.
Using ORIG in encryption or DEST in decryption will now cause an exception to be raised by Lysa2LLysa.l2llProc.
Indices may now also be the empty string (in case you feel that it makes sense)
Annotation corrected in example.sml
Minor corrections in documentation