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.
Akihiro Sakai, Yoshiaki Hori, Kouichi Sakurai, "Collision Detection of Access Control in Web Information Sharing System", Computer Security Symposium 2008, to appear (2008).
Akihiro Sakai, Naoyasu Ubayashi, Shin Nakajima, "Formal Verification of RBAC Descriptions and Evolution Assistant", 2008-SE-159, IPSJ Technical Report, March 2008.