Spi Calculus Translated to pi-Calculus Preserving May-Tests
2004 (English)In: Proceedings of LICS 2004: Logic in Computer Science, Los Alamitos, Calif: IEEE Computer Society, 2004, 22-31 p.Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
Los Alamitos, Calif: IEEE Computer Society, 2004. 22-31 p.
, Proceedings / Symposium on Logic in Computer Science, ISSN 1043-6871
IdentifiersURN: urn:nbn:se:uu:diva-71921DOI: 10.1109/LICS.2004.1319597ISBN: 0769521924OAI: oai:DiVA.org:uu-71921DiVA: diva2:99832
19th Annual IEEE Symposium on Logic in Computer Science, LICS 2004 : Turku, Finland, 13 - 17 July 2004