loading...
Spi Calculus Translated to π--Calculus Preserving May-Tests
Turku, Finland July 13-July 17
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2004.131959719th Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Michael Baldamus, Uppsala University, Sweden
Joachim Parrow, Uppsala University, Sweden
Bj? Victor, Uppsala University, Sweden
We present a concise and natural encoding of the spi-calculus into the more basic π-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 π. The translation also entails a more detailed ooperational 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.
Citation:
Michael Baldamus, Joachim Parrow, Bj? Victor, "Spi Calculus Translated to π--Calculus Preserving May-Tests," lics, pp.22-31, 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.


Suggestions