This Article 
 Bibliographic References 
 Add to: 
Formal Specification and Verification of Modular Security Policy Based on Colored Petri Nets
November/December 2011 (vol. 8 no. 6)
pp. 852-865
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.

[1] H.J. Huang, “Enhancing the Property-Preserving Petri Net Process Algebra for Component-Based System Design (with Application to Designing Multi-Agent Systems and Manufacturing Systems),” PhD thesis, Dept. of Computer Science, City Univ. of Hong Kong, 2004.
[2] P.A. Bonatti, S.D.C. di Vimercati, and P. Samarati, “An Algebra for Composing Access Control Policies,” ACM Trans. Information and System Security, vol. 5, no. 1, pp. 1-35, 2002.
[3] D. Wijesekera and S. Jajodia, “A Propositional Policy Algebra for Access Control,” ACM Trans. Information and System Security, vol. 6, no. 2, pp. 286-325, 2003.
[4] L. Bauer, J. Ligatti, and D. Walker, “Composing Security Policies with Polymer,” Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), pp. 305-314, 2005.
[5] A.J. Lee, J.P. Boyer, L.E. Olson, and C.A. Gunter, “Defeasible Security Policy Composition for Web Services,” Proc. ACM Workshop Formal Methods in Security Eng. (FMSE '06), M. Winslett, A.D. Gordon, D. Sands, eds., pp. 45-54, 2006.
[6] G. Bruns, D.S. Dantas, and M. Huth, “A Simple and Expressive Semantic Framework for Policy Composition in Access Control,” Proc. ACM Workshop Formal Methods in Security Eng. (FMSE '07), pp. 12-21, 2007.
[7] D.J. Dougherty, C. Kirchner, H. Kirchner, and A. Santana de Oliveira, “Modular Access Control via Strategic Rewriting,” Proc. 12th European Symp. Research in Computer Security (ESORICS '07), Sept. 2007.
[8] A. Santana de Oliveira, “Rewriting-Based Access Control Policies,” Electronic Notes in Theoretical Computer Science, vol. 171, no. 4, pp. 59-72, 2007.
[9] C. Kirchner, F. Kirchner, and H. Kirchner, “Strategic Computations and Deductions,” Studies in Logic and the Foundations of Math. Festchrift in Honor of Peter Andrews, 2008.
[10] A. Santana de Oliveira, “Réécriture et Modularité pour les Politiques de Sécurité,” PhD thesis, Univ. Henri Poincaré, Nancy 1, 2008.
[11] B. Shafiq, A. Masood, J. Joshi, and A. Ghafoor, “A Role-Based Access Control Policy Verification Framework for Real-Time Systems,” Proc. 10th IEEE Int'l Workshop Object-Oriented Real-Time Dependable Systems, 2005.
[12] K.H. Mortensen, “Automatic Code Generation Method Based on Coloured Petri Net Models Applied on an Access Control System,” Application and Theory of Petri Nets, pp. 367-386, Springer-Verlag, 2000.
[13] K. Knorr, “Dynamic Access Control through Petri Net Workflows,” Proc. 16th Ann. Conf. Computer Security Applications, pp. 159-167, 2000.
[14] Z.L. Zhang, F. Hong, and J.G. Liao, “Modeling Chinese Wall Policy Using Colored Petri Nets,” Proc. Sixth IEEE Int'l Conf. Computer and Information Technology, 2006.
[15] Z.L. Zhang, F. Hong, and H. Xiao, “Verification of Strict Integrity Policy via Petri Nets,” Proc. Int'l Conf. Systems and Networks Comm., 2006.
[16] K. Juszczyszyn, “Verifying Enterprise's Mandatory Access Control Policies with Coloured Petri Nets,” Proc. 12th IEEE Int'l Workshops Enabling Technologies: Infrastructure for Collaborative Enterprises, 2003.
[17] R. Laborde, B. Nasser, F. Grasset, F. Barrère, and A. Benzekri, “A Formal Approach for the Evaluation of Network Security Mechanisms Based on RBAC Policies,” Electronic Notes in Theoretical Computer Science, vol. 121, pp. 117-142, 2005.
[18] B. Shafiq, J.B.D. Joshi, and A. Ghafoor, “Petri-Net Based Modeling for Verification of RBAC Policies,” technical report, Center for Education and Research in Information Assurance and Security, 2002.
[19] Y. Deng, J.C. Wang, J. Tsai, and K. Beznosov, “An Approach for Modeling and Analysis of Security System Architectures,” IEEE Trans. Knowledge and Data Eng., vol. 15, no. 5, pp. 1099-1119, Sept. 2003.
[20] M. McDougall, R. Alur, and C.A. Gunter, “A Model-Based Approach to Integrating Security Policies for Embedded Devices,” Proc. Fourth ACM Int'l Conf. Embedded Software, pp. 211-219, 2004.
[21] J. Joshi and A. Ghafoor, “A Petri-Net Based Multilevel Security Specification Model for Multimedia Documents,” technical report, Center for Education and Research in Information Assurance and Security, 2000.
[22] T. Murata, “Petri Nets: Properties, Analysis, and Applications,” Proc. IEEE, vol. 77, no. 4, pp. 541-580, Apr. 1985.
[23] K. Jensen, Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, vol. 1, Springer Verlag, 1997.
[24] K. Jensen, “Coloured Petri Nets: A High Level Language for System Design and Analysis,” Advances in Petri Nets 1990, G. Rozenberg, ed., Springer-Verlag, 1991.
[25] M.C. Tschantz and S. Krishnamurthi, “Towards Reasonability Properties for Access-Control Policy Languages,” Proc. 11th ACM Symp. Access Control Models and Technologies (SACMAT), D.F. Ferraiolo and I. Ray, eds., pp. 160-169, 2006.
[26] S. Barker and M. Fernández, “Term Rewriting for Access Control,” Data and Applications Security, pp. 179-193, Springer, 2006.
[27] F. Tiplea, T. Jucan, and C. Masalagiu, “Term Rewriting Systems and Petri Nets,” Analele Stiintifice ale Univ. Al. I. Cuza, vol. 34, no. 4, pp. 305-317, 1988.
[28] R. Verma, M. Rusinowitch, and D. Lugiez, “Algorithms and Reductions for Rewriting Problems,” Fundamental Informatics, vol. 46, no. 3, pp. 257-276, 2001.
[29] I. Leahu and F. Tiplea, “The Confluence Property for Petri Nets and Its Applications,” Proc. Eighth Int'l Symp. Symbolic and Numeric Algorithms for Scientific Computing, 2006.
[30] R. Melinte, O. Oanea, I. Olga, and F. Tiplea, “The Home Marking Problem and Some Related Concepts,” Acta Cybernetica, vol. 15, no. 3, pp. 467-478, 2002.
[31] S. Jajodia, P. Samarati, M.L. Sapino, and V.S. Subrahmanian, “Flexible Support for Multiple Access Control Policies,” ACM Trans. Database Syst., vol. 26, no. 2, pp. 214-260, 2001.
[32] A.A. El Kalam, S. Benferhat, A. Miege, R. El Baida, F. Cuppens, C. Saurel, P. Balbiani, Y. Deswarte, and G. Trouessin, “Organization Based Access Control,” Proc. Fourth IEEE Int'l Workshop Policies for Distributed Systems and Networks (POLICY '03), pp. 120-131, 2003.
[33] T. Moses, “eXtensible Access Control Markup Language (XACML) Version 2.0,” technical report, Organization for the Advancement of Structured Information Standards, Feb. 2005.

Index Terms:
Security policy, colored Petri net, specification and verification, property preservation.
Hejiao Huang, Hélène Kirchner, "Formal Specification and Verification of Modular Security Policy Based on Colored Petri Nets," IEEE Transactions on Dependable and Secure Computing, vol. 8, no. 6, pp. 852-865, Nov.-Dec. 2011, doi:10.1109/TDSC.2010.43
Usage of this product signifies your acceptance of the Terms of Use.