Implementing a calculus for distributed access control in higher order logic and HOL

Access control - determining which requests for services should be honored or not - is particularly difficult in networked systems. Assuring that access-control decisions are made correctly involves determining 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 between bank clients and client banking accounts. The CORBA (Common Object Request Broker Architecture) CSIv2 (Common Secure Interoperability 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 interpretations that lead to consistent and appropriate access-control decisions across potentially differing operating systems and hardware platforms. 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 thinking and a theorem prover to verify our results. We use a logic for authentication 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.