Access control, security, and trust : a logical approach

Developed from the authors' courses at Syracuse University and the U.S. Air Force Research Laboratory, Access Control, Security, and Trust: A Logical Approach equips readers with an access control logic they can use to specify and verify their security designs. Throughout the text, the authors use a single access control logic based on a simple propositional modal logic.

The first part of the book presents the syntax and semantics of access control logic, basic access control concepts, and an introduction to confidentiality and integrity policies. The second section covers access control in networks, delegation, protocols, and the use of cryptography. In the third section, the authors focus on hardware and virtual machines. The final part discusses confidentiality, integrity, and role-based access control.

Taking a logical, rigorous approach to access control, this book shows how logic is a useful tool for analyzing security designs and spelling out the conditions upon which access control decisions depend. It is designed for computer engineers and computer scientists who are responsible for designing, implementing, and verifying secure computer and information systems.

Author Notes

Shiu-Kai Chin is a Meredith Professor in the Department of Electrical Engineering and Computer Science at Syracuse University. He is also director of the Center for Information and Systems Assurance and Trust. While at Syracuse, Dr. Chin has received the Outstanding Teacher Award, the Chancellor's Citation for Outstanding Contributions to the University's Academic Programs, and the Crouse Hinds Award for Excellence in Education.

Susan Older is an associate professor in the Department of Electrical Engineering and Computer Science at Syracuse University. She is also the program director for the Certificate of Advanced Study in Systems Assurance. Dr. Older's research interests include programming-language semantics, logics of programs, formal methods, and information-assurance and computer science education.

List of Tables	p. xiii
List of Figures	p. xv
Preface	p. xix
1 Access Control, Security, Trust, and Logic	p. 1
1.1 Deconstructing Access-Control Decisions	p. 3
1.2 A Logical Approach to Access Control	p. 6
I Preliminaries	p. 9
2 A Language for Access Control	p. 11
2.1 Sets and Relations	p. 11
2.1.1 Notation	p. 12
2.1.2 Approaches for Mathematical Proofs	p. 13
2.2 Syntax	p. 15
2.2.1 Principal Expressions	p. 17
2.2.2 Access-Control Statements	p. 18
2.2.3 Well-Formed Formulas	p. 20
2.3 Semantics	p. 22
2.3.1 Kripke Structures	p. 23
2.3.2 Semantics of the Logic	p. 28
2.4 Summary	p. 37
2.5 Further Reading	p. 37
3 Reasoning about Access Control	p. 39
3.1 Logical Rules	p. 39
3.1.1 The Taut Rule	p. 41
3.1.2 The Modus Ponens Rule	p. 42
3.1.3 The Says Rule	p. 42
3.1.4 The MP Says Rule	p. 42
3.1.5 The Speaks For Rule	p. 43
3.1.6 The & Says and Quoting Rules	p. 43
3.1.7 Properties of →	p. 43
3.1.8 The Equivalence Rule	p. 45
3.1.9 The Controls Definition	p. 46
3.2 Formal Proofs and Theorems	p. 47
3.3 Soundness of Logical Rules	p. 50
3.4 Summary	p. 54
3.5 Further Reading	p. 54
4 Basic Concepts	p. 57
4.1 Reference Monitors	p. 57
4.2 Access-Control Mechanisms: Tickets and Lists	p. 60
4.2.1 Tickets	p. 61
4.2.2 Lists	p. 63
4.2.3 Logical and Pragmatic Implications	p. 66
4.3 Authentication	p. 68
4.3.1 Two-Factor Authentication	p. 68
4.3.2 Using Credentials from Other Authorities	p. 70
4.3.3 Groups	p. 74
4.4 Summary	p. 75
4.5 Further Reading	p. 76
5 Security Policies	p. 77
5.1 Confidentiality, Integrity, and Availability	p. 77
5.2 Discretionary Security Policies	p. 79
5.3 Mandatory Security Policies	p. 81
5.4 Military Security Policies	p. 85
5.4.1 Extending the Logic with Security levels	p. 85
5.4.2 Expressing Military Security Policies	p. 87
5.4.3 Military Security Policies: An Extended Example	p. 90
5.5 Commercial Policies	p. 94
5.5.1 Extending the Logic with Integrity Levels	p. 95
5.5.2 Protecting Integrity	p. 97
5.5.3 Strict Integrity	p. 98
5.5.4 An Extended Example of a Strict Integrity Policy	p. 100
5.6 Summary	p. 105
5.7 Further Reading	p. 105
II Distributed Access Control	p. 107
6 Digital Authentication	p. 109
6.1 Public-Key Cryptography	p. 109
6.2 Efficiency Mechanisms	p. 112
6.2.1 Cryptographic Hash Functions	p. 112
6.2.2 Data-Encryption Keys	p. 113
6.2.3 Digital Signatures	p. 113
6.3 Reasoning about Cryptographic Communications	p. 114
6.4 Certificates, Certificate Authorities, and Trust	p. 116
6.5 Symmetric-Key Cryptography	p. 125
6.6 Summary	p. 131
6.7 Further Reading	p. 131
7 Delegation	p. 133
7.1 Simple Delegations	p. 133
7.2 Delegation and Its Properties	p. 135
7.3 A Delegation Example: Simple Checking	p. 141
7.3.1 Formal Definitions of Checks	p. 142
7.3.2 Bank Policies on Checks	p. 143
7.3.3 Operating Rules for Checks	p. 144
7.4 Summary	p. 147
7.5 Further Reading	p. 147
8 Networks: Case Studies	p. 149
8.1 SSL and TLS: Authentication across the Web	p. 149
8.1.1 Handshake Protocol	p. 150
8.1.2 Record Protocol	p. 155
8.2 Kerberos: Authentication for Distributed Systems	p. 157
8.2.1 Initial Authentication Requests	p. 157
8.2.2 Requests for Service-Specific Tickets	p. 159
8.2.3 Requests for Services	p. 161
8.2.4 Proxiable Tickets	p. 162
8.3 Financial Networks	p. 166
8.3.1 Electronic Clearinghouses	p. 166
8.3.2 Bank Authorities, Jurisdiction, and Policies	p. 169
8.3.3 Bank Operating Rules	p. 170
8.4 Summary	p. 172
8.5 Further Reading	p. 173
III Isolation and Sharing	p. 175
9 A Primer on Computer Hardware	p. 177
9.1 Ones and Zeros	p. 177
9.2 Synchronous Design	p. 178
9.2.1 Synchronous Registers	p. 178
9.2.2 Registers with Load Control	p. 179
9.2.3 Registers with Tri-State Outputs	p. 179
9.2.4 Combinational Logic and Functions	p. 182
9.2.5 Arithmetic Logic Units	p. 184
9.3 Microcode	p. 190
9.3.1 Data Paths and Control Paths	p. 190
9.3.2 Microprogramming	p. 192
9.4 Summary	p. 193
9.5 Further Reading	p. 195
10 Virtual Machines and Memory Protection	p. 197
10.1 A Simple Processor	p. 198
10.1.1 Processor Components	p. 199
10.1.2 Machine Instructions	p. 201
10.2 Processors with Memory Segmentation	p. 204
10.2.1 Segmentation Using a Relocation Register	p. 204
10.2.2 Processor State and Instructions	p. 207
10.2.3 Program Status Word	p. 207
10.2.4 Traps	p. 208
10.3 Controlling Access to Memory and Segmentation Registers	p. 209
10.3.1 Access to Program Memory	p. 210
10.3.2 Implementation Details	p. 212
10.3.3 Access to the Relocation Register	p. 213
10.3.4 Setting the Mode Bit	p. 215
10.4 Design of the Virtual Machine Monitor	p. 217
10.4.1 Privileged Instructions	p. 220
10.4.2 Sensitive Instructions	p. 221
10.4.3 Virtualizable Processor Architectures	p. 223
10.5 Summary	p. 224
10.6 Further Reading	p. 225
11 Access Control Using Descriptors and Capabilities	p. 227
11.1 Address Descriptors and Capabilities	p. 227
11.2 Tagged Architectures	p. 231
11.3 Capability Systems	p. 233
11.3.1 Catalogs	p. 233
11.3.2 Creating New Segments	p. 235
11.3.3 Dynamic Sharing	p. 237
11.3.4 Revocation of Capabilities	p. 239
11.4 Summary	p. 241
11.5 Further Reading	p. 242
12 Access Control Using Lists and Rings	p. 245
12.1 Generalized Addresses	p. 245
12.2 Segment Access Controllers	p. 247
12.3 ACL-Based Access Policy for Memory Accesses	p. 249
12.4 Ring-Based Access Control	p. 253
12.4.1 Access Brackets	p. 254
12.4.2 Call Brackets	p. 255
12.5 Summary	p. 258
12.6 Further Reading	p. 259
IV Access Policies	p. 261
13 Confidentiality and Integrity Policies	p. 263
13.1 Classifications and Categories	p. 263
13.2 Bell-La Padula Model, Revisited	p. 266
13.3 Confidentiality levels: Some Practical Considerations	p. 269
13.4 Biba's Strict Integrity, Revisited	p. 272
13.5 Lipner's Integrity Model	p. 276
13.5.1 Commercial Integrity Requirements	p. 277
13.5.2 Commercial Integrity via Bell-La Padula	p. 277
13.5.3 Commercial Integrity via Bell-La Padula and Strict Integrity	p. 281
13.6 Summary	p. 285
13.7 Further Reading	p. 285
14 Role-Based Access Control	p. 289
14.1 RBAC Fundamentals	p. 289
14.1.1 Role Inheritance	p. 290
14.1.2 Sessions	p. 295
14.2 Separation of Duty	p. 297
14.2.1 Static Separation of Duty	p. 297
14.2.2 Dynamic Separation of Duty	p. 299
14.3 Representing RBAC Systems in the Logic	p. 304
14.3.1 RBAC Extensions to the Logic	p. 304
14.3.2 Translating RBAC into the Logic	p. 305
14.4 Summary	p. 310
14.5 Further Reading	p. 312
A Summary of the Access-Control Logic	p. 313
A.1 Syntax	p. 313
A.2 Core Rules, Derived Rules, and Extensions	p. 315
Bibliography	p. 321
Notation Index	p. 324
General Index	p. 325

Available:*

On Order

Summary

Summary

Author Notes

Table of Contents