Skip to main content
SpringerLink
Log in
Book cover

Transactions on Computational Science IV pp 149–176Cite as

Security Analysis of Role Based Access Control Models Using Colored Petri Nets and CPNtools

  • Chapter

Part of the book series: Lecture Notes in Computer Science ((TCOMPUTATSCIE,volume 5430))

Abstract

Several advanced Role based access control (RBAC) models have been developed supporting specific features (i.e.: role hierarchy, separation of duty) to achieve high flexibility. However, integrating additional features also increases their design complexity, and consequently the opportunity for mistakes that may cause information to flow to inappropriate destinations. In this paper, we present a formal technique to model and analyze RBAC using Colored Petri nets (CP-nets) and CPNtools for editing and analyzing CP-nets. Our purpose is to elaborate a CP-net model which describes generic access control structures based on an RBAC policy. The resulting CP-net model can be then composed with different context-specific aspects depending on the application. A significant benefit of CP-nets and, particularly, CPNtools is to provide a graphical representation and an analysis framework that can be used by security administrators to understand why some permissions are granted or not and to detect whether security constraints are violated.

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

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Samarati, P., di Vimercati, S.d.C.: Access control: Policies, models, and mechanisms. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 137–196. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  2. Sandhu, R.S., Coyne, E.J., Feinstein, H.L., Youman, C.E.: Role-based access control models. Computer 29(2), 38–47 (1996)

    Article  Google Scholar 

  3. Ferraiolo, D.F., Sandhu, R., Gavrila, S., Kuhn, D.R., Chandramouli, R.: Proposed NIST standard for role-based access control. ACM Trans. Inf. Syst. Secur. 4(3), 224–274 (2001)

    Article  Google Scholar 

  4. Barkley, J.F., Cincotta, A.V., Ferraiolo, D.F., Gavrila, S., Kuhn, D.R.: Role based access control for the world wide web. In: Proc. 20th NIST-NCSC National Information Systems Security Conference, pp. 331–340 (1997), http://citeseer.ist.psu.edu/101918.html

  5. Jensen, K., Kristensen, L.M., Wells, L.: Coloured petri nets and CPN tools for modelling and validation of concurrent systems. STTT 9(3-4), 213–254 (2007)

    Article  Google Scholar 

  6. Shafiq, B., Masood, A., Joshi, J., Ghafoor, A.: A role-based access control policy verification framework for real-time systems. In: WORDS 2005: Proceedings of the 10th IEEE International Workshop on Object-Oriented Real-Time Dependable Systems, pp. 13–20. IEEE Computer Society, Washington (2005), http://dx.doi.org/10.1109/WORDS.2005.11

    Google Scholar 

  7. Petri, C.A.: Kommunikation mit automaten. Ph.D. thesis, Institut für instrumentelle Mathematik, Bonn (1962)

    Google Scholar 

  8. Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use (1997) Three Volumes

    Google Scholar 

  9. Zhang, Z.L., Hong, F., Liao, J.G.: Modeling chinese wall policy using colored petri nets. In: CIT 2006: Proceedings of the Sixth IEEE International Conference on Computer and Information Technology, p. 162. IEEE Computer Society, Washington (2006), http://dx.doi.org/10.1109/CIT.2006.123

    Google Scholar 

  10. Bertino, E., Bonatti, P.A., Ferrari, E.: TRBAC: A temporal role-based access control model. ACM Trans. Inf. Syst. Secur. 4(3), 191–233 (2001), doi:10.1145/501978.501979

    Article  Google Scholar 

  11. Ahn, G.J., Hu, H.: Towards realizing a formal RBAC model in real systems. In: SACMAT 2007: Proceedings of the 12th ACM symposium on Access control models and technologies, pp. 215–224. ACM, New York (2007), http://doi.acm.org/10.1145/1266840.1266875

    Google Scholar 

  12. Joshi, J., Bertino, E., Latif, U., Ghafoor, A.: A generalized temporal role-based access control model. IEEE Transactions on Knowledge and Data Engineering 17(1), 4–23 (2005), doi:10.1109/TKDE.2005.1

    Article  Google Scholar 

  13. Gavrila, S.I., Barkley, J.F.: Formal specification for role based access control user/role and role/role relationship management. In: RBAC 1998: Proceedings of the third ACM workshop on Role-based access control, pp. 81–90. ACM, New York (1998), http://doi.acm.org/10.1145/286884.286902

    Chapter  Google Scholar 

  14. Li, J., Fan, Y., Zhou, M.: Performance modeling and analysis of workflow. IEEE Transactions on Systems, Man and Cybernetics, Part A 34(2), 229–242 (2004), doi:10.1109/TSMCA.2003.819490

    Article  Google Scholar 

  15. Ahmed, T., Tripathi, A.R.: Static verification of security requirements in role based CSCW systems. In: SACMAT 2003: Proceedings of the eighth ACM symposium on Access control models and technologies, pp. 196–203. ACM, New York (2003), http://doi.acm.org/10.1145/775412.775438

    Google Scholar 

  16. Van der Aalst, W.: The application of petri nets to workflow management. The Journal of Circuits, Systems and Computers 8(1), 21–66 (1998)

    Article  Google Scholar 

  17. Knorr, K.: Dynamic access control through petri net workflows. In: ACSAC 2000: Proceedings of the 16th Annual Computer Security Applications Conference, p. 159. IEEE Computer Society, Washington (2000)

    Google Scholar 

  18. Varadharajan, V.: Hook-up property for information flow secure nets. In: Proceedings of Computer Security Foundations Workshop IV, pp. 154–175 (1991), doi:10.1109/CSFW.1991.151582

    Google Scholar 

  19. Juopperi, J.: PrT-net based analysis of information flow security nets. Research Report A34, Helsinki University of Technology, Department of Computer Science and Engineering, Digital Systems Laboratory, Espoo, Finland (1995)

    Google Scholar 

  20. Knorr, K.: Multilevel security and information flow in petri net workflows. Tech. rep. In: Proceedings of the 9th International Conference on Telecommunication Systems - Modeling and Analysis, Special Session on Security Aspects of Telecommunication Systems (2001)

    Google Scholar 

  21. Juszczyszyn, K.: Verifying enterprise’s mandatory access control policies with coloured petri nets. In: WETICE 2003: Proceedings of the Twelfth International Workshop on Enabling Technologies, p. 184. IEEE Computer Society, Washington (2003)

    Google Scholar 

  22. Rakkay, H., Boucheneb, H.: Timed secure colored petri net based analysis of information flow. Annals of Telecommunications (2006)

    Google Scholar 

  23. Jiang, Y., Lin, C., Yin, H., Tan, Z.: Security analysis of mandatory access control model. In: IEEE International Conference on Systems, Man and Cybernetics, 2004, vol. 6, pp. 5013–5018 (2004), doi:10.1109/ICSMC.2004.1400987

    Google Scholar 

  24. Zhang, Z.L., Hong, F., Xiao, H.J.: Verification of strict integrity policy via petri nets. In: ICSNC 2006: Proceedings of the International Conference on Systems and Networks Communication, p. 23. IEEE Computer Society, Washington (2006), http://dx.doi.org/10.1109/ICSNC.2006.76

    Chapter  Google Scholar 

  25. Rakkay, H., Boucheneb, H.: Using timed colored petri net to formalize temporal role based access control policies. In: Proceedings of the 7th International Conference on New Technologies of Distributed Systems, Marrakesh, Morocco (2007)

    Google Scholar 

  26. Bell, D.E., LaPadula, L.J.: Secure computer systems: Mathematical foundations. Tech. Rep. MTR-2547, MITRE Corporation, Bedford (1973)

    Google Scholar 

  27. Genrich, H.J.: Predicate/transition nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 254, pp. 207–247. Springer, Heidelberg (1987)

    Google Scholar 

  28. Brewer, D.D.F., Nash, D.M.J.: The chinese wall security policy. sp 00, 206 (1989), http://doi.ieeecomputersociety.org/10.1109/SECPRI.1989.36295

    Google Scholar 

  29. Biba, K.J.: Integrity considerations for secure computer systems. Tech. Rep. MTR-3153, MITRE Corporation, Bedford (1977)

    Google Scholar 

  30. Atluri, V., kuang Huang, W.: An authorization model for workflows. In: Martella, G., Kurth, H., Montolivo, E., Bertino, E. (eds.) ESORICS 1996. LNCS, vol. 1146, pp. 44–64. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  31. Yi, Z., Yong, Z., Weinong, W.: Modeling and analyzing of workflow authorization management. J. Netw. Syst. Manage. 12(4), 507–535 (2004), http://dx.doi.org/10.1007/s10922-004-0674-3

    Article  Google Scholar 

  32. Wedde, H.F., Lischka, M.: Modular authorization and administration. ACM Trans. Inf. Syst. Secur. 7(3), 363–391 (2004), http://doi.acm.org/10.1145/1015040.1015042

    Article  Google Scholar 

  33. Shin, W.: An extension of role based access control for trusted operating systems and its coloured petri net model. Ph.D. thesis, Gwangju Institute of Science and Technology, Korea (2005)

    Google Scholar 

  34. Zao, J., Wee, H., Chu, J., Jackson, D.: RBAC schema verification using lightweight formal model and constraint analysis (2002), http://alloy.mit.edu/community/node/221

  35. Yuan, C., He, Y., He, J., Zhou, Z.: A verifiable formal specification for RBAC model with constraints of separation of duty. In: Lipmaa, H., Yung, M., Lin, D. (eds.) Inscrypt 2006. LNCS, vol. 4318, pp. 196–210. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  36. Drouineaud, M., Bortin, M., Torrini, P., Sohr, K.: A first step towards formal verification of security policy properties for RBAC. In: QSIC 2004: Proceedings of the Quality Software, Fourth International Conference, pp. 60–67. IEEE Computer Society, Washington (2004), http://dx.doi.org/10.1109/QSIC.2004.2

    Google Scholar 

  37. Zhao, C., Heilili, N., Liu, S., Lin, Z.: Representation and reasoning on RBAC: A description logic approach. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 381–393. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  38. Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002), http://doi.acm.org/10.1145/505145.505149

    Article  Google Scholar 

  39. Spivey, J.M.: The Z notation: a reference manual. Prentice Hall International (UK) Ltd., Hertfordshire (1992)

    MATH  Google Scholar 

  40. Canada, O.: Z/EVES version 1.5: An overview. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 367–376. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  41. Brucker, A.D., Rittinger, F., Wol, B., ludwigs-universitat Freiburg, A.: HOL-Z 2.0: A proof environment for Z-specifications. Journal of Universal Computer Science 9, 152–172 (2002)

    Google Scholar 

  42. Lenzerini, M.: A uniform framework for concept definitions in description logics. Journal of Artificial Intelligence Research 6, 87–110 (1997)

    MathSciNet  MATH  Google Scholar 

  43. Knorr, K., Weidner, H.: Analyzing separation of duties in petri net workflows. In: Gorodetski, V.I., Skormin, V.A., Popyack, L.J. (eds.) MMM-ACNS 2001. LNCS, vol. 2052, pp. 102–114. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  44. Jaeger, T., Tidswell, J.E.: Practical safety in flexible access control models. ACM Trans. Inf. Syst. Secur. 4(2), 158–190 (2001), http://doi.acm.org/10.1145/501963.501966

    Article  Google Scholar 

  45. Neumann, G., Strembeck, M.: An approach to engineer and enforce context constraints in an RBAC environment. In: SACMAT 2003: Proceedings of the eighth ACM symposium on Access control models and technologies, pp. 65–79. ACM, New York (2003), http://doi.acm.org/10.1145/775412.775421

    Google Scholar 

  46. Nyanchama, M., Osborn, S.: The role graph model and conflict of interest. ACM Trans. Inf. Syst. Secur. 2(1), 3–33 (1999), http://doi.acm.org/10.1145/300830.300832

    Article  Google Scholar 

  47. Koch, M., Mancini, L.V., Parisi-Presicce, F.: A graph-based formalism for RBAC. ACM Trans. Inf. Syst. Secur. 5(3), 332–365 (2002), http://doi.acm.org/10.1145/545186.545191

    Article  Google Scholar 

  48. Harrison, M.A., Ruzzo, W.L., Ullman, J.D.: Protection in operating systems. Commun. ACM 19(8), 461–471 (1976), http://doi.acm.org/10.1145/360303.360333

    Article  MATH  Google Scholar 

  49. Choppy, C., Petrucci, L., Reggio, G.: Designing coloured petri net models: a method. In: Proceedings of the 8th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools Aarhus, Denmark, pp. 22–24 (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. École Polytechnique de Montréal, Québec, Canada

    Hind Rakkay & Hanifa Boucheneb

Authors
  1. Hind Rakkay
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hanifa Boucheneb
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Calgary, 2500 University Drive N.W., T2N 1N4, Calgary, AB, Canada

    Marina L. Gavrilova

  2. OptimaNumerics Ltd., Cathedral House, 23-31 Waring Street, BT1 2DX, Belfast, UK

    C. J. Kenneth Tan

  3. University of Amazonas State - UEA Manaus, AM, Brazil

    Edward David Moreno

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Rakkay, H., Boucheneb, H. (2009). Security Analysis of Role Based Access Control Models Using Colored Petri Nets and CPNtools. In: Gavrilova, M.L., Tan, C.J.K., Moreno, E.D. (eds) Transactions on Computational Science IV. Lecture Notes in Computer Science, vol 5430. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-01004-0_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-01004-0_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-01003-3

  • Online ISBN: 978-3-642-01004-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation