Several secrecy models are known in practice, and governance requirements may make it necessary to combine them in order to implement the secrecy policies of an enterprise. However, inconsistencies may arise as a result of implementing multiple secrecy models in an enterprise network, and these inconsistencies may well undermine the intended functioning of the system. We propose a method to detect and report these inconsistencies at the time when the secrecy system is designed. The method is based on specifying the models and their secrecy policies in logic and applying a formal analyzer. A given combination of such models can be analysed for inconsistency, and if found inconsistent this combination of models must be modified before implementation. Our proposed method is demonstrated by using as example a mixed model involving Bell-La Padula (BLP) and Role based access control (RBAC) in addition to separation of concerns (SOC). The logic analyzer Alloy is used to check consistency. The method's principles are conjectured to be generic and hence can apply to any secrecy model.

Keywords: Governance, secrecy models, consistency, formal methods, Alloy.