《密码协议：基于可信任新鲜性的安全性分析（英文版）》主要介绍如何利用系统工程思想和可信任新鲜性的方法，分析和设计密码通信协议。作者基于可信任的新 鲜性标识符概念，提出了一个新颖的新鲜性原则。该原则指出了一种有效的、易用的密码协议安全性分析方法。使用这种分析方法，可以有效检验协议在实际应用中 能否满足安全需要。此外，书中给出大量的分析实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

信息安全系列