Verifying enterprise´s mandatory access control policies with coloured Petri nets

The paper addresses important problems met when implementing mandatory access control policies in complex distributed systems (e.g. enterprise networks). The role of formal security models is also presented and the properties of the model suitable for systems under consideration are defined. Then a formal security model, Secure Coloured Petri - using coloured Petri net´s semantics - is proposed. It is shown how the enterprise security management system may take advantage of the proposed model´s properties. Application of coloured Petri nets analysis and construction methods to information flow security analysis is also proposed and discussed.