A modal logic for role-based access control

Thumrongsak Kosiyatrakul, Susan Older, Shiu Kai Chin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations

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 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.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages179-193
Number of pages15
DOIs
StatePublished - Dec 1 2005
Event3rd International Workshop on Mathematical Methods, Models, and Architectures for Computer Network Security, MMM-ACNS 2005 - St. Petersburg, Russian Federation
Duration: Sep 24 2005Sep 28 2005

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3685 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other3rd International Workshop on Mathematical Methods, Models, and Architectures for Computer Network Security, MMM-ACNS 2005
CountryRussian Federation
CitySt. Petersburg
Period9/24/059/28/05

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A modal logic for role-based access control'. Together they form a unique fingerprint.

Cite this