Automating open bisimulation checking for the Spi calculus

Alwen Tiu*, Jeremy Dawson

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    56 Citations (Scopus)

    Abstract

    We consider the problem of automating open bisimulation checking for the spi-calculus, an extension of the pi-calculus with cryptographic primitives. The notion of open bisimulation considered here is indexed by a (symbolic) environment, represented as bi-traces (i.e., pairs of symbolic traces), which encode the history of interaction between the intruder with the processes being checked for bisimilarity. A crucial part of the definition of this open bisimulation, that is, the notion of consistency of bi-traces, involves infinite quantification over a certain notion of "respectful substitutions". We show that one needs only to check a finite number of respectful substitutions in order to check bi-trace consistency. Our decision procedure uses techniques that have been well developed in the area of symbolic trace analysis for security protocols. More specifically, we make use of techniques for symbolic trace refinement, which transform a symbolic trace into a finite set of symbolic traces in a certain "solved form". Crucially, we show that refinements of a projection of a bitrace can be uniquely extended to refinements of the bi-trace, and that consistency of all instances of the original bi-trace can be reduced to consistency of its finite set of refinements. We then give a sound and complete procedure for deciding open bisimilarity for finite spi-processes.

    Original languageEnglish
    Title of host publication23rd IEEE Computer Security Foundations Symposium, CSF 2010
    Pages307-321
    Number of pages15
    DOIs
    Publication statusPublished - 2010
    Event23rd Computer Security Foundations Symposium, CSF 2010 - Edinburgh, United Kingdom
    Duration: 17 Jul 201019 Jul 2010

    Publication series

    NameProceedings - IEEE Computer Security Foundations Symposium
    ISSN (Print)1940-1434

    Conference

    Conference23rd Computer Security Foundations Symposium, CSF 2010
    Country/TerritoryUnited Kingdom
    CityEdinburgh
    Period17/07/1019/07/10

    Fingerprint

    Dive into the research topics of 'Automating open bisimulation checking for the Spi calculus'. Together they form a unique fingerprint.

    Cite this