A logical reconstruction of SPKI

TL;DR

This paper provides a formal logical framework for SPKI/SDSI, extending previous work on SDSI's local name logic to include features like revocation and expiry, clarifying the semantics and rules of SPKI.

Contribution

It extends the Logic of Local Name Containment to model SPKI features such as revocation and expiry without added complexity, and analyzes SPKI's tuple reduction rules.

Findings

The extended logic captures SPKI features effectively.

SPKI's tuple reduction rules require additional rules for completeness.

Revocation and expiry can be modeled without nonmonotonic logic.

Abstract

SPKI/SDSI is a proposed public key infrastructure standard that incorporates the SDSI public key infrastructure. SDSI's key innovation was the use of local names. We previously introduced a Logic of Local Name Containment that has a clear semantics and was shown to completely characterize SDSI name resolution. Here we show how our earlier approach can be extended to deal with a number of key features of SPKI, including revocation, expiry dates, and tuple reduction. We show that these extensions add relatively little complexity to the logic. In particular, we do not need a nonmonotonic logic to capture revocation. We then use our semantics to examine SPKI's tuple reduction rules. Our analysis highlights places where SPKI's informal description of tuple reduction is somewhat vague, and shows that extra reduction rules are necessary in order to capture general information about binding and authorization.