Strict Integrity Policy is one of important security policies. In this paper, based on Petri net and Biba Model, the Petri net-based definitions of Strict Integrity Policy are formally described in detail. The Petri net-based definitions and the coverability graph allow one to analyze and verify Strict Integrity Policy in Petri net model of a system. Subsequently, an example of the integrity policy is illustrated and the conclusions show that Petri net is not only a concise graphic analysis method, but also suited to formal verification. This verification approach can efficiently improve the integrity policies during the system security design and implementation.
Citation:
Zhao-Li Zhang, Fan Hong, Hai-Jun Xiao, "Verification of Strict Integrity Policy via Petri Nets," icsnc, pp.23, International Conference on Systems and Networks Communication (ICSNC'06), 2006