ASPASyA: Documentation

User Manual

Installation and contents.

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

bin/ -- contains the executable
docs/ -- contains this manual
protocols/ -- contains some examples

Usage

ASPASyA takes as input four files:

filename.pr -- containing the cIP template of principals involved in the protocol.
filename.pl -- containing the security formula to check specified in PL-Logic.
filename.pj -- containing the invariant property to be satisfied by all runs, specified in PL-Logic.
filename.kb -- containing the description of the initial intruder knowledge.

These files need to be passed to ASPASyA togheter with some switches to specify behaviour:

-T -- select trace output. The output of ASPASyA will be a text description of the analysed traces. You can specify a -t option to select only terminal traces.
-G param -- select GraphViz output. It is used to obtain a graphical representation of the state space but could be impractical for big LTS (Labelled Transition Systems). The output is in dot format and have to be processed with GraphViz to obtain a graphic file. -G has a numeric parameter specifying which information is added to the graph. It is a decimal number [0..15] obtained from a 4 bit number where each bit represent a graphical feature. Starting from the least significant bit:
- assignment -- add assignment description for each state
- knowledge -- add knowledge description
- action -- add the action labelling the transition
- context -- add the description of principals in the context
if you want to have actions and knowledge for each state, param should be 4 + 2 = 6 where 4 is action and 2 is knowledge. -G option is used for debug purposes and may be not present in final version.
-V -- select verification. The output of ASPASyA will be a description of the attacks found (if any).
-i -- select interactive verification. Not yet implemented. After finding an attack asks for continuation.
-f -- select feedback. While searching for an attack ASPASyA prints out an estimate of the time needed to complete the operations (it may be inaccurate depending on the property of the protocol). It also produces a summary of the elaboration.
-nprinc num -- specifies the number of principal instances in a context

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];

Summation has an higher precedence with respect to Parallelis (i.e. in(x)+out(y) | out(z)+in(w) means (in(x)+out(y)) | (out(z)+in(w)) )
Only variables and decorated names can occur as a key in a cryptogram (decorated names or variable are terminated by + or -. They represent public and private keys in asymmetric cryptography)
Comments are allowed everywhere. A comment can be a '//' and means that everything on that line is ignored. A multiline comment begina with '/*' and end with '*/'. Everything in between is ignored.
We assume that a cIP process can only perform a finite sequence of in(d) or out(d) actions where d is a message where variables can appear.
We denote the binding occurrences of a variable x with ?x and assume that, for any variable x, output actions out(d) do not contain any occurrence of ?x in d and input actions in(d) have at most one occurrence of ?x in d.

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.

- Comments are allowed everywhere. A comment can be a '//' and means that everything on that line is ignored. A multiline comment begin with '/*' and end with '*/'. Everything in between is ignored.
precedences between operator are: forall, exists &gt implies &gt and, or &gt not, derive, equal

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.