Michele Boreale, Marzia Buscemi
STA (Symbolic Trace Analyzer) is a prototype tool for the
analysis of security protocols. Within STA, a protocol is modeled as a
system of concurrent processes. STA analyzes the execution traces of
this system to detect possible faults of security properties, such as
authentication and secrecy.
STA accepts a description of the protocol in a language similar to
Abadi and Gordon' spi-calculus, and a specification of some property,
expressed in terms of traces generated by the protocol, e.g., "every commit
action of principal B happens only after the corresponding begin
action of principal A". If no attack against the specified property
exists, "No
attack was found" is reported. Otherwise, an attack is reported in the
form of an execution trace that violates the specified property.
Currently, shared-key, public-key cryptography and one-way hash functions are supported.
A key feature of STA is that exploration of the state-space is performed symbolically: in essence, STA uses a systematic method to avoid the explicit construction of all, possibly inenditely many, protocol traces. The theory underlying STA is developed and explained in full detail in [Bor01] and [BB02b].
STA is written in ML.
Please report comments and bugs to: Michele
Boreale (boreale.a.t.dsi.unifi.it) or Marzia Buscemi
(buscemi.a.t.di.unipi.it).
The distribution of STA consists of a .rar archive of two ML object files, STA.uo and STA.ui, and is available for Mac, Linux and Windows.
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.
Please refers to this documentation for installing and using STA.
We have tested STA on some simple protocols and compared our results to methods based on endite-state model checking (see [BB02a]). The files below include STA scripts for some of these protocols. These examples can be pasted into a text file and fed to the tool.