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