Formal verification of Access Control

Access control is an approach to protecting the confidential information from the illegal accesses in a variety of information systems.
However, model vulnerability and insufficient access control specification might be cause illegal access to information.
To prevent this issue, validate model and access control specification with formal approach. If found error in verification process, show counter example. As a result, System administrators can refer it for evolution.