The objective of this paper is to assist the security administrators, in their attempt to specify, define and formalize security policies suited to a given high risk environment. It is then possible for the administrators to automatically derive consequences of these policies. In particular we want to provide users with the following functionalities: query a given security policy; verify that properties such as consistency and completeness are enforced by a given policy; verify that a given situation does not violate the security policy; investigate interoperability problems between several security policies. In this paper we more precisely focus on the problem of security policies formulization. We want to get a generic approach, being as much domain-independent as possible. In order to achieve the above goals, we have chosen a logic-based approach. It combines a deontic logic to model the concept of permission, obligation and prohibition with a modal logic of action. It also includes the possibility to deal with additional concepts such as role, responsibility and delegation. We illustrate this approach through a case study: a regulation whose purpose is to define means to protect secret data related to the National Defense.