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
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 infinitely 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
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
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 finite-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.