Notes:
The original publication is available at link.springer.com.
|
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.
|