Modelling and Analysis of Security Protocols

Peter Ryan, Steve Schneider, Michael Goldsmith, Gavin Lowe, Bill Roscoe

Modelling and Analysis of Security Protocols
  • 出版商: Addison Wesley
  • 出版日期: 2000-12-21
  • 售價: $1,950
  • 貴賓價: 9.8 折 $1,911
  • 語言: 英文
  • 頁數: 320
  • 裝訂: Paperback
  • ISBN: 0201674718
  • ISBN-13: 9780201674712
  • 相關分類: 資訊安全

    • 下單後立即進貨 (約5~7天)

買這商品的人也買了...

商品描述


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


Back to Top

商品描述(中文翻譯)

《安全協議：機制、角色、漏洞和設計的權威技術參考》是關於安全協議的技術參考書籍，涵蓋了安全協議的目標、機制、特性以及漏洞。書中詳細介紹了通信順序處理（CSP）數學框架，用於描述和分析分布式代理之間的交互作用，這是設計、驗證和評估高度安全協議的最強大工具之一。作者Peter Ryan和Steve Schneider是領先的安全協議研究人員，他們回顧了安全協議所要解決的關鍵安全問題，包括身份驗證、完整性、機密性、匿名性、不可否認性和可用性；並介紹了對稱和非對稱加密、哈希、數字簽名和密鑰管理等機制。此外，他們還介紹了CSP過程代數，這是一個用於建模安全特性、協議和環境的數學框架，包括敵對代理。書中還詳細介紹了描述和分析分布式代理之間的交互作用的技術，包括模型檢查和定理證明技術，這對於任何需要評估或驗證安全協議的人來說都是必不可少的。

作者Peter Ryan在英國國防研究機構發起了一個利用通信順序處理框架和模型檢查來分析SP5的重大研究計劃。他是ESORICS的主席，並擔任IEEE計算機安全基礎研討會和IEEE安全與隱私研討會的組織委員會成員。Steve Schneider在並發理論和安全協議方面發表了大量論文，並擔任多個會議委員會的成員。

目錄包括：
0. 簡介
1. CSP簡介
2. 在CSP中建模安全協議
3. 表達協議目標
4. FDR概述
5. Casper

該書提供了對安全協議的全面介紹和分析，並介紹了相關的數學框架和工具，對於研究和實踐安全協議的專業人士非常有價值。

類似商品