顶部
收藏

密码协议 基于可信任新鲜性的安全性分析(英文版)


作者:
Ling Dong, Kefei Chen
定价:
48.00元
ISBN:
978-7-04-031331-4
版面字数:
550.000千字
开本:
16开
全书页数:
373页
装帧形式:
精装
重点项目:
暂无
出版时间:
2011-10-11
读者对象:
高等教育
一级分类:
计算机/教育技术类
二级分类:
信息安全专业课程

《密码协议:基于可信任新鲜性的安全性分析(英文版)》主要介绍如何利用系统工程思想和可信任新鲜性的方法,分析和设计密码通信协议。作者基于可信任的新 鲜性标识符概念,提出了一个新颖的新鲜性原则。该原则指出了一种有效的、易用的密码协议安全性分析方法。使用这种分析方法,可以有效检验协议在实际应用中 能否满足安全需要。此外,书中给出大量的分析实0例,详细说明如何基于概率定义安全性,如何将安全指标定量化,如何针对具体的协议寻找漏洞,如何自动实现 协议漏洞的查找,等等。

《密码协议:基于可信任新鲜性的安全性分析(英文版)》总结了作者近年来的研究成果,这些成果的有效性和易用性对从事通信协议安全性研究的人员,特别是工 程技术人员,具有很好的参考和实用价值。董玲网络系统建设和信息安全领域高级工程师,上海交通大学密码与信息安全实验室兼职教授、研究兴趣是信息安全和应 用密码学,特别是实际应用的密码通信协议和密码系统的安全性分析。陈克非上海交通大学计算机科学与工程系教授,长期从事密码与信息安全理论研究。主要研究 兴趣是序列密码、可证明安全、密码协议分析、数据安全。近年来承担多项国家自然科学基金、国家高技术研究发展计划(863计划),发表学术论文150多 篇,编辑出版学术著作7部。

  • Front Matter
  • 1 Introduction of Cryptographic Protocols
    • 1.1 Information security and cryptography
    • 1.2 Classes of cryptographic protocols
      • 1.2.1 Authentication protocol
      • 1.2.2 Key establishment protocol
      • 1.2.3 Electronic commerce protocol
      • 1.2.4 Secure multi-party protocol
    • 1.3 Security of cryptographic protocols
    • 1.4 Motivations of this book
    • References
  • 2 Background of Cryptographic Protocols
    • 2.1 Preliminaries
      • 2.1.1 Functions
      • 2.1.2 Terminology
    • 2.2 Cryptographic primitives
      • 2.2.1 Cryptology
      • 2.2.2 Symmetric-key encryption
      • 2.2.3 Public-key encryption
      • 2.2.4 Digital signatures
      • 2.2.5 Hash Functions
      • 2.2.6 Message authentication
    • 2.3 Cryptographic protocols
      • 2.3.1 Secure channel
      • 2.3.2 Principals
      • 2.3.3 Time-variant parameters
      • 2.3.4 Challenge and response
      • 2.3.5 Other classes of cryptographic protocols
    • 2.4 Security of cryptographic protocols
      • 2.4.1 Attacks on primitives
      • 2.4.2 Attacks on protocols
      • 2.4.3 Security of protocols
      • 2.4.4 Analysis methods for protocol security
    • 2.5 Communication threat model
      • 2.5.1 Dolev-Yao threat model
      • 2.5.2 Assumptions of protocol environment
      • 2.5.3 Expressions of cryptographic protocols
    • References
  • 3 Engineering Principles for Security Design of Protocols
    • 3.1 Introduction of engineering principles
      • 3.1.1 Prudent engineering principles
      • 3.1.2 Cryptographic protocol engineering principles
    • 3.2 Protocol engineering requirement analysis
      • 3.2.1 Security requirement analysis
      • 3.2.2 Plaintext analysis
      • 3.2.3 Application environment analysis
      • 3.2.4 Attack model and adversary abilities analysis
      • 3.2.5 Cryptographic service requirement analysis
    • 3.3 Detailed protocol design
      • 3.3.1 Liveness of the principal's identity
      • 3.3.2 Freshness and association of time-variant parameter
      • 3.3.3 Data integrity protection of message
      • 3.3.4 Stepwise re¯nement
    • 3.4 Provable security
    • References
  • 4 Informal Analysis Schemes of Cryptographic Protocols
    • 4.1 The security of cryptographic protocols
      • 4.1.1 Authenticity and con¯dentiality under computational model
      • 4.1.2 Security de¯nitions
    • 4.2 Security mechanism based on trusted freshenss
      • 4.2.1 Notions
      • 4.2.2 Freshness principle
      • 4.2.3 Security of authentication protocol
      • 4.2.4 Manual analysis based on trusted freshness
      • 4.2.5 Application of security analysis based on trusted freshness
    • 4.3 Analysis of classic attacks
      • 4.3.1 Man in the middle attack
      • 4.3.2 Source-substitution attack
      • 4.3.3 Message replay attack
      • 4.3.4 Parallel session attack
      • 4.3.5 Re°ection attack
      • 4.3.6 Interleaving attack
      • 4.3.7 Attack due to type °aw
      • 4.3.8 Attack due to name omission
      • 4.3.9 Attack due to misuse of cryptographic services
      • 4.3.10 Security analysis of other protocols
    • References
  • 5 Security Analysis of Real World Protocols
    • 5.1 Secure Socket Layer and Transport Layer Security
      • 5.1.1 SSL and TLS overview
      • 5.1.2 The SSL handshake protocol
      • 5.1.3 Security analysis of SSL based on trusted freshness
    • 5.2 Internet Protocol Security
      • 5.2.1 IPSec overview
      • 5.2.2 Internet Key Exchange
      • 5.2.3 Security analysis of IKE based on trusted freshness
    • 5.3 Kerberos|the network authentication protocol
      • 5.3.1 Kerberos overview
      • 5.3.2 Basic Kerberos network authentication service
      • 5.3.3 Security analysis of Kerberos based on trusted freshness
      • 5.3.4 Public-key Kerberos
    • References
  • 6 Guarantee of Cryptographic Protocol Security
    • 6.1 Security de¯nition of authentication
      • 6.1.1 Formal modeling of protocols
      • 6.1.2 Formal modeling of communications
      • 6.1.3 Formal modeling of entity authentication
    • 6.2 Security de¯nition of SK-security
      • 6.2.1 Protocol and adversary models in CK model
      • 6.2.2 SK-security in CK model
    • 6.3 Authentication based on trusted freshness
      • 6.3.1 Trusted freshness
      • 6.3.2 Liveness of principal
      • 6.3.3 Con¯dentiality of freshness identi¯er
      • 6.3.4 Freshness of freshness identi¯er
      • 6.3.5 Association of freshness identi¯er
      • 6.3.6 Security analysis based on trusted freshness
      • 6.3.7 De¯nition of security
      • 6.3.8 Non-repudiation based on trusted freshness
    • References
  • 7 Formalism of Protocol Security Analysis
    • 7.1 BAN logic
      • 7.1.1 Basic notation
      • 7.1.2 Logical postulate
      • 7.1.3 Steps for security analysis based on BAN logic
      • 7.1.4 BAN-like logic
    • 7.2 Model checking
    • 7.3 Theorem proving
    • 7.4 Belief multisets based on trusted freshness
      • 7.4.1 Belief logic language
      • 7.4.2 Logical postulate
    • 7.5 Applications of belief multiset formalism
      • 7.5.1 Analysis of Needham-Schroeder public-key protocol
      • 7.5.2 Analysis of Kerberos pair-key agreement in DSNs
      • 7.5.3 Analysis of authentication in IEEE 802.11i
    • 7.6 Comparison
    • References
  • 8 Design of Cryptographic Protocols Based on Trusted Freshness
    • 8.1 Previously known methods for protocol design
      • 8.1.1 A simple logic for authentication protocol design
      • 8.1.2 Fail-stop protocol design
      • 8.1.3 Authentication test
      • 8.1.4 Canetti-Krawczyk model
      • 8.1.5 Models for secure protocol design and their compositions
    • 8.2 Security properties to achieve in protocol design
      • 8.2.1 Con¯dentiality
      • 8.2.2 Data integrity
      • 8.2.3 Data origin authentication
      • 8.2.4 Entity authentication
      • 8.2.5 Origin entity authentication
      • 8.2.6 Non-repudiation
      • 8.2.7 Access control
      • 8.2.8 Key establishment
      • 8.2.9 Fairness
    • 8.3 Protocol design based on trusted freshness
      • 8.3.1 Notations and descriptions
      • 8.3.2 Design of cryptographic protocols
      • 8.3.3 Lower bounds for SK-secure protocols
    • 8.4 Application of protocol design via trusted freshness
      • 8.4.1 Construction of a two-party key establishment protocol
    • References
  • 9 Automated Analysis of Cryptographic Protocols Based on Trusted Freshness
    • 9.1 Previously known methods for automated analysis
      • 9.1.1 Automated analysis tool based on logic
      • 9.1.2 Automated analysis tool based on model checking
      • 9.1.3 Automated analysis tool based on theorem proving
      • 9.1.4 CAPSL speci¯cation language
    • 9.2 Automated cryptographic protocol analysis based on trusted freshness
      • 9.2.1 Analyzer frame based on belief multiset formalism
      • 9.2.2 Comparision of two initial implementations of BMF
      • 9.2.3 Implementation of the belief multiset formalism
    • References
  • Index

相关图书