Implementing a Calculus for Distributed Access Control in Higher Order Logic and HOL

  • Thumrongsak Kosiyatrakul
  • Susan Older
  • Polar Humenn
  • Shiu-Kai Chin
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2776)


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.


Modal Logic Theorem Prover Logical Rule Kripke Model Banking Server 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Object Management Group: CORBAServices: Common Object Services. no formal/98-07-05 (July 1998), Available via
  2. 2.
    Object Management Group: The Common Secure Interoperability Version 2, no ptc/01-06-17 (June 2001), Available via
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York (1993)zbMATHGoogle Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge (1997)Google Scholar
  7. 7.
    Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)zbMATHGoogle Scholar
  8. 8.
    Wobber, E., Abadi, M., Burrows, M., Lampson, B.: Authentication in the Taos Operating System. ACM Transactions on Computer Systems 12(1), 3–32 (1994)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Thumrongsak Kosiyatrakul
    • 1
  • Susan Older
    • 1
  • Polar Humenn
    • 1
  • Shiu-Kai Chin
    • 1
  1. 1.Department of Electrical Engineering and Computer Science & Systems Assurance InstituteSyracuse UniversitySyracuseUSA

Personalised recommendations