Bisimulation for Demonic Schedulers

  • Konstantinos Chatzikokolakis
  • Gethin Norman
  • David Parker
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5504)


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.


Transition System Security Property Nondeterministic Choice Probabilistic Automaton Report Version 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Roscoe, A.W.: Modelling and verifying key-exchange protocols using CSP and FDR. In: Proc. CSFW, pp. 98–107. IEEE Computer Soc. Press, Los Alamitos (1995)Google Scholar
  2. 2.
    Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148, 1–70 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of POPL 2001, pp. 104–115. ACM, New York (2001)Google Scholar
  4. 4.
    Kremer, S., Ryan, M.D.: Analysis of an electronic voting protocol in the applied pi calculus. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 186–200. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    McLean: A general theory of composition for a class of “possibilistic” properties. IEEETSE: IEEE Transactions on Software Engineering 22 (1996)Google Scholar
  6. 6.
    Roscoe, B.: CSP and determinism in security modelling. In: Proc. of 1995 IEEE Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos (1995)Google Scholar
  7. 7.
    Chatzikokolakis, K., Palamidessi, C.: Making random choices invisible to the scheduler. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 42–58. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. 8.
    Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT (1995)Google Scholar
  9. 9.
    Chatzikokolakis, K., Norman, G., Parker, D.: Bisimulation for demonic schedulers. Technical report (2009),
  10. 10.
    Chatzikokolakis, K.: Probabilistic and Information-Theoretic Approaches to Anonymity. PhD thesis, Ecole Polytechnique, Paris (2007)Google Scholar
  11. 11.
    Baier, C.: Polynomial-time algorithms for testing probabilistic bisimulation and simulation. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 50–61. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  12. 12.
    Bhargava, M., Palamidessi, C.: Probabilistic anonymity. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 171–185. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Chaum, D.: The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of Cryptology 1, 65–75 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Canetti, R., Cheung, L., Kaynar, D., Liskov, M., Lynch, N., Pereira, O., Segala, R.: Task-structured probabilistic i/o automata. In: Proceedings the 8th International Workshop on Discrete Event Systems (WODES 2006), Ann Arbor, Michigan (2006)Google Scholar
  15. 15.
    Canetti, R., Cheung, L., Kaynar, D.K., Liskov, M., Lynch, N.A., Pereira, O., Segala, R.: Time-bounded task-PIOAs: A framework for analyzing security protocols. In: Dolev, S. (ed.) DISC 2006. LNCS, vol. 4167, pp. 238–253. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  16. 16.
    Garcia, F.D., van Rossum, P., Sokolova, A.: Probabilistic anonymity and admissible schedulers, arXiv:0706.1019v1 (2007)Google Scholar
  17. 17.
    Jürjens, J.: Secrecy-preserving refinement. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, p. 135. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  18. 18.
    Mantel, H.: Possibilistic definitions of security - an assembly kit. In: CSFW, pp. 185–199 (2000)Google Scholar
  19. 19.
    Lincoln, P., Mitchell, J., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: Proceedings of the 5th ACM Conference on Computer and Communications Security, pp. 112–121. ACM Press, New York (1998)CrossRefGoogle Scholar
  20. 20.
    Schneider, S., Sidiropoulos, A.: CSP and anonymity. In: Martella, G., Kurth, H., Montolivo, E., Bertino, E. (eds.) ESORICS 1996. LNCS, vol. 1146, pp. 198–218. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  21. 21.
    Chatzikokolakis, K., Knight, S., Panangaden, P.: Epistemic strategies and games on concurrent processes. In: Geffert, V., Karhumäki, J., Bertoni, A., Preneel, B., Návrat, P., Bieliková, M. (eds.) SOFSEM 2008. LNCS, vol. 4910. Springer, Heidelberg (2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Konstantinos Chatzikokolakis
    • 1
  • Gethin Norman
    • 2
  • David Parker
    • 2
  1. 1.Eindhoven University of TechnologyThe Netherlands
  2. 2.Oxford Computing LaboratoryUK

Personalised recommendations