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.

Paper: [pdf] [ps]

An expanded version of this paper is also available as a journal publication.

This page updated October 14, 2005.