paper announcement

[Michele Boreale <boreale@xxxxxxxxxxxx>]

Dear all,

I would like to announce a paper  and a tool on analysis of cryptographic
protocols [its main focus is not on mobility, but I hope it may be of some
interest to  people in this list.]


Title: Symbolic trace analysis  of cryptographic protocols
Author: Michele Boreale

Abstract
A cryptographic protocol  can be described as a system of   concurrent
processes, and analysis of the traces generated by  this system  can be used
to verify authentication and secrecy properties of the protocol.
However, this approach suffers from a state-explosion problem  that causes
the set  of states and traces to be typically infinite or very large.
In this paper, starting from  a process language inspired by the
spi-calculus,
we   propose a symbolic operational semantics  that relies on  unification and
leads to compact models of protocols.
We prove that the symbolic and the conventional semantics are in full
agreement, and then give a method by which trace analysis can be
carried out directly on the symbolic model. The method is proven to
be complete for the considered class of properties  and is amenable to
to automatic checking.



The paper is available from http://www.dsi.unifi.it/~boreale/symbspi.ps

STA (Symbolic Trace Analyzer), a protoype implementation of the method, is
available from the page http://www.dsi.unifi.it/~boreale/tool.html

Comments will be very appreciated.

 Michele




===============================================
  Michele Boreale
  Dipartimento di Sistemi e Informatica
  Universita' di Firenze
  Via Lombroso, 6/17  --- I-50134 Firenze (Italy)
  phone:  +39 055 4796769    fax: +39 055 4796730

  e-mail: boreale@xxxxxxxxxxxx
  http://www.dsi.unifi.it/~boreale/

===============================================