User Manual

Installation and contents.

After downloading the distribution unpack it following the instructions on the download page. The distribution contains the following directories:

Usage

ASPASyA takes as input four files: These files need to be passed to ASPASyA togheter with some switches to specify behaviour: ASPASyA outputs on the standard output so redirection to a file is suggested. Refer to examples to better understand ASPASyA usage.

Protocol specification

A protocol may be tought as a finite sequence of message between partecipants called principals. In ASPASyA a protocol is specified giving a cIP template of the principals involved. cIP is a name-passing calculus in the style of the well-known pi-calculus, adding cryptographic primitives. A cIP processes A: (X)[E]; is a principal whose name is A having open variables X and whose sequence of actions is specified by E.

Syntax

A principal is specified in a file with .pr extension.

Id :: = uppercase combination of letters #Usually S stands for a server, A for initiator and B for responder
Var ::= lowercase string not beginning with 'k' or 'n'  
Key ::= lowercase string beginning with 'k'  
Nonce ::= lowercase string beginning with 'n'  
Msg ::= (Msg, Msg) $ \;\;\mid\;\;$ {Msg}Msg $ \;\;\mid\;\;$ Key  
  $ \;\;\mid\;\;$ Id $ \;\;\mid\;\;$ Id+ $ \;\;\mid\;\;$ Id- $ \;\;\mid\;\;$ Nonce  
  $ \;\;\mid\;\;$ Var $ \;\;\mid\;\;$ ?Var $ \;\;\mid\;\;$ Var+ $ \;\;\mid\;\;$ Var-  
Act ::= in(Msg) $ \;\;\mid\;\;$ out(Msg)  
PROCESS ::= Act  
  $ \;\;\mid\;\;$ Act.PROCESS #Prefix
  $ \;\;\mid\;\;$ PROCESS + PROCESS #Non-deterministic choice
  $ \;\;\mid\;\;$ PROCESS $ \vert$ PROCESS #Parallel composition
PRINCIPAL ::= Id: (Var,...,Var) [PROCESS];  

A: (x) [in(?y).out({y}x)];
is an example of a principal A that reads a datum in y and encrypt y with x.

Properties specification

In ASPASyA security properties are expressed by the PL-logic (protocol logic) that allows one to express properties concerning values that variables are supposed to assume, membership of messages to the intruder's knowledge and relations among the values shared by different instances. Refer to examples to better understand how logic is used. We report the syntax:

Syntax

Formulae for security properties are specified in a .pl file.
FORMULA ::= INDEXED-VARIABLE = INDEXED-MESSAGE ||
            INDEXED-VARIABLE <> INDEXED-MESSAGE ||
            :> INDEXED-MESSAGE ||                   //Message can be derived from current knowledge
            !:> INDEXED-MESSAGE ||                  //Non derivability
            forall NAME.INDEX: FORMULA ||   //Universal quantifier 
            exists NAME.INDEX: FORMULA ||   //Existential quantifier
            [ not || ! ] FORMULA ||
            FORMULA [and || &] FORMULA ||
            FORMULA [or || |] FORMULA ||
            FORMULA [implies || =>] FORMULA ||
            (FORMULA) ||
            true || false
INDEX ::= a lowercase letter.
INDEXED-VARIABLE ::= VARIABLE_INDEX || VARIABLE_NAME_NUMBER
INDEXED-MESSAGE ::= MESSAGE_INDEX || MESSAGE_NAME_NUMBER     //Couples and Crypt are not indexed.

Invariant specification

Often we would like to specify an invariant property satisfied by all runs of a protocol. This property is specified in a .pj file using PL-Logic. Refer to examples for further explanation.

Knowledge specification

We can specify the initial knowledge as a list of messages separated by commas.