STA, a Tool for the Analysis of

Cryptographic Protocols

Michele Boreale, Marzia Buscemi

Overview


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 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 (buscemi.a.t.di.unipi.it).


Download [Updated June 5th, 2007]

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.

STA.rar

Please refers to this documentation for installing and using STA. 


Examples

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.


References

[Bor01] Symbolic Trace Analysis of Cryptographic Protocols. M. Boreale. In Proc. of ICALP'01, LNCS 2076, Springer-Verlag, 2001. [.pdf]

[BB02a] Experimenting with STA, a Tool for Automatic Analysis of Security Protocols. M. Boreale, M. Buscemi. A shorter version appears in Proc. of SAC '02, ACM Press, 2002. [.pdf]

[BB02b] A Framework for the Analysis of Security Protocol. M. Boreale, M. Buscemi. To appear in Proc. of CONCUR '02. [.ps.gz]