Formalism of the Access Control Model Based on the Marqued Petri Nets

An access control system is a mandatory step in the implementation of security policy. The algebra of security introduced by McLean is not enough expressive to model an access control system. Several models appeared thereafter, namely the mandatory models and discretionary models. In this paper we will use the graphs of privileges and the Marked Petri Nets in order to model formally the access control system for the Unix/Linux systems. The access control model used will be the RBAC (Role-BasedAccess Control) model coupled with the SuperUser model of Unix/Linux.