## AI helps you reading Science

## AI Insight

AI extracts a summary of this paper

Weibo:

# Model checking SPKI/SDSI

Journal of Computer Security, no. 3 (2004): 317-353

EI

Abstract

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-a...More

Code:

Data:

Introduction

- Systems with shared resources use access-control mechanisms for protection. There are two fundamental problems in access control: authorization and enforcement.
- Consider again the PDS P = (P , Γ, ∆), where P = {p1, p2}, Γ = {γ1, · · · , γ6}, and ∆ contains the following transition rules: p2, γ4 → p2, γ1γ2 p1, γ5 → p2, γ4γ3 p1, γ6 → p1, Consider the automaton shown in Fig. 6, which accepts the set of configurations C = { p1, γ5 }.

Highlights

- Systems with shared resources use access-control mechanisms for protection
- In the case of certificate-chain discovery, we show that an operation that is used as a subroutine in algorithms for model checking pushdown systems provides a new algorithm for the problem
- This section explains the connection between SPKI/SDSI and pushdown systems, and demonstrates how the authorization problem, as well as a variety of other certificate-set analysis problems, can be viewed as model-checking problems on pushdown systems
- There are two reasons why Apost is of interest: (i) it can serve as a subroutine in the algorithm for Linear time logic model checking, which provides a way to answer a general class of certificate-set-analysis questions [25, Section 3.2.3], and in other kinds of pushdown systems modelchecking problems, it has been found that, in practice, post works faster than pre [25]
- This section discusses applications of model checking to specific certificate-setanalysis problems; in particular, we show how model checking furnishes algorithms for the analysis problems listed in the introduction. (Here, we use the term “model checking” to mean both (i) the problem of checking whether a given pushdown systems satisfies a given Linear time logic formula, and the problem of answering simple forward and backward reachability queries; the latter can be stated in terms of set-former expressions that use the basic automaton-building operations pre∗ and post∗.) Given a set of certs C and a set of configurations X, we write pre [PC](X) as pre [C](X)
- The SPKI/SDSI-to-pushdown systems connection presented in this paper provides an alternative semantics for SPKI/SDSI: The names of an SPKI/SDSI name space are identified with the configurations of the transition system defined by a pushdown systems

Results

- This section explains the connection between SPKI/SDSI and PDSs, and demonstrates how the authorization problem, as well as a variety of other certificate-set analysis problems, can be viewed as model-checking problems on PDSs. Assume that the authors are given a set of certs C and a request r = (KP , TP ).
- There are two reasons why Apost is of interest: (i) it can serve as a subroutine in the algorithm for LTL model checking, which provides a way to answer a general class of certificate-set-analysis questions [25, Section 3.2.3], and in other kinds of PDS modelchecking problems, it has been found that, in practice, post works faster than pre [25].
- The authors will explain how to construct a certificate chain from such structures using the example from Section 2.2, for which the final configuration automaton is given in Fig. 9.
- When the pre algorithm has been extended as described above, a certificate chain for request r can be obtained from the auxiliary structure associated with (Kowner[T ], , s) in the final configuration automaton.
- (Here, the authors use the term “model checking” to mean both (i) the problem of checking whether a given PDS satisfies a given LTL formula, and the problem of answering simple forward and backward reachability queries; the latter can be stated in terms of set-former expressions that use the basic automaton-building operations pre∗ and post∗.) Given a set of certs C and a set of configurations X, the authors write pre [PC](X) as pre [C](X).

Conclusion

- This section discusses how annotating the PDS and the configuration automaton with labels from a bounded idempotent semiring can answer several useful questions, such as, “How long does a specific authorization last?” and “What is the trust level associated with an authorization?”.10 It describes an alternative way to handle authorization specifications, which has certain advantages over previous proposals.
- Referring back to the example from Section 2.2, for which the final automaton is given in Fig. 9, if a trust level drawn from {Z, L, M , H} were assigned to each certificate, the value that labels the transition (Kowner[H], , s) in the automaton constructed by the algorithm Apre represents the “trust level” of Alice’s authorization.

- Table1: Kinds of arrows used in the paper
- Table2: Semirings for trust and validity
- Table3: A semiring for authorization

Related work

- A certificate-chain-discovery algorithm for SPKI/SDSI was first proposed by Clarke et al [12]. Their algorithm was based on the idea of computing the namereduction closure of the certificate set. A credential-chain-discovery algorithm for the role-based trust management language RT0 was presented by Li et al [23]. One feature that distinguishes our work from both of those papers is the use of automatonbased model-checking techniques from the theory of model checking pushdown systems [8,17]. In the present paper, we have shown that the techniques from the PDS model-checking literature solve not only the problem of discovering certificate chains, but also provide answers to a broad array of questions that one might wish to pose about a set of SPKI/SDSI certificates. One of the most striking differences between this approach and previous work on certificate-chain-discovery is that the PDS-based certificate-chain-discovery algorithms compute the actual closure of the certificate set, not just the name-reduction closure (e.g., see “Authorized access 3” in Section 4.4). In general, the closure of a certificate set is an infinite set; however, it is a regular set – a fact that we are not aware of anyone observing before in the authorization literature – and hence can be represented via a finite-state automaton.

Funding

- *This work was supported in part by the National Science Foundation under grant CCR-9619219, by the Office of Naval Research under contracts N00014-01-1-0796 and N00014-01-1-0708, and by the Alexander von Humboldt Foundation

Reference

- M. Abadi, On SDSI’s linked local name spaces, Journal of Computer Security 6(1–2) (1998), 3–21.
- R. Alur, K. Etessami and M. Yannakakis, Analysis of recursive state machines, in: Proc. Computer-Aided Verif., 2001.
- R. Alur and M. Yannakakis, Model checking of hierarchical state machines, Volume 23 of Software Engineering Notes, New York, ACM Press, 1998, pp. 175–188.
- M. Benedikt, P. Godefroid and T. Reps, Model checking of unrestricted hierarchical state machines, in: ICALP ’01, 2001.
- M. Blaze, J. Feigenbaum, J. Ioannidis and A.D. Keromytis, The KeyNote trust-management system version 2, RFC 2704, September 1999.
- M. Blaze, J. Feigenbaum, J. Ioannidis and A.D. Keromytis, The role of trust management in distributed systems security, in: Secure Internet Programming: Security Issues for Mobile and Distributed Objects, Vitek and Jensen, eds, LNCS 1603, 1999, pp. 185–210.
- R.F. Book and F. Otto, String-Rewriting Systems, Springer, 1993.
- A. Bouajjani, J. Esparza and O. Maler, Reachability analysis of pushdown automata: Application to model checking, in: Proc. CONCUR, Volume 1243 of Lec. Notes in Comp. Sci., Springer-Verlag, 1997, pp. 135–150.
- J.R. Büchi, Finite Automata, Their Algebras and Grammars, Springer, 1988.
- O. Burkart and B. Steffen, Model checking for context-free processes, in: Proc. CONCUR, Volume 630 of Lec. Notes in Comp. Sci., Springer-Verlag, 1992, pp. 123–137.
- D. Caucal, On the regular structure of prefix rewriting, Theoretical Computer Science 106 (1992), 61–86.
- D. Clarke, J.-E. Elien, C.M. Ellison, M. Fredette, A. Morcos and R.L. Rivest, Certficate chain discovery in SPKI/SDSI, Journal of Computer Security 9 (2001), 285–322.
- E.M. Clarke, O. Grumberg and D. Peled, Model Checking, MIT Press, 2000.
- J.-E. Elien, Certificate discovery using SPKI/SDSI 2.0 certificates, Master’s thesis, Massachusetts Institute of Technology, May 1998.
- C. Ellison, Personal communication to S. Jha, T. Reps and S. Schwoon, April 2003.
- C.M. Ellison, B. Frantz, B. Lampson, R.L. Rivest, B.M. Thomas and T. Ylonen, SPKI certificate theory, RFC 2693, September 1999.
- J. Esparza, D. Hansel, P. Rossmanith and S. Schwoon, Efficient algorithms for model checking pushdown systems, in: Proc. Computer-Aided Verif., Volume 1855 of Lec. Notes in Comp. Sci., Springer-Verlag, 2000, pp. 232–247.
- R. Gerth, D. Peled, M. Vardi and P. Wolper, Simple on-the-fly automatic verification of linear temporal logic. in: Protocol Specification Testing and Verification, Chapman & Hall, Warsaw, Poland, 1995, pp. 3–18.
- J.Y. Halpern and R.V.D. Meyden, A logical reconstruction of SPKI, in: Proceedings of the 14th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, 2001, pp. 59–70.
- J. Howell and D. Kotz, A formal semantics for SPKI, Technical Report 2000-363, Department of Computer Science, Dartmouth College, Hanover, NH, March 2000.
- J. Knoop, Demand-driven model checking for context-free processes, in: Proc. Asian Comp. Sci. Conf., Volume 1742 of Lec. Notes in Comp. Sci., P.S. Thiagarajan and R. Yap, eds, Springer-Verlag, 1999, pp. 201–213.
- N. Li and J.C. Mitchell, Understanding SPKI/SDSI using first-order logic, in: Comp. Sec. Found. Workshop, IEEE Comp. Soc., Wash., DC, 2003.
- N. Li, W.H. Winsborough and J.C. Mitchell, Distributed credential chain discovery in trust management, Journal of Computer Security 2002.
- N. Li, Local names in SPKI/SDSI 2.0, in: Proceedings of the 13th IEEE Computer Security Foundations Workshop, 2000.
- S. Schwoon, Model-checking pushdown systems, PhD thesis, University of Munich, Munich, Germany, July 2002.
- S. Schwoon, S. Jha, T. Reps and S. Stubblebine, On generalized authorization problems, in: Comp. Sec. Found. Workshop, IEEE Comp. Soc., Wash., DC, 2003.
- S. Weeks, Understanding trust management systems, in: Proceedings of the IEEE Symposium on Research in Security and Privacy, Research in Security and Privacy, Oakland, CA, IEEE Computer Society,Technical Committee on Security and Privacy, IEEE Computer Society Press, 2001.

Tags

Comments

数据免责声明

页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果，我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问，可以通过电子邮件方式联系我们：report@aminer.cn