Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
9655982 | Electronic Notes in Theoretical Computer Science | 2005 | 26 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
R. Laborde, B. Nasser, F. Grasset, F. Barrère, A. Benzekri,