[moca] Spi Calculus Translated to pi-Calculus Preserving May-Testing

[Michael Baldamus <michaelb@xxxxxxxx>]

[ Apologies if you receive more than one copy of this message. ]

The following technical report is available:


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

Spi Calculus Translated to pi-Calculus Preserving May-Testing

Michael Baldamus, Joachim Parrow, and Björn Victor

Uppsala University, Department of Information Technology,
Report 2003-063

http://www.it.uu.se/research/reports/2003-063


Abstract
========

We present a concise and natural encoding of the spi calculus
into the more basic pi-calculus and establish its correctness
with respect to a formal notion of testing. This is particularly
relevant for security protocols modelled in spi since the tests
can be viewed as adversaries. The translation has been implemented
in a prototype tool. As a consequence, protocols can be described
in the spi calculus and analysed with the emerging flora of tools
already available for pi. The translation also entails a more
detailed operational understanding of spi since high level constructs
like encryption are encoded in a well known lower level. The formal
correctness proof is nontrivial and interesting in its own ; so
called context bisimulations and new techniques for compositionality
make the proof simpler and more concise.

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


Any comments, remarks and suggestions will be greatly appreciated.

Regards

  Michael

+ Michael Baldamus (postdoc) - Uppsala University, Department of
| Information Technology, Box 337, 751 05 UPPSALA, Sweden
| E-Mail: Michael.Baldamus@xxxxxxxx - Link: user.it.uu.se/~michaelb
+ Phone: +46.18.471 7952 - Fax: +46.18.511925

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