Analysis of SPKI/SDSI certificates using model checking
Analysis of SPKI/SDSI certificates using model checking
复制标题
使用模型检查分析 SPKI/SDSI 证书
DOI：
10.1109/csfw.2002.1021812
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
T. Reps
中科院分区：
文献类型：
--
作者：
S. Jha;T. Reps
SPKI/SDSI是一个框架，用于表达分布式计算环境中出现的命名和授权问题。我们在SPKI/SDSI和一种被称为下推系统（pds）的形式主义之间建立了联系。我们展示了SPKI/ sdsi到pds的连接为形式化各种证书分析问题提供了一个框架。此外，该连接具有计算意义：使用现有的模型检查下推系统算法可以有效地解决许多分析问题（即在证书集大小的时间多项式中）。
SPKI/SDSI is a framework for expressing naming and authorization issues that arise in a distributed-computing environment. 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.