Information Technology Reference
In-Depth Information
be provably secure. An implication of this last point is the need for a simple,
formal, and rigorous logic for reasoning about access control in a wide variety
of forms and situations. Such a logic could be used by designers to reason about
access-control decisions in ways that are analogous to how digital designers use
propositional logic to reason about digital designs. Our conclusion is that such
a logic is possible, based on our experience defining a modal logic capable of
specifying and reasoning about access-control policies and decisions that utilize
role-based access control (RBAC).
In our logic, user assignments, permission assignments, and role hierarchies
are defined within the access-control logic. In so doing, we have soundly united
in a single logic the ability to reason about privileges, authority, delegation,
credentials, and RBAC. We are currently extending the logic to support the
administration of RBAC roles with concepts such as administrative scope [14,3].
The requirement that engineers prove that their designs are correct and se-
cure necessitates the development of automated tools and verification methods.
To help meet this need, both the access-control logic and the consistency checks
for static and dynamic separation-of-duty constraints are defined as conservative
extensions to the logic of the Higher Order Logic (HOL) theorem prover [10].
The HOL extensions provide an executable implementation of the access-control
logic, and the inference rules have been verified to be sound. Likewise, verifi-
cation of static and dynamic separation-of-duty constraints of RBAC policies is
also done in HOL. While we do not anticipate that theorem provers such as HOL
will be routinely used by practicing engineers, the HOL definitions and theorems
are a rigorous and provably correct basis for computer-assisted reasoning tools
such as symbolic simulators, rewriting systems, and symbolic calculators. Such
tools are accessible and familiar to engineers and do not carry the same burden
of formal proof when compared to full-scale theorem proving systems such as
HOL.
References
1. Abadi, M., Burrows, M., Lampson, B., Plotkin, G.: A Calculus for Access Control in
Distributed Systems. ACM Transactions on Programming Languages and Systems,
15(4) (1993) 706-734
2. Cuppens, F., Demolombe, R.: A Modal Logical Framework for Security Policies.
Proceedings of the 10th International Symposium on Foundations of Intelligent
Systems, Lecture Notes in Computer Science, Vol.1325. Springer. (1997) 579-589
3. Cramton, J., Loizou, G.: Administrative Scope: A Foundation for Role-Based Ad-
ministrative Models. ACM Transactions on Information and System Security, 6(2)
(2003) 201-231
4. Ferraiolo, D.F., Barkley, J.F., Kuhn, D.R.: A Role-Based Access Control Model
and Reference Implementation Within a Corporate Intranet. ACM Transactions
on Information and System Security, 2(1) (1999) 34-64
5. Ferraiolo, D., Kuhn, R.: Role-Based Access Control. 15th NIST-NCSC National
Computer Security Conference, Gaithersburg, MD (1992) 554-563
