Download ASLan++ specification and tutorial

D2.3 (update): ASLan++ specification and tutorial
--of str
Select the output format and it’s level of verbosity.
The default value is ’if’, and choices are :
ASLan Standard output format from the Avantssar project;
if
Standard output format from the Avispa project;
if+
Same as ’if’ but also shows the protocol specification
as it was understood;
if++
Same as ’if+’ but show things exactly as they were
analysed (i.e. after simplification);
ifShows a quick view of the attack trace, if any;
brief Shows an even more concise view of the attack trace and
analysis result.
--out
Write the attack to file.atk
--dir d
(string) Output directory to use with -out
--ns
Do not simplify the input file (complete trace).
--opt
Try to replace hashing by tokens. (slower or faster
depending on the protocol) (Default for IF).
--noopt
Do not try to replace hashing by tokens. (slower or
faster depending on the protocol) (Default for ASLan).
--verbose Print more output informations (same as ’--of if+’).
--noexec Do not analyse, only write the specification as it is.
--col n
Number of column in the output, default 80.
--bench
Benchmark output format (very concise).
--ASLan
Expect AVANTSSAR’s ASLan in input, use ASLan for output.
--if
Expect AVISPA’s IF as input; Not default anymore.
--lvl n
Level of protocol rebuilding (see explanation above).
--store
When an attack is found, store the current state in
a .state file.
--split
Create a directory with the spec’s name and fill it with
more than 300 sub state files, so that many different
instances of Cl-AtSe can analyse them in parallel.
--hc str Choses a strategy for Horn clauses. Default is btd+
btd
Backward strategy with depth-first recursivity;
blr
Backward strategy with breadth-first recursivity;
btd+
Backward TopDown plus heuristical choice of the fact to
descend into first.
--not_hc Extend tests for negtive constraints w.r.t Horn Clauses.
Debugging options :
--max n
--vv
--tab
--par
--heavy
--debug
(int) Forced activation of -lvl 0 if this number of
steps is reached (default 80).
Print even more output and term informations (debug).
Write the correspondence table (debug).
Write the parser output (debug).
Extend the search for unforgeable atoms.
Write debuging informations for Read.ml (debug).
FP7-ICT-2007-1
Project No. 216471
187/190