Modeling of Access Control System in Event-B - Hussain, S.; Farid, S.; Alam, M.; Iqbal, S.; Ahmad, S. (The Nucleus, 2018)
Computer security is a major challenge in the current era of ubiquitous computing and the Internet. The external security measures are good but not enough to secure software systems. That is why the internal security of software systems is of much importance and more emphasis needs to be given to describe internal design of software systems. Access control system is a mechanism to ensure the internal security of software systems. There are various access control systems which are claimed to provide a secure way to access the resources but in reality these systems have many loopholes and drawbacks. Authentication and authorization are the major key elements of access control systems. Authentication is a mechanism to verify unique identification of a user in the system, and authorization is to grant access to a user to system resources. In this paper, a new generic and simplified model of access control any system is proposed which is based on formal methods. The formal method used in this access control system is Event-B. Event-B is a formal specification and modeling language based on set theory and first order logic. Authentication process ensures that which type of users are allowed to access the system. In authorization mechanism it is ensured that a user is granted access to a system resource only if he/she has access rights for that particular resource. The resulting formal models are analyzed and verified by using RODIN tools.