Paper Info
Title
Bisimulation for Demonic Schedulers
Abstract
Bisimulation between processes has been proven a successful method for formalizing security properties. We argue that in certain cases, a scheduler that has full information on the process and collaborates with the attacker can allow him to distinguish two processes even though they are bisimilar. This phenomenon is related to the issue that bisimilarity is not preserved by refinement. As a solution, we introduce a finer variant of bisimulation in which processes are required to simulate each other under the "same" scheduler. We formalize this notion in a variant of CCS with explicit schedulers and show that this new bisimilarity can be characterized by a refinement-preserving traditional bisimilarity. Using a third characterization of this equivalence, we show how to verify it for finite systems. We then apply the new equivalence to anonymity and show that it implies strong probabilistic anonymity, while the traditional bisimulation does not. Finally, to illustrate the usefulness of our approach, we perform a compositional analysis of the Dining Cryptographers with a non-deterministic order of announcements and for an arbitrary number of cryptographers.
Year
DOI
Venue
2009
10.1007/978-3-642-00596-1_23
FoSSaCS
Keywords
Field
DocType
certain case,traditional bisimulation,new equivalence,refinement-preserving traditional bisimilarity,arbitrary number,compositional analysis,dining cryptographers,new bisimilarity,demonic schedulers,strong probabilistic anonymity,finer variant
Transition system,Dining cryptographers problem,Computer science,Algorithm,Theoretical computer science,Equivalence (measure theory),Security properties,Bisimulation,Probabilistic logic,Anonymity,Probabilistic automaton
Conference
Volume
ISSN
Citations 
5504
0302-9743
10
PageRank 
References 
Authors
0.51
15
3
Name
Order
Citations
PageRank
Konstantinos Chatzikokolakis1104852.66
Gethin Norman24163193.68
David Parker34018184.00