Analysis of SPKI/SDSI certificates using model checking
Somesh Jha and Thomas Reps.
In 15th IEEE Computer Security Fuondations Workshop (CSFW).
Cape Breton, Nova Scotia, June 2002.
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.
An expanded version of this paper is also available as a journal publication.
