One of the most important and integral components of modern computer security are access control systems. The objective of an access control system (ACS) is often described in terms of protecting system resources against inappropriate or unwanted user access. However, a large degree of sharing can interfere with the protection of resources, so a sufficiently detailed AC policy should allow selective exchange of information when, in its absence, sharing can be considered too risky in general. Erroneous configurations, faulty policies, as well as flaws in the implementation of software can lead to global insecurity. Identifying the differences between policy specifications and their intended functions is crucial because the correct implementation and enforcement of the policies of a particular application is based on the premise that the specifications of this policy are correct. As a result of the policy, the specifications presented by the models must undergo rigorous validation and legalization through systematic checks and tests to ensure that the specifications of the policies really correspond to the wishes of the creators. Verifying that access control policies and models are consistent is not a trivial and critical task. And one of the important aspects of such a check is a formal check for inconsistency and incompleteness of the model, and the security requirements of the policy, because the access control model and its implementation do not necessarily express policies that can also be hidden, embedded by mixing with direct access restrictions or another access control model.