Modelling and Analysis of Security Protocols | 拾書所
pickbooks 拾書所
pickbooks 拾書所
x

Site Breadcrumb

Modelling and Analysis of Security Protocols

$ 1,911 元 原價 1,950
立即前往

Description

The definitive technical reference to security protocols: mechanisms, roles, vulnerabilities, and design.

  • Modeling security properties, protocols, environments, and hostile agents.
  • Introduces the Communicating Sequential Processes (CSP) mathematical framework for describing and analyzing interactions amongst distributed agents.
  • Covers key distribution systems, authentication, integrity, confidentiality, anonymity, non-repudiation, availability, and more.
Security protocols (SPs) are the key building blocks for secure distributed systems -- the cornerstones of secure computing. This is the definitive technical reference to security protocols: their goals, mechanisms, properties, and especially their vulnerabilities. It includes in-depth coverage of CSP, a powerful mathematical framework for describing and analyzing the interactions between distributed agents, and one of the most powerful tools available for designing, verifying, and evaluating highly secure protocols. Leading security protocol researchers Peter Ryan and Steve Schneider review the key security issues SPs are intended to address, including authentication, integrity, confidentiality, anonymity, non-repudiation, and availability; and review the mechanisms they employ, including symmetric and asymmetric encryption, hashes, digital signatures, and key management. Next, they introduce the CSP process algebra, a mathematical framework for modeling security properties, protocols, and environments, including hostile agents. They present exceptionally thorough coverage of describing and analyzing the interactions amongst distributed agents, including model-checking and theorem proving techniques essential for anyone who must evaluate or verify security protocols.

Peter Ryan initiated a major research program at the UK Defence Research Agency that utilized the Communicating Sequential Processes framework and model checking to analyze SP5. He chairs the Steering Committee of ESORICS, and serves on the Organizing Committee of the IEEE Computer Security Foundations Workshop, and IEEE Symposium on Security and Privacy. Steve Schneider has published extensively on concurrency theory and security protocols, and is a member of several conference committees.

Back to Top


Table Of Contents

0. Introduction.
Security Protocols.
Security Properties.
Cryptography.
Public-key Certificates and Infrastructures.
Encryption Modes.
Cryptographic Hash Functions.
Digital Signatures.
Security Protocol Vulnerabilities.
The CSP Aproach.
Casper: the User-friendly Interface of FDR.
Limits of Formal Analysis.
Summary.

1. An Introduction to CSP.
Basic Building Blocks.
Parallel Operators.
Hiding and Renaming.
Further Operators.
Process Behaviour.
Discrete Time.

2. Modelling Security Protocols in CSP.
Trustworthy Processes.
Data Types for Protocol Models.
Modelling an Intruder.
Putting the Network Together.

3. Expressing Protocol Goals.
The Yahalom Protocol.
Secrecy.
Authentication.
Non-repudiation.
Anonymity.
Summary.

4. Overview of FDR.
Comparing Processes.
Labelled Transition Systems.
Exploiting Compositional Structure.
Counterexamples.

5. Casper.
An Example Input File.
The %-notation.
Case Study: The Wide-Mouthed-Frog Protocol.
Protocol Specifications.
Hash Functions and Vernam Encryption.
Summary.

6. Encoding Protocols and Intruders for FDR.
CSP from Casper.
Modelling the Intruder: The Perfect Spy.
Wiring the Network Together.
Example Deduction System.
Algebraic Equivalences.
Specifying Desired Properties.

7. Theorem Proving.
Rank Functions.
Secrecy of the Shared Key: a Rank Function.
Secrecy on nB.
Authentication.
Machine Assistance.
Summary.

8. Simplifying Transformations.
Simplifying Transformations for Protocols.
Transformations on Protocols.
Examples of Safe Simplifying Transformations.
Structural Transformations.
Case Study: The CyberCash Main Sequence Protocol.
Summary.

9. Other Approaches.
Introduction.
The Dolev-Yao Model.
BAN Logic and Derivatives.
FDM and InaJo.
NRL Analyser.
The B-method Approach.
The Non-interference Approach.
Strand Spaces.
The Inductive Approach.
Spi Calculus.
Provable Security.

10. Prospects and Wider Issues.
Introduction.
Abstraction of Cryptographic Primitives.
The Refinement Problem.
Combining Formal and Cryptographic Styles of Analysis.
Dependence on Infrastructure Assumptions.
Conference and Group Keying.
Quantum Cryptography.
Data Independence.

Appendix A. Background Cryptography.
The RSA Algorithm.
The ElGamal Public Key System.
Complexity Theory.

Appendix B. The Yahalom Protocol in Casper.
The Casper Input File.
Casper Output.

Appendix C. CyberCash Rank Function Analysis.
Secrecy.
Authentication.

Bibliography.
Notation.
Index. 0201674718T04062001
&

Brand Slider