Skip to main content

Secure Bisimulation for Interactive Systems

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9530))

Abstract

In real applications, many systems have the same functions but their securities are different due to different security policies. We find that different security policies can affect the interacting behavior of a system, which exactly is the reason why a good policy can strengthen the security. In other words, two interactive systems with different security policies are not of an equivalent behavior although their functions are identical. However, the classic (weak) bisimulation theory draws an opposite conclusion that their behaviors are equivalent. The notion of (weak) bisimulation is not suitable for these security-oriented interactive systems since it does not consider a security policy while the security policy can affect their interacting behaviors. This paper proposes the concept of secure bisimulation in order to solve the above problem. Based on secure bisimulation, we furthermore define a binary relation \(\ge _{SL}\) to compare the levels of different security policies. We prove that \(\ge _{SL}\) is a partial order but not a total one.

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    The security of a system is related to many factors including cryptosystems, rights of accessing data, and other supporting policies like the one of separating “verification” from “login” in Fig. 1(b). The security in this paper is about those supporting policies rather than cryptosystems.

References

  1. Autant, C., Schnoebelen, P.: Place bisimulations in Petri nets. In: Jensen, K. (ed.) ICALP 1992. LNCS, vol. 616, pp. 45–61. Springer, Heidelberg (1992)

    Google Scholar 

  2. Boudol, G., Castellani, I.: On the semantics of concurrency: partial orders and transition systems. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds.) TAPSOFT 1987. LNCS, vol. 249, pp. 123–137. Springer, Heidelberg (1987)

    Google Scholar 

  3. van Glabbeek, R.J., Vaandrager, F.: Petri net models for algebraic theories of concurrency. In: de Bakker, J.W., Nijman, A.J., Treleaven, P.C. (eds.) PARLE Parallel Architectures and Languages Europe. LNCS, vol. 259, pp. 224–242. Springer, Heidelberg (1987)

    Chapter  Google Scholar 

  4. Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory. Languages and Computation. Addison-Wesley, Boston (1979)

    MATH  Google Scholar 

  5. Milner, R.: Communication and Concurrency. Printice Hall, Upper Saddle River (1989)

    MATH  Google Scholar 

  6. Milner, R.: Communicating and Mobile Systems: The \(\pi \)-Calculus. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

  7. Nielsen, M., Thiagarajaa, P.S.: Degrees of non-determinism and concurrency: a Petri net view. In: Joseph, M., Shyamasundar, R. (eds.) Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 181, pp. 89–117. Springer, Heidelberg (1984)

    Chapter  Google Scholar 

  8. Nielsen, M., Winskel, G.: Bisimulations and Petri nets. Theor. Comput. Sci. 153, 211–244 (1996)

    Article  MATH  Google Scholar 

  9. Pao, H.K., Fadlil, J., Lin, H.Y., Chen, K.T.: Trajectory analysis for user verification and recognition. Knowl.-Based Syst. 34, 81–90 (2012)

    Article  Google Scholar 

  10. Peterson, J.: Petri Net Theory and the Modeling of Systems. Prentice Hall, Upper Saddle River (1981)

    MATH  Google Scholar 

  11. Reisig, W.: Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies. Springer, Heidelberg (2013)

    Book  MATH  Google Scholar 

  12. Rúa, E.A., Castro, J.L.A.: Online signature verification based on generative models. IEEE Trans. Syst., Man, Cybern. B: Cybern. 42, 1231–1242 (2012)

    Google Scholar 

  13. Shen, C., Cai, Z., Guan, X., Du, Y., Maxion, R.A.: User authentication through mouse dynamics. IEEE Trans. Inf. Forensics Secur. 8, 16–30 (2013)

    Article  Google Scholar 

  14. Vogler, W.: Bisimulation and action refinement. In: Choffrut, C., Jantzen, M. (eds.) STACS 1991. LNCS, vol. 480, pp. 309–321. Springer, Heidelberg (1991)

    Google Scholar 

Download references

Acknowledgement

The authors would like to thank the three reviewers for their helpful comments. This paper is supported in part by the Alexander von Humboldt Foundation and in part by the National Natural Science Foundation of China (Grant Nos. 61202016, 61572360, and 91218301).

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Guanjun Liu .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Liu, G., Jiang, C. (2015). Secure Bisimulation for Interactive Systems. In: Wang, G., Zomaya, A., Martinez, G., Li, K. (eds) Algorithms and Architectures for Parallel Processing. ICA3PP 2015. Lecture Notes in Computer Science(), vol 9530. Springer, Cham. https://doi.org/10.1007/978-3-319-27137-8_45

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-27137-8_45

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-27136-1

  • Online ISBN: 978-3-319-27137-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics