Automating Open Bisimulation Checking for the Spi Calculus
-
Altmetric Citations
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.author | Tiu, Alwen | |
---|---|---|
dc.contributor.author | Dawson, Jeremy | |
dc.coverage.spatial | Edinburgh Scotland | |
dc.date.accessioned | 2015-12-07T22:55:22Z | |
dc.date.created | July 17-19 2010 | |
dc.identifier.uri | http://hdl.handle.net/1885/28353 | |
dc.description.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. | |
dc.publisher | IEEE Computer Society | |
dc.relation.ispartofseries | IEEE Computer Security Foundations Symposium 2010 | |
dc.source | Proceedings of IEEE Computer Security Foundations Symposium 2010 | |
dc.subject | Keywords: 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.title | Automating Open Bisimulation Checking for the Spi Calculus | |
dc.type | Conference paper | |
local.description.notes | Imported from ARIES | |
local.description.refereed | Yes | |
dc.date.issued | 2010 | |
local.identifier.absfor | 080303 - Computer System Security | |
local.identifier.ariespublication | u4963866xPUB57 | |
local.type.status | Published Version | |
local.contributor.affiliation | Tiu, Alwen, College of Engineering and Computer Science, ANU | |
local.contributor.affiliation | Dawson, Jeremy, College of Engineering and Computer Science, ANU | |
local.description.embargo | 2037-12-31 | |
local.bibliographicCitation.startpage | 15 | |
local.identifier.doi | 10.1109/CSF.2010.28 | |
local.identifier.absseo | 890199 - Communication Networks and Services not elsewhere classified | |
dc.date.updated | 2016-02-24T11:30:50Z | |
local.identifier.scopusID | 2-s2.0-77957574536 | |
local.identifier.thomsonID | 000308460400021 | |
Collections | ANU Research Publications |
Download
File | Description | Size | Format | Image |
---|---|---|---|---|
01_Tiu_Automating_Open_Bisimulation_2010.pdf | 356.02 kB | Adobe 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