A Modal Logic for Role-Based Access Control

@incollection{citeulike:1912526, abstract = {Making correct access-control decisions is central to security, which in turn requires accounting correctly for the identity, credentials, roles, authority, and privileges of users and their agents. In networked systems, these decisions are made more complex because of delegation and differing access-control policies. Methods for reasoning rigorously about access control and computer-assisted reasoning tools for verification are effective for providing assurances of security. In this paper we extend the access-control logic of [11,1] to also support reasoning about role-based access control (RBAC), which is a popular technique for reducing the complexity of assigning privileges to users. The result is an access-control logic which is simple enough for design and verification engineers to use to assure the correctness of systems with access-control requirements but yet powerful enough to reason about delegations, credentials, and trusted authorities. We explain how to describe RBAC components such as user assignments, permission assignments, role inheritance, role activations, and users’ requests. The logic and its extensions are proved to be sound and implemented in the HOL (Higher Order Logic version 4) theorem prover. We also provide formal support for RBAC’s static separation of duty and dynamic separation of duty constraints in the HOL theorem prover. As a result, HOL can be used to verify properties of RBAC access-control policies, credentials, authority, and delegations.}, author = {Kosiyatrakul, Thumrongsak and Older, Susan and Chin, Shiu-Kai }, citeulike-article-id = {1912526}, doi = {http://dx.doi.org/10.1007/11560326\_14}, journal = {Computer Network Security}, keywords = {inference, rbac}, pages = {179--193}, posted-at = {2007-11-14 06:56:00}, priority = {2}, title = {A Modal Logic for Role-Based Access Control}, url = {http://dx.doi.org/10.1007/11560326\_14}, year = {2005} }

TY - CHAP ID - citeulike:1912526 L3 - citeulike-article-id:1912526 N2 - Making correct access-control decisions is central to security, which in turn requires accounting correctly for the identity, credentials, roles, authority, and privileges of users and their agents. In networked systems, these decisions are made more complex because of delegation and differing access-control policies. Methods for reasoning rigorously about access control and computer-assisted reasoning tools for verification are effective for providing assurances of security. In this paper we extend the access-control logic of [11,1] to also support reasoning about role-based access control (RBAC), which is a popular technique for reducing the complexity of assigning privileges to users. The result is an access-control logic which is simple enough for design and verification engineers to use to assure the correctness of systems with access-control requirements but yet powerful enough to reason about delegations, credentials, and trusted authorities. We explain how to describe RBAC components such as user assignments, permission assignments, role inheritance, role activations, and users’ requests. The logic and its extensions are proved to be sound and implemented in the HOL (Higher Order Logic version 4) theorem prover. We also provide formal support for RBAC’s static separation of duty and dynamic separation of duty constraints in the HOL theorem prover. As a result, HOL can be used to verify properties of RBAC access-control policies, credentials, authority, and delegations. JF - Computer Network Security EP - 193 TI - A Modal Logic for Role-Based Access Control SP - 179 KW - inference KW - rbac AU - Kosiyatrakul, Thumrongsak AU - Older, Susan AU - Chin, Shiu-Kai PY - 2005/// UR - http://dx.doi.org/10.1007/11560326_14 ER -