Spider: a Security Model Checker


Lenzini, G. and Gnesi, S. and Latella, D. (2003) Spider: a Security Model Checker. In: 1st Int. Workshop on Formal Aspect of Security and Trust (FAST), Pisa, Italy (pp. pp. 163-180).

open access
Abstract:This paper presents SpyDer, a model checking environment for security protocols. In SpyDer a protocol is described as a term of a process algebra (called spy-calculus) consisting in a parallel composition of a finite number of communicating and finite-behaviored processes. Each process represents an instance of a protocol's role. The Dolev-Yao intruder is implicitly defined in the semantics of the calculus as an environment controlling all the communication events. Security properties are written as formulas of a linear-time temporal logic. Specifically the spy-calculus has a semantics based on labeled transition systems whose traces are the temporal model over which the satisfiability relation of the temporal logic is defined. The model checker algorithm is a depth first search that tests the satisfiability of a formula over all the traces, generated on-the fly, from a typed version of calculus. Here the use of types is finalized to obtain finite-state models, where the number of messages coming from the intruder is finite. Typed terms (i.e. typed versions of a protocol description) are obtained at run-time by providing each variable with a sum of basic types. We prove that an attack over a typed version always implies the presence of an attack over the untyped version and more interesting, that if there is an attack over a specification, a typing transformation catching the flaw exists. The main contribution of the paper lives in the flexibility of the framework proposed. In fact the modeling environment is quite general and a protocol is specified once for all as an untyped spy-calculus term admitting infinite-state semantics. Then different typed versions, with finite-state semantics may be obtained in a semi-automatic way from the same untyped specification just providing types constraints. Moreover the use of a logic allows the specification of a not fixed a priori class of properties.
Item Type:Conference or Workshop Item
Additional information:Imported from DIES
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Link to this item:http://purl.utwente.nl/publications/66690
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page