%% Hello, this is the WebCassis services provider, nice to meet you.
%% Running : /var/lib/tomcat6/webapps/WebCassis/BIN/cl-atse --help [limit 10s]
European Project AVANTSSAR's
&European Project AVISPA's
___ __ _____ __ ___
| | | | | | |
| | --- |--| | -- |--
|___ |___ | | | __| |___
Version 2.5-19 (2012-octobre-11)
Usage : cl-atse [options] [-f file] [files]
[files] Name of the IF/ASLANv1 files to process (default is standard input)
Note : HLPSL files allowed if hlpsl2if is available. Multiple files allowed.
-f file Name of a specification file to process. Same as [files].
-u Do not take term types into account.
-o Write the attack to file.atk
-v Print more output informations, in the avispa O.F. (same as '--of if+').
Expert/Long options :
--nb n (int) Maximum number of iterations per ASLan transition rule. (default is 3 for IF, 1 for ASLAN).
WARNING: This option must be manually increased if no attack is found. No heuristic for a max. bound.
With --lvl 2 : this corresponds to nb. of role iterations, or loops at ASlan++ level;
With --lvl 0 : this is the nb. of times each transition can be run in any attack trace.
--free Uses a free pairing symbol (default for the typed model).
--assoc Uses an associative pairing symbol (default for the untyped model).
--typed Use term types as defined in the spec. (default).
--untyped Do not take term types into account.
--short Perform breath-first search (minimal attack).
--of str Select the output format and it's level of verbosity. Default is 'if', choices are :
aslan Standard output format from the Avantssar project, very concise;
if Standard output format from the Avispa project, with step details;
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 (after simpl.);
if- Shows a quick view of the attack trace, if one is found;
brief Shows an even more concise view of the attack trace and analysis result.
--out (string) Write the attack to some specific file
--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 dep. on protocol) (Default for IF).
--noopt Do not try to replace hashing by tokens. (slower or faster dep. on protocol) (Default for ASLAN).
--verbose Print more output informations, in the avispa O.F. (same as '--of if+').
--noexec Do not Analyse, i.e. only write the specification the way it was understood.
--col n (int) Number of column in the output (default 80, disabled with -1).
--bench Benchmark output format (very concise).
--aslan Expect AVANTSSAR's ASLAN in input and tries to follow ASLAN in output.
--if Expect AVISPA's IF as input; Not default anymore since AVANTSSAR.
--lvl n (int) Level of protocol rebuilding: 0 for none; 2 for full processing (default).
--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 >100 sub state files,
so that many different instances of cl-atse can analyse them in parallel.
--hc str Choses a strategy for Horn clauses deductions. Default is btd+, choices are :
btd Backward TopDown strategy, i.e. backward strategy with depth-first recursivity;
blr Backward LeftRight strategy, i.e. 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.
--sets Follows the Aslan semantic by treating all facts as objets in a set (not multiset).
By default, all facts (and contains) are in multisets, i.e. without any rule 'fact.fact = fact'.
Debugging options :
--max n (int) Forced activation of -lvl 0 if this number of steps is reached (default 80).
--vv Print even more output and term informations (debug). Same as '--of if++'.
--tab Write the correspondence table (debug).
--par Write the parser output (debug).
--heavy Extend the search for unforgeable atoms during simplification.
--debug Write debuging informations for Read.ml (debug).
--split Use the --split option on hlpsl2if for hlpsl input file.
--states Shows all internal system states of the analysis.
--trace Use -trace "Short trace" to follow one particular trace.
--reverse Inverse the order of protocol steps in the read_aslan module.
--unforgeable Computes a list of unforgeable terms before analysis.
Miscellaneous options :
--version Print the version number.
--licence Print the CL-Atse's disclaimer (licence).
-help Display this list of options
--help Display this list of options
%% Job terminated successfully.