Validation of a Security Policy by the Test of Its Formal B Specification -- A Case Study

This paper discusses the use of test and animation techniques to validate an access control policy, expressed in Secure UML. It reports on a case study of secure medical information system, where the Secure UML model expresses both functional and security models of the information system. It is translated into a specification in the B language. The case study takes advantage of animation tools associated to the B language to validate the functional model, to perform systematic test of permission rules and to investigate potential insiders attacks.