STA requires Moscow ML, a lightweight implementation of Standard ML. Moscow ML can be freely downloaded for various platforms from the MOSML page http://www.dina.kvl.dk/~sestoft/mosml.html.
Put the two files of the distribution, sta.uo and Sta.ui, into some directory of your choice. From that directory, launch the ML interactive environment. Give the following sequence of commands from the ML interaction window (whose prompt is written `>' below):
> load "Sta.uo";
> open Sta;
(please note the uppercase 'S').
The system is now ready to accept and verify specifications of
security protocols.
Warning: when running, STA needs to create and write 2 files, named STATemp and STAScript.
Each specification consists of a list of declarations, of 4 possible kinds (described below):
The four kinds of declarations can be mixed in any order, provided the obvious dependencies are respected.
Identifier (labels, names and variables) declarations :
DeclLabel $ a1, a2, ....,an $;
DeclName $ k1, k2,...,km $;
DeclVar $ x1, x3,..., xr $;
Process declarations (one of which typically represents the protocol to analyze):
val Pr = P;
where P is a process written according to the following syntax (inspired to Abadi and Gordon's spi-calculus):
P ::= stop (terminated process)
| a?x >> P (input: a is a label, x a variable)
| a!M >> P (output: a is a label, M is a message -- see below)
| (M is N) P (equality test and shared-key decryption:
M,N are messages -- see below)
| (M pkdecr (y,-u)) >> P (asymmetric decryption)
| P1 || P2 (parallel composition)
| P1 & P2 (nondeterministic choice)
| k new_in P (new-name: k is a name)
Labels, names and variables that appear in a process must have been declared before. The syntax of messages is:
M ::= u (name or variable)
| +u (encryption key)
| -u (decryption key)
| (M1,M2) (pair)
| {M}u (shared-key encryption of M under u)
| (M)^+u (asymmetric encryption of M under the key +u;
the corresponding decryption key is -u)
| H(M) (hashing of M)
Shared-key decryption is implemented via matching. When y is a variable not occurring in M, (M is {y}k) >> P works as follows: try and decrypt message M using key k; if decryption succeeds (i.e. if M is anything encrypted with k), bind the result to variable y and proceed like P, otherwise stop.
Asymmetric decryption (M pkdecr (y,-k)) >> P works as follows: try and decrypt message M using key -k; if decryption succeeds (i.e. if M is anything encrypted with +k), bind the result to variable y and proceed like P, otherwise stop.
Input actions may contain message patterns, which are interpreted in the obvious way. E.g, a?{x}k >> P is interpreted as a?y >> (y is {x}k) >> P, for some fresh variable y.
|| and (.,.) are right-associative.
Here is a list of the operators in decreasing order of precedence:
{.}u , (.)^+u, H(.)
( . , . )
!, ?, is, pkdecr
>>
new_in
|| , &
These precedences can be altered by round parentheses.
Comments can be inserted between pairs (* and *).
The symbol `$' should never be used outside variable, name or label declarations (either within comments).
Configuration declarations. A configuration is used to specify the initial environment's knowledge. Each such declaration has the form:
val Conf = (L @ Pr);where
L is a possibly empty list of input/output actions, L= [A1,...,An]. Each action is of the form a?M or a!M (the difference between input and output is not really relevant as far as L is concerned). These actions carry the information that is initially known to the environment.
Pr is a previously declared process.
val Prop = (A <-- B);
where A and B are input/output actions, of the form a?M or a!M. Actions may contain variables, which should be distinct from those appearing in processes. Moreover, variables occurring in A should also occur as variables of B (unless the flag MODE is set; see below).
The meaning of Prop is: "in every execution of the protocol, every instance of action B is preceded by the corresponding instance of action A". Here `instance' refers to the instantiation of variables in A, B. For example, a(x,{y}k) <-- b(x,y) means " in every execution of the protocol, for every x and y, each b(x,y) is preceded by some a(x,{y}k)".
A special action `Absurd' is provided, which cannot be executed. So, (Absurd <-- B) simply means "no instance of B is ever executed".
Suppose the file MySpec.sml contains a STA specification, as described above. From the ML interaction window, give the command:
> STAComp "MySpec.sml";
If no syntax error is reported, the system is now ready to verify any declared property Prop on any declared configuration Conf. To do this, from the ML interaction window, give the command:
> CHECK Conf Prop;
If an attack exists, it will be reported as a trace of Conf that violates Prop. Otherwise, "No attack was found" will be reported. Traces that are reported as attacks may contain free variables. A variable is meant as a placeholder that can be instantiated to any message the environment can produce.
There are two system flags, MODE and FULL, which have the following meaning:
if MODE = 1 then properties A <-- B are allowed where action A may also contain variables not occurring in B. These variables are regarded as existentially quantified. E.g., a({x,y}k) <-- b(x,z) means: for every x and z, every occurrence of b(x,z) is preceded by an occurrence of a({x,y}k), for some y. The verification algorithm is slower when MODE is set. The default value of MODE is 0.
if FULL = 1 then the whole set of cryptoprimitives can be used. If FULL = 0, only shared-key encryption is permitted, and a more specialized and faster verification algorithm is used. The default value of FULL is 0.
The value of these flags can be changed by assignment commands := given from the ML interaction window, e.g.:
> MODE:= 1;
When ML reports syntax errors, it is convenient to keep in mind that the ML internal representation of syntactic terms is slightly different from the concrete syntax described above. For example,