Modeling and Verification of Chinese Wall Policy Based on Petri Nets with Data

Abstract

Information security is an important issue in the design and development of information systems. As a well-known information security policy, Chinese Wall policy concerns the conflict of interest among sensitive information items. Since it is widely applied in many fields, it is important to explore the verification methods. Petri nets are a widely used formal method in the modeling and verification of information systems, and they are suitable for verifying Chinese Wall policy due to the capability of characterizing the concurrency. Particularly, some studies utilize colored Petri nets for modeling and verification of Chinese Wall policy. However, they do not characterize data operations including read, write and delete, which may affect the verification results. In this paper, we utilize Petri nets with data (PD-nets) to model and verify this policy. Specifically, we propose PD-nets for Chinese Wall policy to depict the control-flows, data-flows and data operations of information systems and introduce configurations and reachability graphs to describe the running states. We give theorems to prove the correctness of our method. Based on these theorems, we develop an algorithm to detect the violations of Chinese Wall policy. Furthermore, a case study is presented to show the effectiveness of our method, especially in modeling data operations and verifying their relevant CW policy.