Timed secure colored Petri net based analysis of information flow

We present in this paper a novel framework named Timed Secure Colored Petri Net (Tscpn) to carry out security verification in a formal and systematic manner,Tscpn is a security policy model to both express time constraints on information (availability) and specify a wide range of information flow security requirements (through multilevel security policies such as Bell-LaPadula) in a decentralized way. We also propose a suitable analysis method to verify security properties by constructing and examining the state space of the constructed model. However as timed models are generally infinite, applying this method must pass by contracting its state space into a finite graph (state class graph) preserving properties of interest. According to this graph, it is possible to verify confidentiality and integrity, enforce control on information flow security, specify temporal access control and information availability. By using this formal method, many security drawbacks can be eliminated in advance during the system design.