SpyDer: a Security Model Checker

G. Lenzini, S. Gnesi, D. Latella

    Research output: Contribution to conferencePaperAcademicpeer-review

    9 Downloads (Pure)


    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.
    Original languageEnglish
    Number of pages18
    Publication statusPublished - Sep 2003
    Event1st International Workshop on Formal Aspect of Security and Trust, FAST 2003 - CNR - Area della Ricerca di Pisa, Pisa, Italy
    Duration: 8 Sep 20038 Sep 2003
    Conference number: 1


    Workshop1st International Workshop on Formal Aspect of Security and Trust, FAST 2003
    Abbreviated titleFAST


    • Security protocols
    • Security properties
    • Process algebras
    • Temporal logics
    • Model checking


    Dive into the research topics of 'SpyDer: a Security Model Checker'. Together they form a unique fingerprint.

    Cite this