TELECOM & Management SudParis
The authors address the issue of formally validating the deployment of access control security policies. They show how the use of a formal expression of the security requirements, related to a given system, ensures the deployment of an anomaly free abstract security policy. They also describe how to develop appropriate algorithms by using a theorem proving approach with a modeling language allowing the specification of the system, of the link between the system and the policy, and of certain target security properties. The result is a set of proved algorithms that constitute the certified technique for a reliable security policy deployment.