Foundations of Security Analysis and Design: Tutorial Lectures (Lecture Notes in Computer Science, 2171)

✍ Scribed by Riccardo Focardi (editor), Roberto Gorrieri (editor)

• Publisher: Springer
• Year: 2001
• Tongue: English
• Leaves: 406
• Category: Library

✦ Synopsis

Security is a rapidly growing area of computer science, with direct and increasing relevance to real life applications such as Internet transactions, electronic commerce, information protection, network and systems integrity, etc. This volume presents thoroughly revised versions of lectures given by leading security researchers during the IFIP WG 1.7 International School on Foundations of Security Analysis and Design, FOSAD 2000, held in Bertinoro, Italy in September. Mathematical Models of Computer Security (Peter Y.A. Ryan); The Logic of Authentication Protocols (Paul Syversen and Iliano Cervesato); Access Control: Policies, Models, and Mechanisms (Pierangela Samarati and Sabrina de Capitani di Vimercati); Security Goals: Packet Trajectories and Strand Spaces (Joshua D. Guttman); Notes on Nominal Calculi for Security and Mobility (Andrew D. Gordon); Classification of Security Properties (Riccardo Focardi and Roberto Gorrieri).

✦ Table of Contents

Foundations of Security Analysis and Design
International School on Foundations of Security Analysis and Design
Table of Contents
Mathematical Models of Computer Security
Background
Mathematical Models
Formal Models and Methods
A Brief History of Security Models
The Bell and LaPadula Model
The Simple Security Property
The * Property
The Harrison-Ruzzo-Ullman Model
Chinese Walls
The Clark Wilson Model
The Biba Model
Drawbacks of BLP
Non-interference
Goguen Meseguer
Unwinding
Non-interference Is Not a Trace Property
Relationship to Bell LaPadula
Generalisations to Non-deterministic Systems
The Process Algebraic Approach
Introduction to CSP and Process Algebra
CSP Syntax
Prefix
Prefix Choice
Communication
External Choice
Internal Choice
Parallel Composition
Interleave
Hiding
Renaming
After
Semantics
Definition
Refinement
Some Useful Processes
Labelled Transition Systems
Acceptances and Ready Sets
CSP Formulations of Non-interference
Abstraction
Unwinding the CSP Formulation
Unwinding (Symmetric Version)
Operational Semantics
Strong Bi-simulation
Weak Bi-simulation
Unwinding and Bi-simulation
Power Bi-simulation
Loose Bi-simulation
Power Bi-simulation for Non-interference
Composability
The Roscoe-Woodcock-Wulf Approach
Definition.
The Jacob Security Ordering
Testing Equivalence
May Testing Equivalence
May Testing Non-interference
Non-deducibility
Non-deducibility on Strategies
The Lowe Approach to Information Flow
Generalisations
Limitations of Non-interference
Encrypted Channels
Downgrading Statistical Information from a Sensitive Database
File Editing
Operating Systems
Intransitive Non-interference
Fault-Tolerance
Intrusion-Tolerance
Anonymity
Dynamic Separation of Duty
Dealing with Probability
Dealing with Time
Future Directions
Composition Results
Links to Cryptographic Analysis Techniques
Subliminal Channels and Information Hiding
Automated Support
Links to Other Process Algebras
Static and Typing Analysis
Conclusions
Acknowledgements
References
The Logic of Authentication Protocols
Introduction
Background on Authentication Protocols
Running Example
Organization
BAN Logic
BAN Notation
BAN Rules
BAN Protocol Analysis
Example: Analysis of Needham-Schroeder Shared-Key (NSSK)
The Denning-Sacco Attack
The Nessett Protocol
Nessett Protocol Derivations
Nessett's Critique of BAN
Expanding Beyond BAN
SVO Logic: Unifying the Predecessors
SVO Notation
SVO Rules
SVO Axioms
Belief Axioms
Source Association Axioms
Key Agreement Axioms
Receiving Axioms
Possession Axioms
Comprehension Axiom
Saying Axioms
Freshness Axioms
Jurisdiction and Nonce-Verification Axioms
Symmetric Goodness Axiom
Protocol Analysis
The Nessett Protocol in SVO
Authentication Goals
BAN Authentication Goals
VO Authentication Goals
Replay Attacks
A Taxonomy of Replays
Gauging Expressiveness
Adding Time to Increase Expressiveness
Roles in Cryptographic Protocols
A Child's Garden of Authentications
What Do We Mean by Entity Authentication?
Agreements
Intensional Specification
Matching Histories
Cautionary Note
Design Principles and Protocol Logics
Protocol Design Principles
Design Principle Comments
Fail-Stop Protocols
Extensible Fail-Stop Protocols
Design Rules and Protocol Logics
Semantic Approaches
NPATRL
The NRL Protocol Analyzer Model
A Requirement Language for the NRL Protocol Analyzer
Strand Semantics for BAN Languages
Overview of Strands
Possible Worlds from Strand Spaces
Strand Semantics for Knowledge
Truth Conditions for BAN-Style Formulae
The Future
References
Access Control: Policies, Models, and Mechanisms
Introduction
Basic Concepts of Discretionary Policies
The Access Matrix Model
Implementation of the Access Matrix
Vulnerabilities of the Discretionary Policies
Mandatory Policies
Security Classifications
Secrecy-Based Mandatory Policies
The Bell-LaPadula Model (Some History)
Integrity-based Mandatory Policies: The Biba Model
Applying Mandatory Policies to Databases
Limitations of Mandatory Policies
Enriching DAC with Mandatory Restrictions
The Chinese Wall Policy
Authorization-Based Information Flow Policies
Discretionary Access Control Policies
Expanding Authorizations
Temporal Authorizations
A Calculus for Access Control
Administrative Policies
Integrity Policies
Role-Based Access Control Policies
Named Protection Domain
Role-Based Policies
Advanced Access Control Models
Logic-Based Authorization Languages
Composition of Access Control Policies
Certificate-Based Access Control
References
Security Goals: Packet Trajectories and Strand Spaces
Introduction
The Purpose of These Lectures
The Structure of These Lectures
Acknowledgements
The Packet Protection Problem
Packet Filtering
An Example
Types of Information in Our Security Goals
The Logical Form of Our Security Goals
Some Security Goals
Security Modeling
Localization
Two Algorithms
Posture Checking
Posture Generation
Implementing Boolean Algebras
The Abstraction Problem
The Logic of Access Lists
Binary Decision Diagrams
Finding Atoms in BDDs
An Algorithm for Finding Atoms
Source and Destination Addresses, Multiple Filters
Atomizer Results
Packet Trajectories and Security Management
Strand Spaces and Protocol Security Goals
What is a Cryptographic Protocol?
The Dolev-Yao Problem
An Example: The Needham-Schroeder Public Key Protocol
Unintended Services
Another Example: An ISO Candidate
Types of Unintended Service
The Dolev-Yao Problem Defined
Strand Space Ideas
The Powers of the Penetrator
Representing Protocols
Auxiliary Functions
Parametric Strands
Restricted Values
Unique Origination and Non-origination
What Is an Authentication Goal?
What Is a Secrecy Goal?
Summary of this Section
Appendix: Strand Space Definitions
Strand Spaces
Bundles and Causal Precedence
Terms, Encryption, and Freeness Assumptions
Penetrator Strands
Paths and Well-Behaved Bundles
Bundle Equivalence
Redundancies
Paths
Constructive and Destructive Edges, Normal Bundles
Rising and Falling Paths
A Catalog of Penetrator Paths
New Components and Efficient Bundles
Penetrable Keys
Safe Keys
Proving Authentication
The Outgoing Authentication Test
The Incoming Authentication Test
The Unsolicited Test
Neuman-Stubblebine
Protocol Independence via Disjoint Encryption
Avoiding Conflict
Multiprotocol Strand Spaces
Linking Paths
Bridges
Disjoint Encryption
The Protocol Independence Theorem
An Application of Protocol Independence
Conclusion
References
Notes on Nominal Calculi for Security and Mobility
Introduction
Part I: The Pi Calculus
Outline of the Pi Calculus
Security Examples Using Restricted Channels
A First Example
An Example with Channel Establishment
Discussion: The Pi Calculus
Part: II: The Spi Calculus
The Spi Calculus with Shared-Key Cryptography
Security Examples Using Shared-Key Cryptography
A First Cryptographic Example
An Example with Key Establishment
A Complete Authentication Example (with a Flaw)
A Complete Authentication Example (Repaired)
Discussion of the Examples
Formal Semantics of the Spi Calculus
The Reaction Relation
Testing Equivalence
Further Cryptographic Primitives
Hashing
Public-Key Encryption and Digital Signatures
Discussion: The Spi Calculus
Part III: The Ambient Calculus
Motivation for Ambients
Ambients
Technical Context: Systems
Technical Context: Formalisms
Summary of Our Approach
A Polyadic Ambient Calculus
Types for the Ambient Calculus
Introduction to Exchange Types
Topics of Conversation
Intuitions
Typing of Processes
Typing of Ambients
Typing of Open
Typing of In and Out
Groups
Typed Ambient Calculus
Types and Processes
Typing Rules
Subject Reduction
Opening Control
The System
Subject Reduction
Crossing Control
The System
The Need for Objective Moves
Encoding a Distributed Language
The Distributed Language
Typed Translation to the Ambient Calculus
Discussion: The Ambient Calculus
Related Work on Types
Related Work on Ambients
References
Classification of Security Properties
Introduction
SPA and Value-Passing
The Language
Operational Semantics and Equivalences
Trace Equivalence
Observational Equivalence
Failure/Testing Equivalence
Value-Passing SPA
The Access Monitor
Information Flow Properties
Properties Based on Trace Equivalence
Detecting High Level Deadlocks through Failure/Testing Equivalences
Properties Based on Observational Equivalence
Building Channels by Exploiting Deadlocks
Comparison with Related Work
Lazy Security
Failure Non Deducibility on Compositions
Comparison
Other Security Properties
The Compositional Security Checker
Input-Output and Architecture
Checking the Information Flow Properties
A Sample Session
An Example: Checking the Access Monitor
State Explosion and Compositionality
Conclusion
References
Author Index