Abstract
Access control – determining which requests for services sho-uld 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.
Partially supported by the New York State Center for Advanced Technology in Computer Applications and Software Engineering (CASE).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Object Management Group: CORBAServices: Common Object Services. no formal/98-07-05 (July 1998), Available via http://www.omg.org/cgi-bin/doc?formal/98-07-05
Object Management Group: The Common Secure Interoperability Version 2, no ptc/01-06-17 (June 2001), Available via http://www.omg.org/cgi-bin/doc?ptc/01-06-17
Abadi, M., Burrows, M., Lampson, B., Plotkin, G.: Access Control in Distributed Systems. ACM Transactions on Programming Languages and Systems 15(4), 706–734 (1993)
Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York (1993)
Lampson, B., Abadi, M., Burrows, M., Wobber, E.: Authentication in Distributed Systems: Theory and Practice. ACM Transactions on Computer Systems 10(4), 265–310 (1992)
Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge (1997)
Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)
Wobber, E., Abadi, M., Burrows, M., Lampson, B.: Authentication in the Taos Operating System. ACM Transactions on Computer Systems 12(1), 3–32 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kosiyatrakul, T., Older, S., Humenn, P., Chin, SK. (2003). Implementing a Calculus for Distributed Access Control in Higher Order Logic and HOL. In: Gorodetsky, V., Popyack, L., Skormin, V. (eds) Computer Network Security. MMM-ACNS 2003. Lecture Notes in Computer Science, vol 2776. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45215-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-45215-7_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40797-3
Online ISBN: 978-3-540-45215-7
eBook Packages: Springer Book Archive