Spi calculus translated to /spl pi/-calculus preserving may-tests
- 1 January 2004
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
We present a concise and natural encoding of the spi-calculus into the more basic /spl 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 /spl 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.Keywords
This publication has 12 references indexed in Scilit:
- An efficient cryptographic protocol verifier based on prolog rulesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Bisimulation Proof Methods for Mobile AmbientsLecture Notes in Computer Science, 2003
- On the symbolic reduction of processes with cryptographic functionsTheoretical Computer Science, 2003
- From Co-algebraic Specifications to Implementation: The Mihda ToolkitLecture Notes in Computer Science, 2003
- A Calculus for Cryptographic Protocols: The Spi CalculusInformation and Computation, 1999
- On the expressiveness of internal mobility in name-passing calculiTheoretical Computer Science, 1998
- Bisimulation for Higher-Order Process CalculiInformation and Computation, 1996
- Testing Equivalence for Mobile ProcessesInformation and Computation, 1995
- A calculus of mobile processes, IInformation and Computation, 1992
- Testing equivalences for processesTheoretical Computer Science, 1984