Formal Verification of Access Control for XML Documents
- 주제(키워드) Formal Verification , Access Control , XML , CSP , FDR
- 발행기관 고려대학교 대학원
- 지도교수 최진영
- 발행년도 2013
- 학위수여년월 2013. 2
- 학위구분 박사
- 학과 일반대학원 컴퓨터학과
- 원문페이지 168 p
- 실제URI http://www.dcollection.net/handler/korea/000000038490
- 본문언어 한국어
- 제출원본 000045745775
초록/요약
XML component-based access control systems has become an active research topic with the increase of XML components and with the importance of access control to XML data. Reasoning about the access control model for XML documents is a non-trivial topic because of its own challenging issues: the speci cation of query, schema and schema-level access control policy XPath language, and semantics of con iction resolution. In this paper, we present a novel methodology for specifying and verifying access control model to XML documents consisting of query, schema, and an ac- cess control policy. To achieve this, we translate query, schema, and the seman- tics of access control policies including con iction resolution into CSP-like process algebra languages through some examples. In addition, We present how to de- scribe a formal speci cation for authorized view on schema-level access control by assigning already well-established concurrency semantics. The behavioral equiva- lence between a process algebra view and authorized view to XML components is proven to illustrate the validity of our approach. Then, we demonstrate how this technique can be applied to specify and verify access control model for electronic patient record using CSP and FDR tool. Finally, our work opens the possibility to reason about the of access control policies with the support of automated model checking tools, because it provides the formal semantics for access control policies and XML documents with the tree structure.
more목차
1 Introduction 1
1.1 Thesis Overview 1
1.2 Related Works 4
2 Background 7
2.1 Electronic Health Record (EHR) 7
2.2 Privacy and Security 9
2.2.1 Privacy 10
2.2.2 Security 12
2.3 Security Protocols 16
2.3.1 Key Distribution Protocol 17
2.3.2 Authentication Protocol 17
2.3.3 Examples of Security Protocols 18
2.4 Attack Types 27
2.4.1 Man-in-the-middle Attack 27
2.4.2 Reflection Attack 28
2.4.3 Replay Attack 29
2.4.4 Interleave Attack 29
2.4.5 Dictionary Attack 31
2.4.6 Type-flaw Attack 32
2.4.7 Buffer Overflow Attack 34
2.5 XML Encryption and XML Signature 38
3 Formal Specification 41
3.1 CSP(Communicating Sequential Processes) 41
3.2 Casper(A Compiler of Security Protocol Analyzer) 51
4 Model Checking 53
4.1 Model Checking vs Theorem Proving 53
4.2 FDR(Failure and Divergence Refinement) 54
5 Verification of Access Control Policy to XML Documents 59
5.1 Framework for Static Verification of Access Control to
XML Documents 59
5.2 Illustrative Example 60
5.3 Schema-level Access Control 63
5.3.1 XPath Expression 64
5.3.2 Semantics of Access Control Policy 66
5.4 A Process Algebra View of Access Control Semantics 68
5.4.1 Formal Model for Schema and ACP 69
5.4.2 Strong Equivalence 75
5.4.3 Verification using FDR 78
5.5 Putting Together 82
5.5.1 Scalability 86
6 Formal Verification of Security Properties to AXML
Documents 91
6.1 Introduction 91
6.2 Active XML 95
6.2.1 Security Issues 97
6.3 Utilizing Security Service calls in AXML 99
6.3.1 XML Encryption and XML Signature 99
6.3.2 Security Services and Calls 102
6.4 Case Study : Electronic Patient Record 106
6.4.1 Scenario 106
7 Conclusion 113
Bibliography 114
