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

Changes in Version 2.0

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

Changes in Version 1.1

• 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

Changes in Version 1.0

• 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

Initial version was 0.1