### 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.

Original language | English |
---|---|

Number of pages | 18 |

Publication status | Published - Sep 2003 |

Event | 1st International Workshop on Formal Aspect of Security and Trust, FAST 2003 - CNR - Area della Ricerca di Pisa, Pisa, Italy Duration: 8 Sep 2003 → 8 Sep 2003 Conference number: 1 |

### Workshop

Workshop | 1st International Workshop on Formal Aspect of Security and Trust, FAST 2003 |
---|---|

Abbreviated title | FAST |

Country | Italy |

City | Pisa |

Period | 8/09/03 → 8/09/03 |

### Keywords

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

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

## Cite this

Lenzini, G., Gnesi, S., & Latella, D. (2003).

*SpyDer: a Security Model Checker*. Paper presented at 1st International Workshop on Formal Aspect of Security and Trust, FAST 2003, Pisa, Italy.