Model Checking SPKI/SDSI
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.
(Click here to access the paper:
PDF.)
University of Wisconsin