------------------- SPAN 1.1 -------------------------- ------------------- A Security Protocol ANimator -------------------------- (For AVISPA) includes: - SPAN: a Security Protocol Animator for Avispa. This tool permits to simulate the execution of protocols specified in HLPSL. - a graphical interface to use with AVISPA verification tools for cryptographic protocols and SPAN. See file manual.pdf for the documentation on SPAN. Depending on availability on different architectures, the packages also include binary versions of tools from AVISPA: - hlpsl2if : a translator from HLPSL language to Intermediate Format - OFMC, ATSE, SATMC, TA4SP : verification tools for cryptographic protocols from the AVISPA project (see http://www.avispa-project.org) --------------------------------------------------------------------------- SPAN: Copyright (C) 2006-2007 Thomas Genet and Yann Glouche. This program is free software; you can redistribute it and/or modify it under the terms of the GNU Library General Public License version 2, as published by the Free Software Foundation. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. Those programs are distributed under the GNU LGPL. See the enclosed file COPYING and LGPL --------------------------------------------------------------------------- Changes and corrections from 1.0 to 1.1 - Corrected bug: bad semantic for '='. - Corrected bug: in intruder mode, keys in scrypt can be exp or xors and should be unified using Mathieu Turuani's matching algorithm. That is ok now. - Corrected bug: xor left or right member can be deduced if the other part is in intruder's knowledge. - In variable monitoring, content of a variable at step (i) is displayed ABOVE the transition (i). So as to avoid to have irrelevant dummy value of step 0 and also to be abble to display values of variable at the final step of the protocol. - Default mode is no message emissions - It is possible to change the size of the font and it is saved from one session to another. --------------------------------------------------------------------------- 1st of March 2007 (Compiled and tested with Ocaml 3.09: http://caml.inria.fr/ocaml/) In the next sections we successively give: - Prerequisites for running SPAN - Running instructions - Compilation instructions (if necessary) * PREREQUISITES: The SPAN library is distributed in four different forms: source, Windows, Linux, and MacOS binary files. SPAN needs Tcl/Tk but it is likely to be already installed on your system: - Tck/Tk 8.4 for Linux - Tcl/Tk 8.4 and (a running) Xfree for MacOS. Under MacOS, is generally installed with the Xcode tools. Check if the following libraries are present on your system: /sw/lib/libtcl8.4.dylib /sw/lib/libtk8.4.dylib If it is not the case install first Tcl/Tk using fink. It will download the files (as well as download Xfree if necessary) in the right place. - Tcl/Tk 8.3 for WINDOWS. (http://prdownloads.sourceforge.net/tcl/tcl832.exe for instance) Furthermore, on WINDOWS, after installing Tcl/Tk 8.3, your Tcl/Tk library must be in the PATH variable of your system. To find its location simply search for the file tk83.dll on your system. Then, if it is in the directory (say): C:/Program Files/Tcl/bin you have to add this directory to your PATH: set PATH= %PATH%;C:/Program Files/Tcl/bin The easiest way is to add this line to your autoexec.bat file (windows 2000) or to your system configuration by the system control panel ('advanced' Tab in windows XP), see windows help on the 'environment variable' subject. * RUNNING SPAN: - For Linux and MacOs users: Before running SPAN you have to set two environment variables. Let /usr/bob/span be the directory where you extracted SPAN: setenv SPAN /usr/bob/span (csh shell) or export SPAN=/usr/bob/span (bash shell) If the AVISPA system is NOT installed on your system, you can use the version of AVISPA which is embedded in the SPAN directory by setting the following environment variable: setenv AVISPA_PACKAGE /usr/bob/span (csh shell) or export AVISPA_PACKAGE=/usr/bob/span (bash shell) However, if AVISPA is already correctly installed, the better solution is to keep the initial value of this variable and use your installed version of AVISPA. Finally, to run SPAN, in a terminal window, set the current directory to the directory where you extracted all the files (/usr/bob/span in our example) and execute SPAN: ./span then refer to the reference manual 'manual.pdf' - For Windows users, set up the Tcl/Tk configuration (see PREREQUISITES), then double-click on the span application in the span directory then refer to the reference manual 'manual.pdf'. For 'old' versions of windows XP and old versions of Windows, it may be necessary to open the environment variable panel and check that the SPAN variable has been set by the installer. To do so: right-click on 'My computer', then click on the 'Advanced' tab, click on the 'environment variables' button, check that the directory of Tcl/Tk has been added to the PATH and that the SPAN variable has the correct value. Then, click on OK. SPAN should be ready to run. * COMPILATION INSTRUCTION: + Tcl/Tk 8.4 for Linux and MacOS. To check if your installation of Ocaml and Tcl/Tk works, simply search for the labltk binary on your system and execute it in command line window: it should start an Ocaml interpreter with Tcl/Tk support. If this does not work, check your Ocaml installation first or recompile Ocaml from the sources so that Tcl/Tk is taken into account. + Tcl/Tk 8.3 and Cygwin for WINDOWS. + Ocaml 3.09 or greater is necessary for compile source distribution of SPAN. Decompress the archive : the directory "span" is created. Set the environment variables (see 'RUNNING SPAN' part). Then, in the span directory, compile SPAN: make install (make installbytecode, for MacOS) Run the graphical interface with the command "./span". See the reference manual for other details. More details about compilation: In the directory containing the source files of SPAN, typing: 'make clean' cleans all the *.cmi, *.cmo, *.cmx, *.mli files generated by a compilation in byte code or in native code of SPAN. 'make depend' reinspect dependencies between files (file Makefile.dep must exist in the directory) 'make doc' generate a caml doc -> Windows users (Cygwin is necessary) The entire source distribution can be compiled with any complete installation of Ocaml (from 3.09) and the compilation scripts 'Makefile' included in the source distribution. If your Ocaml installation is not complete you will need at least: - labltk ocaml library. - ocamldep : needed if extending the source and recompiling. - ocamlc : needed if compiling in byte code. - ocamlopt: needed if compiling in native code. - ocamldoc : needed if generating a caml doc. - Cygwin : to use the 'make' command like in a UNIX system. Compiling in a Cygwin Command Window : There are still some bugs in the Makefile for this architecture, however the following works: Let $SPAN be the directory where you extracted the archive. * In the directory $SPAN/bin/protocol_simulation 1) replace the Makefile.dep files by an empty file: rm Makefile.dep touch Makefile.dep 2) build hlpsl2scenario make native * In the directory $SPAN, proceed in the same way: 1) replace the Makefile.dep files by an empty file: rm Makefile.dep touch Makefile.dep 2) build span make native ----------------------------------------------------------------------- Bug Report: Please report comments, improvements and bugs to Thomas.Genet@irisa.fr