Issue No. 06 - November/December (2011 vol. 8)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TDSC.2010.43
Hejiao Huang , Harbin Institute of Technology Shenzhen Graduate School, Shenzhen
Hélène Kirchner , INRIA Bordeaux Sud-Ouest, France, Talence
Security policies are one of the most fundamental elements of computer security. Current security policy design is concerned with the composition of components in security systems and interactions among them. Consequently, in a modular specification and verification of a policy, the composition of the modules must consistently assure security policies. A rigorous and systematic way to predict and assure such critical properties is crucial. This paper addresses the problem in a formal way. It uses colored Petri net process (CPNP) to specify and verify security policies in a modular way. It defines fundamental policy properties, i.e., completeness, termination, consistency, and confluence in Petri net terminology and gets some theoretical results. According to the eXtensible Access Control Markup Language (XACML) combiners and property preserving Petri net process algebra (PPPA), several policy composition operators are specified and property preserving results are stated for the policy correctness verification. As an application, the approach is illustrated for the design of Chinese Wall Policy.
Security policy, colored Petri net, specification and verification, property preservation.
H. Huang and H. Kirchner, "Formal Specification and Verification of Modular Security Policy Based on Colored Petri Nets," in IEEE Transactions on Dependable and Secure Computing, vol. 8, no. , pp. 852-865, 2010.