A Formal Approach for the Evaluation of Network Security Mechanisms Based on RBAC Policies

Security policy models allow reasoning about security goals achievements. When security mechanisms are implemented, it is difficult to formally validate the security properties against the security goals especially in a network environment. To assess the implemented security properties, one should consider details regarding the network topology, the forwarding as well as filtering and transform engines. In this paper, we present a Colored Petri Net based tool which allows to describe graphically a given network topology, the network security mechanisms and the security goals required. The tool computes the different functionalities to set up the security properties and formally validates the solution using the dead state of the generated reachability graph analysis. Different security properties such as confidentiality and availability can be studied.