[moca] expressivity on name generation

[Roberto Amadio <Roberto.Amadio@xxxxxxxxxxxxxxx>]

The following two (still unpublished) papers analyse the expressivity
of name generation. The study is carried on in two contexts: the
asynchronous pi-calculus and the Dolev-Yao model of cryptographic
protocols, and it refers in particular to the basic control
reachability problem.  Comments and pointers to related work we might
have missed are welcome. Full papers available at
	http://www.cmi.univ-mrs.fr/~amadio/papers.html

Truly,

Roberto Amadio
Laboratoire d'Informatique Fondamentale de Marseille

------------------

On decidability of the control reachability problem in the
asynchronous pi-calculus (joint work with Charles Meyssonnier)

ABSTRACT We study the decidability of the control reachability problem
for various fragments of the asynchronous pi-calculus. We consider the
combination of three main features: name generation, name mobility,
and unbounded control.  We show that the combination of name
generation with either name mobility or unbounded control leads to an
undecidable fragment.  On the other hand, we prove that name
generation with unique receiver and bounded input (a condition weaker
than bounded control) is decidable by reduction to the coverability
problem for Petri Nets with transfer.

-------------------

On name generation and set-based analysis in Dolev-Yao model
(joint work with Witold Charatonik)

ABSTRACT We study the control reachability problem in the Dolev-Yao
model of cryptographic protocols when principals are represented by
tail recursive processes with generated names.  We propose a
conservative approximation of the problem by reduction to a
non-standard collapsed operational semantics and we introduce
checkable syntactic conditions entailing the equivalence of the
standard and the collapsed semantics.  Then we introduce a
conservative and decidable set-based analysis of the collapsed
operational semantics and we characterize a situation where the
analysis is exact.  Finally, we describe how our framework can be used
to specify secrecy and freshness properties of cryptographic
protocols.

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