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. 163180).

Postscript
292kB 
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 spycalculus) consisting in a parallel composition of a finite number of communicating and finitebehaviored processes. Each process represents an instance of a protocol's role. The DolevYao 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 lineartime temporal logic. Specifically the spycalculus 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 onthe fly, from a typed version of calculus. Here the use of types is finalized to obtain finitestate 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 runtime 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 spycalculus term admitting infinitestate semantics. Then different typed versions, with finitestate semantics may be obtained in a semiautomatic 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 
Faculty:  Electrical Engineering, Mathematics and Computer Science (EEMCS) 
Link to this item:  http://purl.utwente.nl/publications/66690 
Export this item as:  BibTeX EndNote HTML Citation Reference Manager 
Repository Staff Only: item control page