paper announcement

[Roberto Amadio <Roberto.Amadio@xxxxxxxxxxxxxxxxxx>]

Michele Boreale writes:
 > 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

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

With Denis Lugiez and Vincent Vanackere we have been doing some more
work on this topic that is described below. As Michele says [its main
focus is not on mobility, but I hope it may be of some interest to
people in this list.]

With kind regards,

Roberto Amadio

---------

On the symbolic reduction of processes with cryptographic functions

Available at 
http://www.cmi.univ-mrs.fr/~amadio/papers.html
To appear as INRIA-RR, March 2001.

ABSTRACT
We study the reachability problem for cryptographic protocols
represented as processes relying on perfect cryptographic
functions.  We introduce a symbolic reduction system that can
handle hashing functions, symmetric keys, and public keys.  Desirable
properties such as secrecy or authenticity are specified by
inserting logical assertions in the processes.

We show that the symbolic reduction system provides a flexible
decision procedure for finite processes and a reference for
sound implementations.  The symbolic reduction system can be regarded
as a variant of syntactic unification which is compatible
with certain set-membership constraints. For a significant fragment
of our formalism, we argue that a dag implementation of the
symbolic reduction system leads to an algorithm running in 
NPTIME thus matching the lower bound of the problem.

In the case of iterated or finite control processes, we
show that the problem is undecidable in general and in PTIME
for a subclass of iterated processes that do not rely on
pairing. Our technique is based on rational transductions of regular 
languages and it applies to a class of processes containing the
ping-pong protocols presented in Dolev et al 1982.

--------
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html