Experimenting with STA, a tool for automatic analysis of security protocols
Michele Boreale, Maria Grazia Buscemi · 2002
We present STA (Symbolic Trace Analyzer), a tool for the analysis of security protocols. STA relies on symbolic techniques that avoid explicit construction of the whole, possibly infinite, state-space of protocols. This results in accurate protocol modeling, increased efficiency and more direct formalization, when compared to finite-state techniques. We illustrate the use of STA by analyzing the well-known asymmetric Needham Schroeder protocol. We discuss the results of this analysis, and contrast them with previous work based on finite-state model checking.