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