A metamodel of the B modeling of access-control policies: Work in progress

Abstract

Verification and validation of access-control policies for information systems is a difficult yet necessary task. In order to take advantage of the formal properties and tools of the B method, we introduce in this paper a metamodel of the B modeling of access control policies. This metamodel lead to the development of a formal prototype of an access control filter combined to the system. It allows verification and validation of policies before implementation. © 2012 Springer-Verlag.