SPKI/SDSI is a language for expressing distributed access control policy, derived from SPKI and SDSI. We provide a first-order
logic (FOL) semantics for SDSI, and show that it has several advantages over previous semantics. For example, the FOL semantics
is easily extended to additional policy concepts and gives meaning to a larger class of access control and other policy analysis
queries. We prove that the FOL semantics is equivalent to the string rewriting semantics used by SDSI designers, for all queries
associated with the rewriting semantics. We also provide a FOL semantics for SPKI/SDSI and use it to analyze the design of
SPKI/SDSI. This reveals some problems. For example, the standard proof procedure in RFC 2693 is semantically incomplete. In
addition, as noted before by other authors, authorization tags in SPKI/SDSI are algorithmically problematic, making a complete
proof procedure unlikely. We compare SPKI/SDSI with
RT
1
C
, which is a language in the
RTRole-based Trust-management framework that can be viewed as an extension of SDSI. The constraint feature of
RT
1
C
, based on Constraint Datalog, provides an alternative mechanism that is expressively similar to SPKI/SDSI tags, semantically
natural, and algorithmically tractable.
Keywords SPKT - SDSI - Trust - management - Logic - Logic programs - Language
Preliminary version of this paper appeared in Proceedings of the 16th IEEE Computer Security Foundations Workshop, July 2003. Most of this work was performed while the first author was a research associate at the Department of Computer
Science, Stanford University in Stanford, CA 94305.