A couple of papers.

[Marcelo Fiore <Marcelo.Fiore@xxxxxxxxxxxx>]

Semantics of Name and Value Passing, by M.Fiore and D.Turi.  To appear in 
LICS'01.  

  We provide a semantic framework for (first order) message-passing process
  calculi by combining categorical theories of abstract syntax with binding 
  and operational semantics.  In particular, we obtain abstract rule formats 
  for name and value passing with both late and early interpretations.  
  These formats induce an initial-algebra/final-coalgebra semantics that is 
  compositional, respects substitution, and is fully abstract for late and
  early congruence.  We exemplify the theory with the pi-calculus and 
  value-passing CCS.

  URL: http://www.cl.cam.ac.uk/~mpf23/papers/Concurrency/snvp.ps.gz


Computing Symbolic Models for Verifying Cryptographic Protocols, by M.Fiore 
and M.Abadi.  To appear in CSFW'01.

  We consider the problem of automatically verifying infinite-state 
  cryptographic protocols.  Specifically, we present an algorithm that given 
  a finite process describing a protocol in a hostile environment (trying to 
  force the system into a ``bad'' state) computes a model of traces on which 
  security properties can be checked.  Because of unbounded inputs from the 
  environment, even finite processes have an infinite set of traces; the main 
  focus of our approach is the reduction of this infinite set to a finite set 
  by a symbolic analysis of the knowledge of the environment.  Our algorithm 
  is sound (and we conjecture complete) for protocols with shared-key 
  encryption/decryption that use arbitrary messages as keys; further it is 
  complete in the common and important case in which the cryptographic keys 
  are messages of bounded size.

  URL: http://www.cl.cam.ac.uk/~mpf23/papers/Concurrency/symbmod.ps.gz

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