----------------------------------------------------------- European Project AVANTSSAR and AVISPA 's ___ __ _____ __ ___ | | | | | | | | | --- |--| | -- |-- |___ |___ | | | __| |___ Constraint Logic-based Model-checking of Security Protocols ----------------------------------------------------------- Author ......: Mathieu Turuani Contributors : Judson Santiago, Max Tuengerthal email .......: turuani@loria.fr URL .........: www.loria.fr/equipes/cassis/softwares/AtSe/ www.loria.fr/~turuani Institute ...: Loria - INRIA Team ........: CASSIS Address .....: Loria-INRIA, Cassis Team, Campus Scientifique, BP 239, 54506 Vandoeuvre-lès-Nancy France Project .....: AVISPA - Automated Validation of Internet Security Protocols and Applications Project URL .: www.avispa-project.org =========================================================== Overview: --------- CL-Atse is an OCaml-based implementation of the deduction rules developed in the CASRUL tool-suite, the AVISPA European project, and the AVANTSSAR European Project. These rules allows anyone to interpret and automatically "execute" a protocol or more generally a web service in every possible ways against an generic intruder with the Dolev-Yao deductional capabilities. A protocol, written in the Avispa's intermediate format or in the newest ASLAN v1 language for AVANTSSAR is executed over a finite (user decided) number of iterations, or entirely if no loop is involved. There are no other restrictions: either an attack is found, or the protocol is claimed to be secured over the given number of sessions. The search for attacks can be parametrised. In particular, the service's objects can be typed or untyped, and the pair can be free or (partially) associative. Moreover, the analysis take care of the algebraic properties of the Xor operator, as well as the exponential. That is, as attack can rely on the properties of these operators, and security means that no attack exists even when relying on the properties of these operators. Finally, CL-Atse performs two kind of optimizations : First, the protocol specification itself is simplified to accelerate the search for attacks (steps merged or removed, useless messages ignored, etc..). Second, various optimizations in the deduction rules try to reduce, and often eliminate, redundancies and uselessness in the protocol execution. CL-Atse were developed in the context of the EU Project AVISPA (Automated Validation of Internet Security Protocols and Applications, www.avispa-project.org IST-2001-39252). Earlier development on CL-Atse took place in the context of the predecessor project AVISS (Automated Verification of Infinite-State Systems IST-2000-26410). CL-Atse is now developped in the context of the EU Project AVANTSSAR (Automated VAlidatioN of Trust and Security of Service-oriented ARchitectures, www.avantssar.eu FP7-ICT-2007-1 Project no. 216471). Even if the EU Project AVISPA is now closed, support for the two specification languages it defined is still up. In particular, CL-Atse accepts either IF (the Intermediate Format) files created by the AVISPA's translator hlpsl2if, or HLPSL files if the translator is available to CL-Atse, or the new Aslan specification language from the AVANTSSAR Project. With AVANTSSAR, a translator also exists from Aslan++ to Aslan. Install and USAGE: ------------------ You do not need anything to run cl-atse alone. This is the expected use with the AVANTSSAR Project. This is, if you have an Aslan file, you can annalyse it with : ./cl-atse something.aslan Many options are available to control the analysis : ./cl-atse --help Moreover, CL-Atse is usually shipped in many version, depending it it was compiled natively (this is the best/fastest) or in bytecode (interpreted at runtime). Moreover, you will can expect two native version of CL-Atse, one compiles on 64bits architecture, the other on 32bits architecture. Please look at the file names to choose most appropriate one for you. Ever precompiled distributions are for Linux, usually, but you can compile sources for other architectures using a standard OCaml intall plus a assembly compiler. To run CL-Atse through the other avispa's tools, make sure that : - the $AVISPA_PACKAGE variable contain the path to the avispa-package directory. For example, if it is in /home/mathieu/avispa-pack then with Debian uses $export AVISPA_PACKAGE=/home/mathieu/avispa-pack - the cl-atse binary file is present in the avispa-package hierarchy, at the following positions : $AVISPA_PACKAGE/bin/backends/cl/cl-atse for the binary file $AVISPA_PACKAGE/bin/backends/cl.bash for the script file Moreover, you can also choose to run cl-atse directly, as long as the hlpsl2if translator is accessible, that is : - either the $AVISPA_PACKAGE variable is filled as above, - or the hlpsl2if translator is present in the same directory as cl-atse In that case, you can simply run : ./cl-atse something.hlpsl and cl-atse will call hlpsl2if himself to produce the needed IF file. Naturally, if you already have an IF file, you can analyse it directly : ./cl-atse something.if This is the same for Aslan files : ./cl-atse something.aslan Finally, if you like benchmarks, you can provide a SET of protocol specifications to cl-atse (he then process them in sequence) and ask him to summarize the results in a table with the "-bench" option. This can be piped to compare different versions of cl-atse : ./cl-atse *.hlpsl -bench | ./cl-atse_old -bench Detailed Usage: --------------- Usually, CL-Atse is called directly by the AVISPA Tool. You can specify CL-Atse as the desired back-end using the --cl switch as follows: avispa [OPTIONS] --cl-atse [CL-ATSE OPTIONS] Should you wish to call CL-Atse directly, you can do so as follows: ( cl-atse is usually in $AVISPA_PACKAGE/bin/backends/cl/cl-atse ) cl-atse [CL-ATSE_OPTIONS] can be any set of if or hlpsl files. However, if any hlpsl file is provided, then the hlpsl2if translator must be accessible by cl-atse. This is either present in ./; path known by $HLPSL2IF; or accessible with the $AVISPA_PACKAGE variable (default). Be also aware that when given a set of input files, CL-Atse will output it's analysis of each sequentially. To give a set of files as input is particularly useful when using the -bench option. CL-ATSE_OPTIONS can be any set of cl-atse options including : -nb n : Maximum number of role iterations (or loops, default is 3) This option bound the maximum number of times cl-atse is allowed to re-execute any loop in the protocol specification. Since a role iteration (same role re-executed in sequence) is a loop, this also bound the maximum number of times each role instance is executed sequentially. However, this do not bound the parallel role executions, which are already bounded in the if file. -light : Force the use of non-associative unification algorithm. By default, this option is only activated if non restrictive. -notype : Do not take the typing constraints into account. That is, a variable of type pair can be instantiated with a cipher bloc or a nonce with this option. -td : Perform depth-first search (default, less memory) This control the search for attacks in cl-atse. This is the fastest search and the less memory dependant, but it can provide non-minimal attacks. -lr : Perform breath-first search (minimal attack) -short With this option, cl-atse always output one of the shortest attacks (if any). However, memory use can be much higher. -out : Write the attack to file.atk (if any). Simple stdout forward. -dir d : Output directory to use with -out. Also, any temporary if file generated by hlpsl2if is placed in this directory. (CL-Atse call hlpsl2if when provided with hlpsl file) -ns : Do not simplify the IF file (complete trace) With this option, Cl-Atse is forbidden to simplify the given protocol specification (if file). The protocol simplification is an important step which allows CL-Atse to search for attacks much more rapidly. Note that by default, cl-atse shows attacks in it's outputs without any simplification, whatever the protocol was internally simplified or not. Since CL-Atse's output is much nicer to read than the if file, this allows you to check that the translation of your protocol fit your expectations. -noopt : Do not try to optimise the protocol specification for cl-atse's analysis methods. (like replace hashing by tokens). Again, activating this option most probably slow down the analysis. By default, CL-Atse tries to re-organize the protocol to make it easier to check. This option disable this functionality. -v : Print more output informations. In particular, in this mode CL-Atse write the protocol specification as read form the .if file, and write a bit more attack informations. -vv : (Very Verbose) This option shows the protocol exactly as it was interpreted by cl-atse, that is, after both simplifications and optimisations. For debugging purposes. -noexec : Do not search for attacks. This disable the search for attacks. Consequently, all protocols are seen as "safe" with this option. Useful with -ns to look at the protocol specification. -bench : Benchmark output format (very concise). This option activate a benchmark mode for CL-Atse. In this mode, the output is extremely concise (one line per input if or hlpsl file), and stdin an be linked to the stdout of an other instance of cl-atse. For example, you can get a nice comparison table between typed an untyped models with : ~/hlpsl$ cl-atse -bench *.hlpsl | ./cl-atse -bench -notype -split : Use the --split option on hlpsl2if for hlpsl files. This option makes cl-atse run once per splited if file. -col n : Ask cl-atse to make it's output fit within n character columns. Special numbers : 0 means only one term per line, and -1 means no limit (default). --version : Show cl-atse's version number. --licence : Show cl-atse's licence file. -help : Display the complete list of options --help : Display the complete list of options ------------------------------------------ Send questions and bug reports to: Mathieu Turuani ------------------------------------------