Assuring consistency in mixed models

摘要

Information systems security defines three properties of information: confidentiality, integrity, and availability. These characteristics remain major concerns throughout the commercial and military industry. Ordinary users have taken these features as basis for their businesses. Furthermore, users may find it necessary to combine policies in order to protect their information in a suitable way. However, inconsistencies may arise as a result of implementing multiple secrecy and privacy models; and therefore, render these services unsecure. In this paper, we propose an approach to detect and report inconsistencies when choosing mixed models for integrity and security. It is based on specifying the policies in first order logic and applying formal analysis. We demonstrate the feasibility of our proposition by applying it to the Clark Wilson and role based access control models. We use the Alloy language and analyzer to formalize the mixed model and check for any inconsistencies.