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...

• Type: Conference
• Year: 2009
• Where: FOSSACS
• Authors: Konstantinos Chatzikokolakis, Gethin Norman, David Parker
• Keywords: Applied Computing, Bisimulation, Certain Cases, FOSSACS 2009, Successful Method