Information Technology Reference
In-Depth Information
Implementing a Calculus for Distributed Access
Control in Higher Order Logic and HOL
Thumrongsak Kosiyatrakul, Susan Older, Polar Humenn, and Shiu-Kai Chin
Department of Electrical Engineering and Computer Science & Systems Assurance
Institute, Syracuse University, Syracuse, New York 13244, USA
Abstract.
Access control - determining which requests for services sho-
uld be honored or not - is particularly dicult in networked systems.
Assuring that access-control decisions are made correctly involves deter-
mining identities, privileges, and delegations. The basis for making such
decisions often relies upon cryptographically signed statements that are
evaluated within the context of an access-control policy.
An important class of access-control decisions involves
brokered services
,
in which intermediaries (brokers) act on and make requests on behalf
of their clients. Stock brokers are human examples; electronic examples
include the web servers used by banks to provide the online interface be-
tween bank clients and client banking accounts. The CORBA (Common
Object Request Broker Architecture) CSIv2 (Common Secure Interop-
erability version 2) protocol is an internationally accepted standard for
secure brokered services [2]. Its purpose is to ensure service requests,
credentials, and access-control policies have common and consistent in-
terpretations that lead to consistent and appropriate access-control de-
cisions across potentially differing operating systems and hardware plat-
forms. Showing that protocols such as CSIv2 fulfill their purpose requires
reasoning about identities, statements, delegations, authorizations, and
policies and their interactions.
To meet this challenge, we wanted to use formal logic to guide our think-
ing and a theorem prover to verify our results. We use a logic for au-
thentication and access control [5,3,8] that supports reasoning about the
principals in a system, the statements they make, their delegations, and
their privileges. To
assure
our reasoning is correct, we have implemented
this logic as a definitional extension to the HOL theorem prover [4].
We describe this logic, its implementation in HOL, and the application
of this logic to brokered requests in the context of the CORBA CSIv2
standard.
1
Introduction
The rapid growth of wired and wireless networks has resulted in distributed com-
puting on a global scale where services are available anywhere at anytime. While
global access to information and services offers great convenience, it also carries
Partially supported by the New York State Center for Advanced Technology in
Computer Applications and Software Engineering (CASE).
