Understanding SPKI/SDSI Using First-Order Logic

13 years 9 months ago
Understanding SPKI/SDSI Using First-Order Logic
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 RTC 1 , which is a language in the RT Role-based Trust-mana...
Ninghui Li, John C. Mitchell
Added 04 Jul 2010
Updated 04 Jul 2010
Type Conference
Year 2003
Where CSFW
Authors Ninghui Li, John C. Mitchell
Comments (0)