Modeling of Access Control System in Event-B

S. Hussain, S. Farid, M. Alam, S. Iqbal, S. Ahmad


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.

Full Text:



D.D. Clark and D.R. Wilson, “A comparison of commercial and military computer security policies”, IEEE Symposium on Security and Privacy, pp. 184–184, 1987.

S. Hussain, P. Dunne and G. Rasool, “Formal Specification of Security Properties using Z Notation”, Research Journal of Applied Sciences, Engineering and Technology, vol. 5, no. 19, pp. 4664–4670, 2013. [3] S. Hussain, G. Rasool, M. Atef and A.K. Shahid, “A review of approaches to model security into software systems”, Journal of Basic and Applied Scientific Research, vol. 3, no. 4, pp. 642–647, 2013.

S. Hussain, G. Rasool, M. Atef and A.K. Shahid, “FDMSWAP: Formal Development Methodology for Secure Web Applications”, Journal of Basic and Applied Scientific Research, vol. 3, no. 4, pp. 1123-1128, 2013. [5] T.S. Hoang, D. Basin and J.-R. Abrial, “Specifying access control in Event-B”, Technical Report, vol. 624, 2009.

D. Gollmann, “Computer Security”, Wiley Interdisciplinary Reviews: Computational Statistics, vol. 2, no.5, pp. 544-554, 2010. [7] J. Barkley, K. Beznosov and J. Uppal, “Supporting relationships in access control using role based access control”, Proceedings of the fourth ACM workshop on Role-based access control, pp. 55–65, 1999. [8] E.C. Cheng, “An object-oriented organizational model to support dynamic role-based access control in electronic commerce”, Decision Support Systems, vol. 29, no. 4, pp. 357–369, 2000. [9] J.R. Abrial, Modeling in Event-B: System and Software Development, Cambridge University Press, 2010. [10] J.R. Abrial, “Formal methods: Theory becoming practice”, J. UCS, vol. 13, no. 5, pp. 619–628, 2007. [11] M.A. Harrison, W.L. Ruzzo and J.D. Ullman, “Protection in operating systems”, Communications of the ACM, vol. 19 no. 8, pp. 461-471, 1976. [12] S.I. Gavrila and J.F Barkley, “Formal specification for role based access control user/role and role/role relationship management”, Proceedings of the third ACM workshop on Role-based access control, October 1998, pp. 81-90. [13] E. Bertino, P.A Bonatti and E. Ferrari, “TRBAC: A temporal role-based access control model”, ACM Transactions on Information and System Security (TISSEC), vol. 4, no. 3, pp.191-233, 2001. [14] R. Sandhu, D. Ferraiolo and R. Kuhn, “The NIST model for role-based access control: Towards a unified standard”, ACM Workshop on Role-based Access Control, pp. 1-11, July 2000. [15] D.E. Bell and L.J. LaPadula, “Secure computer systems: Mathematical foundations”, Mitre Corp Bedford MA, vol. 1, no. MTR-2547, 1973. [16] K.J. Biba, “Integrity considerations for secure computer systems”, Mitre Corp Bedford MA, vol. 1, no. MTR-3153, 1977.

S. Hussain et al. / The Nucleus 55, No. 2 (2018) 74-84

M.A. Bishop, “The art and science of computer security, Addison-Wesley Longman Publishing Co., Inc., 2002. [18] A. Belapurkar, A. Chakrabarti, H. Ponnapalli, N. Varadarajan, S. Padmanabhuni and S. Sundarrajan, “Distributed systems security: issues, processes and solutions”, John Wiley & Sons, 2009. [19] R. Baskerville, and M. Siponen, “An information security meta-policy for emergent organizations”, Logistics Information Management, vol. 15, no. 5/6, pp. 337-346, 2002. [20] J. Rees, S. Bandyopadhyay and E.H. Spafford, “PFIRES: A policy framework for information security”, Communications of the ACM, vol. 46, no 7, pp.101-106, 2003. [21] C.W. Probst, R.R. Hansen and F. Nielson, “Where can an insider attack?”, Proc. of International Workshop on Formal Aspects in Security and Trust, Heidelberg, Berlin: Springer, , pp.127-142, 2004. [22] M. Abrams, and D. Bailey, “Abstraction and refinement of layered security policy”, Information Security: An Integrated Collection of Essays, pp.126-136, 19995. [23] I.M. Olson and M.D. Abrams, “Information security policy”, Information Security: An Integrated Collection of Essays, 1995. [24] D. Pavlovic and D.R. Smith, 2003. “Software development by refinement”, Formal Methods at the Crossroads from Panacea to Foundational Support, Heidelberg, Berlin: Springer, 2003, pp. 267-286. [25] D. Sannella and A. Tarlecki, “Foundations of algebraic specification and formal software development”, Springer Science & Business Media, 2012. [26] W. Pieters, T. Dimkov and D. Pavlovic, “Security policy alignment: A formal approach”, IEEE Systems Journal, vol. 7, no. 2, pp.275-287, 2013. [27] S. Fugkeaw, P. Manpanpanich and S. Juntapremjitt, “A hybrid multi-application authentication and authorization model using multi-agent system and PKI”, Proc. of the Fourth IASTED Asian Conference on Communication Systems and Networks, ACTA Press, pp. 96-101, March 2007. [28] J. Li, and D. Cordes, “A scalable authorization approach for the Globus grid system”, Future Generation Computer Systems, vol. 21, no. 2, pp. 291-301, 2005. [29] E. Palomar, J.M. Estevez-Tapiador, J.C. Hernandez-Castro and A. Ribagorda, “Certificate-based access control in pure p2p networks”, Sixth IEEE International Conference on Peer-to-Peer Computing, pp. 177-184, 2006. [30] O. Cánovas, A.F. Gómez-Skarmeta, G. López and M. Sánchez, “Deploying authorization mechanisms for federated services in eduroam (DAMe)”, Internet Research, vol. 17, no. 5, pp.479-494, 2007. [31] A. Gbadegesin, R. Batoukov and D.R. Reed, “Flexible scalable application authorization for cloud computing environments”, U.S. Patent 8,418,222, Microsoft Corporation, 2013. [32] J.A Calero, G.M. Perez and A.G. Skarmeta, “Towards an authorisation model for distributed systems based on the Semantic Web”, IET information security, vol. 4, no. 4, pp.411-421, 2010. [33] A. Moini, and A.M. Madni, “Leveraging biometrics for user authentication in online learning: A systems perspective”, IEEE Systems Journal, vol. 3 no, 4, pp. 469-476, 2009. [34] D. Arora, S. Ravi, A. Raghunathan and N.K. Jha, “Hardware-assisted run-time monitoring for secure program execution on embedded processors”, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol. 14, no. 12, pp. 1295-1308, 2006. [35] D.D. Hwang, P. Schaumont, K. Tiri and I. Verbauwhede, “Securing embedded systems”, IEEE Security & Privacy, vol. 4, no. 2, pp.40-49, 2006. [36] D. Mu, W. Hu, B. Mao and B. Ma, “A bottom-up approach to verifiable embedded system information flow security”, IET Information Security, vol. 8, no. 1, pp. 12-17, 2014. [37] M. Abadi and R. Needham, “Prudent engineering practice for cryptographic protocols”, IEEE transactions on Software Engineering, no. 1, pp. 6–15, 1996. [38] P. England, B. Lampson, J. Manferdelli and B. Willman, “A trusted open platform”, Computer, vol. 36, no. 7, pp. 55-62, 2003. [39] J.R. Abrial and S. Hallerstede, “Refinement, decomposition and instantiation of discrete models: Application to Event-B”, Fundamenta Informaticae, vol. 77, no, 1-2, pp. 1-28, 2007. [40] J.P. Bowen, K. Bogdanov, J.A. Clark, M. Harman, R.M. Hierons and P. Krause, 2002, August. “FORTEST: Formal methods and testing”, in Proc. of IEEE 26th Annual International of Computer Software and Applications Conference, pp. 91-101, August 2002. [41] J.R. Abrial, M. Butler, S. Hallerstede, T.S. Hoang, F. Mehta and L. Voisin, “Rodin: An open toolset for modelling and reasoning in Event-B”, Int. Journal on Software Tools for Technology Transfer, vol. 12, no. 6, pp. 447-466, 2010. [42] P. Bjesse, “What is formal verification?”, ACM SIGDA Newsletter, vol. 35, no. 24, p. 1, 2005. [43] L. Ma and J. J. Tsai, “Formal modeling and analysis of a secure mobile-agent system”, IEEE Transactions on Systems, Man and Cybernetics-Part A: Systems and Humans, vol. 38, no. 1, pp. 180–196, 2008. [44] J. Bendisposto, M. Jastram, M. Leuschel, C. Lochert, B. Scheuermann and I. Weigelt, “Validating Wireless Congestion Control and Realiability Protocols using ProB and Rodin”, Workshop on Formal Methods for Wireless Systems, August 2008. [45] N.A. Zafar, “Safety control management at airport taxiing to take-off procedure”, Arabian Journal for Science and Engineering, vol. 39, no. 8, pp. 6137-6148, 2014. [46] N.A. Zafar, “Formal Model of Aircrafts Safety Separation”, International Journal of Innovative Computing, Information and Control, vol. 10, no. 4, pp. 1401-1412, 2014.


  • There are currently no refbacks.