Una Lógica para los Espacios de Nombres Locales Vinculados de SDSI

Abadi ha introducido una lógica para explicar el significado de los nombres locales en SDSI, la Infraestructura de Seguridad Distribuida Sencilla propuesta por Rivest y Lampson. La lógica de Abadi no corresponde precisamente a SDSI; llega a conclusiones sobre los nombres locales que no se derivan del algoritmo de resolución de nombres de SDSI. Además, su semántica es algo no intuitiva. Este documento presenta la Lógica de Contención de Nombres Locales, que no sufre de estas deficiencias. Tiene una semántica clara y proporciona una caracterización precisa de la resolución de nombres de SDSI. Se demuestra que la semántica está estrechamente relacionada con la de los programas lógicos, lo que lleva a un enfoque para la implementación eficiente de consultas sobre nombres locales. También se proporciona una axiomatización completa de la lógica.