Access control, security, and trust : a logical approach

1 Access Control, Security, Trust, and Logic --
1.1 Deconstructing Access-Control Decisions --
1.2 A Logical Approach to Access Control --
I Preliminaries --
2 A Language for Access Control --
2.1 Sets and Relations --
2.1.1 Notation --
2.1.2 Approaches for Mathematical Proofs --
2.2 Syntax --
2.2.1 Principal Expressions --
2.2.2 Access-Control Statements --
2.2.3 Well-Formed Formulas --
2.3 Semantics --
2.3.1 Kripke Structures --
2.3.2 Semantics of the Logic --
3 Reasoning about Access Control --
3.1 Logical Rules --
3.1.1 The Taut Rule --
3.1.2 The Modus Ponens Rule --
3.1.3 The Says Rule --
3.1.4 The MP Says Rule --
3.1.5 The Speaks For Rule --
3.1.6 The & Says and Quoting Rules --
3.1.7 Properties of -->
 --
3.1.8 The Equivalence Rule --
3.1.9 The Controls Definition --
3.2 Formal Proofs and Theorems --
3.3 Soundness of Logical Rules --
4 Basic Concepts --
4.1 Reference Monitors --
4.2 Access-Control Mechanisms: Tickets and Lists --
4.2.1 Tickets --
4.2.2 Lists --
4.2.3 Logical and Pragmatic Implications --
4.3 Authentication --
4.3.1 Two-Factor Authentication --
4.3.2 Using Credentials from Other Authorities. 5 Security Policies --
5.1 Confidentiality, Integrity, and Availability --
5.2 Discretionary Security Policies --
5.3 Mandatory Security Policies --
5.4 Military Security Policies --
5.4.1 Extending the Logic with Security levels --
5.4.2 Expressing Military Security Policies --
5.4.3 Military Security Policies: An Extended Example --
5.5 Commercial Policies --
5.5.1 Extending the Logic with Integrity Levels --
5.5.2 Protecting Integrity --
5.5.3 Strict Integrity --
5.5.4 An Extended Example of a Strict Integrity Policy --
II Distributed Access Control --
6 Digital Authentication --
6.1 Public-Key Cryptography --
6.2 Efficiency Mechanisms --
6.2.1 Cryptographic Hash Functions --
6.2.2 Data-Encryption Keys --
6.2.3 Digital Signatures --
6.3 Reasoning about Cryptographic Communications --
6.4 Certificates, Certificate Authorities, and Trust --
6.5 Symmetric-Key Cryptography --
7 Delegation --
7.1 Simple Delegations --
7.2 Delegation and Its Properties --
7.3 A Delegation Example: Simple Checking --
7.3.1 Formal Definitions of Checks --
7.3.2 Bank Policies on Checks --
7.3.3 Operating Rules for Checks --
8 Networks: Case Studies --
8.1 SSL and TLS: Authentication across the Web --
8.1.1 Handshake Protocol --
8.1.2 Record Protocol --
8.2 Kerberos: Authentication for Distributed Systems --
8.2.1 Initial Authentication Requests --
8.2.2 Requests for Service-Specific Tickets --
8.2.3 Requests for Services --
8.2.4 Proxiable Tickets --
8.3 Financial Networks --
8.3.1 Electronic Clearinghouses --
8.3.2 Bank Authorities, Jurisdiction, and Policies --
8.3.3 Bank Operating Rules. III Isolation and Sharing --
9 A Primer on Computer Hardware --
9.1 Ones and Zeros --
9.2 Synchronous Design --
9.2.1 Synchronous Registers --
9.2.2 Registers with Load Control --
9.2.3 Registers with Tri-State Outputs --
9.2.4 Combinational Logic and Functions --
9.2.5 Arithmetic Logic Units --
9.3 Microcode --
9.3.1 Data Paths and Control Paths --
9.3.2 Microprogramming --
10 Virtual Machines and Memory Protection --
10.1 A Simple Processor --
10.1.1 Processor Components --
10.1.2 Machine Instructions --
10.2 Processors with Memory Segmentation --
10.2.1 Segmentation Using a Relocation Register --
10.2.2 Processor State and Instructions --
10.2.3 Program Status Word --
10.2.4 Traps --
10.3 Controlling Access to Memory and Segmentation Registers --
10.3.1 Access to Program Memory --
10.3.2 Implementation Details --
10.3.3 Access to the Relocation Register --
10.3.4 Setting the Mode Bit --
10.4 Design of the Virtual Machine Monitor --
10.4.1 Privileged Instructions --
10.4.2 Sensitive Instructions --
10.4.3 Virtualizable Processor Architectures --
11 Access Control Using Descriptors and Capabilities --
11.1 Address Descriptors and Capabilities --
11.2 Tagged Architectures --
11.3 Capability Systems --
11.3.1 Catalogs --
11.3.2 Creating New Segments --
11.3.3 Dynamic Sharing --
11.3.4 Revocation of Capabilities. 12 Access Control Using Lists and Rings --
12.1 Generalized Addresses --
12.2 Segment Access Controllers --
12.3 ACL-Based Access Policy for Memory Accesses --
12.4 Ring-Based Access Control --
12.4.1 Access Brackets --
12.4.2 Call Brackets --
IV Access Policies --
13 Confidentiality and Integrity Policies --
13.1 Classifications and Categories --
13.2 Bell-La Padula Model, Revisited --
13.3 Confidentiality levels: Some Practical Considerations --
13.4 Biba's Strict Integrity, Revisited --
13.5 Lipner's Integrity Model --
13.5.1 Commercial Integrity Requirements --
13.5.2 Commercial Integrity via Bell-La Padula --
13.5.3 Commercial Integrity via Bell-La Padula and Strict Integrity --
14 Role-Based Access Control --
14.1 RBAC Fundamentals --
14.1.1 Role Inheritance --
14.1.2 Sessions --
14.2 Separation of Duty --
14.2.1 Static Separation of Duty --
14.2.2 Dynamic Separation of Duty --
14.3 Representing RBAC Systems in the Logic --
14.3.1 RBAC Extensions to the Logic --
14.3.2 Translating RBAC into the Logic 305.