A logic for SDSI's Linked Local Name Spaces 
    (Preliminary  Version) 

    J. Y. Halpern and R. van der Meyden 

    to appear, IEEE Computer Security Foundations Workshop, June 1999 


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.