[moca] [techreport] a fully abstract encoding of applied pi

[Michael Baldamus <michaelb@xxxxxxxx>]

[ Apologies if you receive this message more than once. ]

Dear MOCA readers and others,

the following technical report has become available:

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

Michael Baldamus, Joachim Parrow and Björn Victor.

A Fully Abstract Encoding of the Applied pi-Calculus.

Technical Report 2005-004, Department of Information Technology,
Uppsala University, February 2005.

http://www.it.uu.se/research/reports/2005-004

Abstract
--------

The applied pi-calculus (piA) extends the pure pi-calculus by
including constructors and destructors for arbitrary data types,
where elements of these types can be transmitted between agents.
It has long been known how to encode such data types in pi, but
until now it has been open how to make the encoding _fully
abstract_, meaning that two encodings (in pi) are semantically
equivalent precisely when the original piA agents are
semantically equivalent. We present a new type of encoding and
prove it to be fully abstract with respect to may-testing
equivalence. To our knowledge this is the first result of its
kind, for any calculus enriched with data types. It has
particular importance when representing security properties since
attackers can be regarded as may-test observers. Full abstraction
proves that it does not matter whether such observers are
formulated in pi or piA, both are equally expressive in this
respect. The technical new idea consists of encoding data as
table entries rather than active processes, and using a
firewalled central integrity manager to ensure data security.

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

Best regards

  Michael Baldamus

+ Michael Baldamus (postdoctoral researcher) - Uppsala University,
| Department of Information Technology, Box 337, 751 05 UPPSALA,
| Sweden - Phone: +46.18.47 17 95 2 - Mobile: +46.70.36 79 37 3 -
| Home: +46.18.46 94 21 - Fax: +46.18.51 19 25 -
+ E-Mail: Michael.Baldamus@xxxxxxxx - Web: user.it.uu.se/~michaelb

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