Specification and Realization of Access Control in SPKI/SDSI

SACL is an access control language based on SPKI/SDSI PKI that has features like group certificates, delegation, threshold certificates etc. In this paper, we show how SACL can be effectively realized in a Security Automata framework. We establish the equivalence of the transformation with the SPKI/SDSI semantics as well as the set-theoretic semantics. The transformation gives an efficient way to enforce the policy being defined and allows inference of authorizations obtained from multiple certificates. Further, we describe algorithms for efficiently solving certificate-analysis problems, resource authentication problems etc. The transformation allows us to capture the authorization of tags while being delegated in an unambiguous way and, define the set of tags permissible under threshold certification. The framework succinctly captures the expressive power of SACL and enables heterogenous integration of SACL with state-based security mechanisms that are widely used for protection/security of classical OS, Databases etc. One of the distinct advantages of the framework is the amenability of using finite state model-checking algorithms for verifying access control. We shall show how very useful properties can be verified using our transformation.