Analysis of SPKI/SDSI Certificates Using Model Checking
S. Jha and T. Reps
SPKI/SDSI is a framework for expressing naming and
authorization issues that arise in a distributed-computing
environment. In this paper, we establish a connection between
SPKI/SDSI and a formalism known as pushdown systems
(PDSs). We show that the SPKI/SDSI-to-PDS connection
provides a framework for formalizing a variety of
certificate-analysis problems. Moreover, the connection has
computational significance: Many analysis problems can
be solved efficiently (i.e., in time polynomial in the size
of the certificate set) using existing algorithms for model
checking pushdown systems.
Keywords: SPKI/SDSI, model checking, pushdown system,
naming, authorization, certificate-chain discovery,
certificate-set analysis.
(Click here to access the paper:
PostScript,
PDF.)
University of Wisconsin