Skip navigation
Skip navigation

Automating Open Bisimulation Checking for the Spi Calculus

Tiu, Alwen; Dawson, Jeremy

Description

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...[Show more]

dc.contributor.authorTiu, Alwen
dc.contributor.authorDawson, Jeremy
dc.coverage.spatialEdinburgh Scotland
dc.date.accessioned2015-12-07T22:55:22Z
dc.date.createdJuly 17-19 2010
dc.identifier.urihttp://hdl.handle.net/1885/28353
dc.description.abstractWe 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.
dc.publisherIEEE Computer Society
dc.relation.ispartofseriesIEEE Computer Security Foundations Symposium 2010
dc.sourceProceedings of IEEE Computer Security Foundations Symposium 2010
dc.subjectKeywords: Bisimilarity; Bisimulation checking; Bisimulations; Cryptographic primitives; Decision procedure; Finite number; Finite set; Intruder deduction; Pi calculus; Security protocols; Spi calculus; Symbolic trace analysis; Trace refinement; Calculations; Networ Intruder deduction; Open bisimulation; Spi-calculus; Symbolic trace analysis
dc.titleAutomating Open Bisimulation Checking for the Spi Calculus
dc.typeConference paper
local.description.notesImported from ARIES
local.description.refereedYes
dc.date.issued2010
local.identifier.absfor080303 - Computer System Security
local.identifier.ariespublicationu4963866xPUB57
local.type.statusPublished Version
local.contributor.affiliationTiu, Alwen, College of Engineering and Computer Science, ANU
local.contributor.affiliationDawson, Jeremy, College of Engineering and Computer Science, ANU
local.description.embargo2037-12-31
local.bibliographicCitation.startpage15
local.identifier.doi10.1109/CSF.2010.28
local.identifier.absseo890199 - Communication Networks and Services not elsewhere classified
dc.date.updated2016-02-24T11:30:50Z
local.identifier.scopusID2-s2.0-77957574536
local.identifier.thomsonID000308460400021
CollectionsANU Research Publications

Download

File Description SizeFormat Image
01_Tiu_Automating_Open_Bisimulation_2010.pdf356.02 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  17 November 2022/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator