• Analysis and Verification of Cascading Phenomenon Based on Model Checking for Privacy-aware RBAC   [MASS 2012]
  • Author(s)
  • Mingjie Tang, Li Pan
  • Privacy has been regarded to be a critical requirement for various environments; Privacy-aware Role Based Access Control (P-RBAC) that extends the well known RBAC model is a model that can adequately support the fine-grained specification of privacy policies. Despite the enhanced privacy protection mechanism by P-RBAC, its cascading phenomenon within more than two polices which could lead to infinite execution are not detected and solved. In order to detect this phenomenon caused by the obligation element in P-RBAC, we propose a way that transforms such phenomenon into the process of examining cycles in a directed graph. An algorithm of translating the process into a model checking formalism is also proposed to do automatic verification. According the result, the criteria that solve the cascading are given. The experiments show that this algorithm can automatically detect the cascading in expected complexity, and solve it effectively.
  • RBAC; obligation; cascading; model checking
  • References
  • [1]
    Qun Ni, Elisa Bertino, Jorge Lobo, Carolyn Brodie, Clare-Marie Karat. Privacy-Aware Role-Based Access control [J]. ACM Transactions on Information and System Security (TISSEC), 2010, Volume 13:1-31
    Yoonjeong Kim et al. Privacy-aware Role Based Access Control Model: Revisited for Multi-Policy Conflict Detection [C]. Information Science and Applications (ICISA), Seoul, April 2010,1-7.
    Qun Ni, E. Bertino. An obligation model bridging access control policies and privacy policies[C]. SACAMT’08, NY, June 11-13 2008,133-142.
    Elisa Bertino, Carolyn Brodie, Seraphin Calo. Analysis of Privacy and Security Policies [J].IBM Journal of Research and Development, 2009,Volume 53,Issue 2:1-31.
    Clarke E M, Grumberg O, Peled D A. Model checking [M]. Massachuetts,USA:MIT Press, 2000:33-163.
    Vincent C.Hu, D.Richard Kuhn, Tao Xie, Jeehyun Hwang. Model Checking for verification of mandatory access control models and properties [J].International Journal of Software Engineering and Knowledge Engineering. 2011,Volume 21,Issue 1:103-127
    David Power, Mark Slaymaker, Andrew Simpson. Automatic conformance checking of Role-based access control policies via Alloy [J]. ESSo S, LNCS, 2011, 6542 :15-28.
    M.Toahchoodee, I.Ray. Using Alloy to analyse a spatio-temporal access control model supporting delegation[J]. Information Security,IET, 2009, Volume3,Issue3:75-113.

Engineering Information Institute is the member of/source content provider to