《密码协议：基于可信任新鲜性的安全性分析（英文版）》主要介绍如何利用系统工程思想和可信任新鲜性的方法，分析和设计密码通信协议。作者基于可信任的新 鲜性标识符概念，提出了一个新颖的新鲜性原则。该原则指出了一种有效的、易用的密码协议安全性分析方法。使用这种分析方法，可以有效检验协议在实际应用中 能否满足安全需要。此外，书中给出大量的分析实0例，详细说明如何基于概率定义安全性，如何将安全指标定量化，如何针对具体的协议寻找漏洞，如何自动实现 协议漏洞的查找，等等。
《密码协议：基于可信任新鲜性的安全性分析（英文版）》总结了作者近年来的研究成果，这些成果的有效性和易用性对从事通信协议安全性研究的人员，特别是工 程技术人员，具有很好的参考和实用价值。董玲网络系统建设和信息安全领域高级工程师，上海交通大学密码与信息安全实验室兼职教授、研究兴趣是信息安全和应 用密码学，特别是实际应用的密码通信协议和密码系统的安全性分析。陈克非上海交通大学计算机科学与工程系教授，长期从事密码与信息安全理论研究。主要研究 兴趣是序列密码、可证明安全、密码协议分析、数据安全。近年来承担多项国家自然科学基金、国家高技术研究发展计划（863计划），发表学术论文150多 篇，编辑出版学术著作7部。
- l Introduction of Cryptographic Protocols
- 1.1 Information security and cryptography
- 1.2 Classes of cryptographic protocols
- 1.2.1 Authentication protocol
- 1.2.2 Kev 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 protoco
- 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 ofprotoc01 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 Plailltext 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 neshness 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 protoc01
- 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
- ……
- 5 Security Analysis of Real World Protocols
- 6 Guarantee of Cryptographic Protocol Security
- 7 Formalism of Protocol Security Analysis
- 8 Design of Cryptographic Protocols Based on Trusted
- 9 Automated Analysis of Cryptographic Protocols
- Index
