董玲、陈克非编著的《密码协议：基于可信任新鲜性的安全性分析（英文版）》主要介绍如何利用系统工程思想和可信任新鲜性的方法，分析和设计密码通信协议。指出了一种有效的、易用的密码协议安全性分析方法。使用这种分析方法，可以有效检验协议在实际应用中能否满足安全需要。此外，书中给出大量的分析实例，详细说明如何基于概率定义安全性，如何将安全指标定量化，如何针对具体的协议寻找漏洞，如何自动实现协议漏洞的查找，等等。

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

《密码协议：基于可信任新鲜性的安全性分析（英文版）》总结了作者近年来的研究成果，这些成果的有效性和易用性对从事通信协议安全性研究的人员，特别是工程技术人员，具有很好的参考和实用价值。

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 pretocol

1.2.3 Electronic commerce prctocol

1.2.4 SecuIe multi-party protocol

 1.3 Security of cryptographic pratocols

 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 lesponse

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 prctocols

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 refinement

 3.4 Provable security

 References

4 Informal Analysis Schemes of Cryptographic Protocols

 4.1 The security of cryptographic protocols

4.1.1 Authenticity and confidentiality under computational model

4.1.2 Security definitions

 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 Reflection attack

4.3.6 Interleaving attack

4.3.7 Attack due to type flaw

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 definition 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 definition 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 Confidentiality of freshness identifier

6.3.4 Freshness of freshness identifier

6.3.5 Association of freshness identifier

6.3.6 Security analysis based on trusted freshness

6.3.7 Definition 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 Confidentiality

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 specification 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