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）數學框架。
- 涵蓋關鍵分配系統、身份驗證、完整性、保密性、匿名性、不可否認性、可用性等主題。

安全協議（SPs）是安全分散系統的關鍵構建塊，是安全計算的基石。本書是關於安全協議的權威技術參考：它們的目標、機制、特性，特別是它們的漏洞。書中深入探討了CSP，這是一個強大的數學框架，用於描述和分析分散代理之間的互動，也是設計、驗證和評估高度安全協議的最強大工具之一。領先的安全協議研究者Peter Ryan和Steve Schneider回顧了SPs旨在解決的關鍵安全問題，包括身份驗證、完整性、保密性、匿名性、不可否認性和可用性；並回顧了它們所使用的機制，包括對稱和非對稱加密、哈希、數位簽名和密鑰管理。接下來，他們介紹了CSP過程代數，這是一個用於建模安全性質、協議和環境（包括敵對代理）的數學框架。他們對描述和分析分散代理之間的互動進行了非常徹底的探討，包括模型檢查和定理證明技術，這對於任何需要評估或驗證安全協議的人來說都是必不可少的。

Peter Ryan在英國國防研究機構啟動了一個主要的研究計劃，利用通訊序列過程框架和模型檢查來分析SP5。他擔任ESORICS的指導委員會主席，並在IEEE計算機安全基礎研討會和IEEE安全與隱私研討會的組織委員會中任職。Steve Schneider在並行理論和安全協議方面發表了大量著作，並是幾個會議委員會的成員。

目錄
0. 介紹。
安全協議。
安全性質。
密碼學。
公鑰證書和基礎設施。
加密模式。
密碼哈希函數。
數位簽名。
安全協議漏洞。
CSP方法。
Casper：FDR的用戶友好介面。
形式分析的限制。
摘要。

1. CSP簡介。
基本構建塊。
並行運算子。
隱藏和重新命名。
進一步的運算子。
過程行為。
離散時間。

2. 在CSP中建模安全協議。
可信過程。
協議模型的數據類型。
建模入侵者。
組合網絡。

3. 表達協議目標。
Yahalom協議。
保密性。
身份驗證。
不可否認性。
匿名性。
摘要。

4. FDR概述。
比較過程。
標記轉換系統。
利用組合結構。
反例。

5. Casper。
示例輸入文件。
%-表示法。
案例研究：寬口青蛙協議。
協議規範。
哈希函數和Vernam加密。
摘要。

6. 為FDR編碼協議和入侵者。
來自Casper的CSP。
建模入侵者：完美間諜。
連接網絡。
示例推導系統。
代數等價。
指定所需性質。

7. 定理證明。
秩函數。
共享密鑰的保密性：一個秩函數。
nB的保密性。
身份驗證。
機器輔助。
摘要。

8. 簡化轉換。
協議的簡化轉換。
對協議的轉換。
安全簡化轉換的示例。
結構轉換。
案例研究：CyberCash主序列協議。
摘要。

9. 其他方法。
介紹。
Dolev-Yao模型。
BAN邏輯及其衍生物。
FDM和InaJo。
NRL分析器。
B方法。
非干擾方法。
Strand空間。
歸納方法。
Spi計算。
可證明的安全性。

10. 前景和更廣泛的問題。
介紹。
密碼原語的抽象。
細化問題。
結合形式和密碼分析風格。
對基礎設施假設的依賴。
會議和群組密鑰。
量子密碼學。
數據獨立性。

附錄A. 背景密碼學。
RSA算法。
ElGamal公鑰系統。
複雜性理論。

附錄B. Casper中的Yahalom協議。
Casper輸入文件。
Casper輸出。

附錄C. CyberCash秩函數分析。
保密性。
身份驗證。

參考文獻。
符號。
索引。

類似商品