SATMC v. 2.0
=============

SATMC (SAT-based Model Checker) is an open and flexible platform for
model-checking security protocols via reduction to SAT.  SATMC takes
as input a security problem expressed either in the IF or SATE
language and returns either an attack or fail stating that no attack
has been found on the input security problem.

SATMC is currently interfaced with the sat solvers Chaff (you can get
it at the URL http://www.ee.princeton.edu/~chaff/), SIM (you can get
it at http://www.mrg.dist.unige.it/star/sim/home.html. Note that the
version of the interfaced SIM has been modified by its staff for
returning the assignment relative to the propositional formula.)  and
SATO (you can get it at http://www.cs.uiowa.edu/~hzhang/sato).


RUNNING
--------

You can execute SATMC v.2.0 to issue at the shell prompt:

  "satmc OPTION"
  "satmc FILE [OPTIONS]" 

where:

* OPTION:
  -h,  --help       display this help and exit.
  -v,  --version    output version information and exit.
  -ex, --examples   output some examples of usage of the SATMC 
		    executable.

* OPTIONS:

  --solver=SOLVER		: SOLVER is the selected state-of-the-art 
				  SAT solver you want to use to
				  evaluate the satisfiability of the
				  generated propositional formula.
				  Accepted value are:
	                            'chaff'    : Chaff2 solver selected;
		                    'sim'      : SIM solver selected; 
		                    'sato'     : SATO solver selected.
				  (Default value of SOLVER is 'chaff'.)

  --max=MAX        		: MAX is the maximum depth of the 
				  search space up to which SATMC will
				  explore; it can be set to -1 meaning
				  infinite, but in this case the
				  procedure is not guaranteed to
				  terminate; by default it is set to
				  11;

  --enc=ENC	 		: ENC is the selected SAT reduction 
				  encoding technique; it can be set to
				  either 'linear' or 'graphplan'
				  (default value);

  --absRef=ABSREF		: ABSREF is a boolean parameter for 
				  enabling or disabling the
				  abstraction/refinement strategy the
				  back-end provides; by default it is
				  set to false (i.e.the mutex axioms
				  are generated and therefore the
				  abstraction/refinement strategy is
				  disabled);

  --output_dir=ODIR		: ODIR is the directory in which SATMC 

				  will store temporary files and put
				  the results of the analyses; (by
				  default these files will be put in
				  the same directory in which FILE is
				  contained);

  --if2sate=IF2SATE		: IF2SATE is the version of the 
				  compiler used for translating a IF
				  specification into a SATE
				  specification; it can be set either
				  to 1 (default value) or 2;

  --prelude=PRELUDE		: PRELUDE is the prelude file 
				  (comprehensive of the path); by
				  default it is assumed that the
				  prelude file is in the same
				  directory of FILE with the name
				  'prelude.if';

  --avispa=AVISPA 		: AVISPA is a boolean parameter for 
				  enabling or disabling the AVISPA
				  output format; for more details on
				  the EU project AVISPA see
				  http://www.avispa-project.org.

* FILE is either the IF or the SATE file (comprehensive of the path)
  you want to translate and to analyze.


MAILING LIST
--------------------

You can use two mailing list:

satmc-support@mrg.dist.unige.it   - to send messages to the SATMC team
satmc-users@mrg.dist.unige.it     - to exchange messages with other SATMC 
				    users


AUTHORS
--------
Written by: Alessandro Armando              and Luca Compagna
email:      armando@dist.unige.it           and compa@mrg.dist.unige.it
URL:        www.mrg.dist.unige.it/~armando  and www.mrg.dist.unige.it/~compa

Address:    DIST -- Universita' degli Studi di Genova
            Viale Causa 13
            16145 Genova 
            ITALIA

Project:      AVISPA - Automated Validation of Internet Security Protocols 
		       and Applications

Project URLs: http://www.mrg.dist.unige.it/satmc/
	      http://www.avispa-project.org/	

Send bug-reports and/or questions to: satmc-support@mrg.dist.unige.it