Access control allows one to specify a part of the security Policy of an IS (information system). An AC (access control) policy defines which conditions must old for someone to have access to something. Main concepts used in AC are: permissions, prohibitions, obligations and SoD (separation of duty). Permissions allow someone to access to some resources. On the opposite, prohibitions forbid users to have access to some resources. Obligations link at least two actions: when a user performs an action, he must perform another one. SoD secures an action by dividing it in different tasks, and entrusting the execution of these tasks to different users. Many AC policies modelling methods already exist. The main particularities of the EB3Sec methods are:- All AC concepts can be expressed in a unique model,- This modelling method is event-based. No existing AC modelling methods presents these two characteristics. We define a set of patterns; each pattern corresponds to a specific AC constraint. An EB3Sec model can be used for different purposes:- Simulation and verification,- Implementation.Verifying a model consists in checking that the model complies with some properties that we have defined. Mainly, blocking must be detected. Blocking corresponds to a step of execution where no action can be executed or to situations where an action cannot be performed anymore. Current model checking methods cannot be used to check properties on dynamic AC constraints. Thus, model-checking techniques are combined to simulation techniques. Once a model is verified, it can be transformed in an implementation. To implement an EB3Sec model two ways can be considered: the EB3Sec model can be translated into an other language, such as XACML, which possesses a mature implementation, or a security kernel using EB3Sec as input language can be implemented
