Sciweavers

FOSSACS
2009
Springer

Bisimulation for Demonic Schedulers

14 years 6 months ago
Bisimulation for Demonic Schedulers
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 usefuln...
Konstantinos Chatzikokolakis, Gethin Norman, David
Added 19 May 2010
Updated 19 May 2010
Type Conference
Year 2009
Where FOSSACS
Authors Konstantinos Chatzikokolakis, Gethin Norman, David Parker
Comments (0)