Options
Adding branching to the strand space model
Citation Link: https://doi.org/10.15480/882.4033
Publikationstyp
Journal Article
Date Issued
2009-07-03
Sprache
English
Author(s)
TORE-DOI
Volume
242
Issue
1
Start Page
139
End Page
159
Citation
Electronic Notes in Theoretical Computer Science 242 (1): 139-159 (2009-07-09)
Publisher DOI
Scopus ID
Publisher
Elsevier Science
The strand space model is one of the most successful and widely used formalisms for analysing security protocols. This might seem surprising given that the model is not able to reflect choice points in a protocol execution: the key concept in the strand space model is that of a bundle, which models exactly one possible execution of a security protocol. Inspired by the branching processes of Petri nets, we show that branching can be introduced into the strand space model in a very natural way: bundles can be generalized to branching bundles, which are able to capture several conflicting protocol executions. Our investigations of the theory of branching bundles will motivate the concept of symbolic branching bundles, and culminate in the result that every protocol has a strand space semantics in terms of a largest symbolic branching bundle. We hope our results provide a strong theoretical basis for comparing models and providing process calculi semantics in security protocol analysis. Altogether our work is related but different to a series of works by Crazzolara and Winskel. Throughout we will profit from a close relationship of the strand space model to event structures, which has already been pointed out by these authors.
Subjects
branching processes
event structures
Models for security protocol analysis
strand spaces
DDC Class
004: Informatik
Publication version
publishedVersion
Loading...
Name
1-s2.0-S1571066109001960-main.pdf
Size
371.6 KB
Format
Adobe PDF