A Logic for SDSI's Linked Local Name Spaces

TL;DR

This paper introduces the Logic of Local Name Containment, a formal framework that accurately models SDSI's name resolution, offering clear semantics, a complete axiomatization, and efficient implementation methods.

Contribution

It presents a new logic that precisely captures SDSI's name resolution, addressing previous semantics issues and enabling efficient query processing.

Findings

Provides a clear semantics for SDSI local names

Offers a tight characterization of SDSI name resolution

Enables efficient implementation of local name queries

Abstract

Abadi has introduced a logic to explicate the meaning of local names in SDSI, the Simple Distributed Security Infrastructure proposed by Rivest and Lampson. Abadi's logic does not correspond precisely to SDSI, however; it draws conclusions about local names that do not follow from SDSI's name resolution algorithm. Moreover, its semantics is somewhat unintuitive. This paper presents the Logic of Local Name Containment, which does not suffer from these deficiencies. It has a clear semantics and provides a tight characterization of SDSI name resolution. The semantics is shown to be closely related to that of logic programs, leading to an approach to the efficient implementation of queries concerning local names. A complete axiomatization of the logic is also provided.