SpiDer: a security model checker

This paper presents SpyDer, a model checkeing 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 a run-time by providing each variables 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 flaws 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 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.