TY - GEN
T1 - A modal logic for role-based access control
AU - Kosiyatrakul, Thumrongsak
AU - Older, Susan
AU - Chin, Shiu Kai
PY - 2005
Y1 - 2005
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 accesscontrol 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.
AB - 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 accesscontrol 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.
UR - http://www.scopus.com/inward/record.url?scp=33646123997&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33646123997&partnerID=8YFLogxK
U2 - 10.1007/11560326_14
DO - 10.1007/11560326_14
M3 - Conference contribution
AN - SCOPUS:33646123997
SN - 354029113X
SN - 9783540291138
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 179
EP - 193
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
T2 - 3rd International Workshop on Mathematical Methods, Models, and Architectures for Computer Network Security, MMM-ACNS 2005
Y2 - 24 September 2005 through 28 September 2005
ER -