Safety analysis is a fundamental problem in authorization models. Safety decidable models provide theoretical foundations for decentralized security administration. Attributes of objects are central to usage control authorization models. It… Click to show full abstract
Safety analysis is a fundamental problem in authorization models. Safety decidable models provide theoretical foundations for decentralized security administration. Attributes of objects are central to usage control authorization models. It has previously been shown that inclusion of a single infinite attribute leads to undecidable safety, even without any creation of objects. Therefore unrestricted inclusion of infinite attributes is not possible in a safety decidable model. On the other hand, it has recently been shown that the safety problem for the pre-authorization usage control sub-model with finite attribute domains, called ${PreUCON_A^{finite}}$PreUCONAfinite, is decidable even with unbounded object creation. A major limitation of finite attributes is the inability to link objects through attribute values in presence of unbounded object creation (since attributes that reference other objects must be infinite in this case). It would be desirable to have safety-decidable attribute-based models which include both finite and infinite attributes (necessarily with some restrictions). This paper develops a pre-authorization usage control sub-model, called ${PreUCON}_A^{id}$PreUCONAid, with attribute domains solely comprised of infinite object identifiers with considerable restrictions on how these attributes can be updated. Safety decidability for ${PreUCON}_A^{id}$PreUCONAid is proved by defining the notion of $\omega$ω-equivalent usage configurations, and showing that the reachable set of $\omega$ω-equivalent usage configurations is computable and can be used to answer safety questions. The utility of such models in practice is illustrated by means of an example. The paper further shows that addition of even a single finite domain attribute to ${PreUCON}_A^{id}$PreUCONAid results in undecidable safety. These results indicate that combining finite and infinite attributes in a safety decidable model is a challenging task, which will likely require carefully crafted restrictions on updates to these attributes. The formulation of such a model remains an important open question.
