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

.2.2.5 hash functions
2.2.6 message authentication
2.3 cryptographic protocols
2.3.1secure 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
3engineering 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.4attack 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.
4informal analysis schemes of cryptographic protocols
4.1 the security of cryptographic protocols
4.1.1authenticity and confidentiality under computational model
4.1.2 security definitions
4.2 security mechanism based on trusted freshenss
4.2.1notions
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.2source-substitution attack
4.3.3message replay attack
4.3.4parallel session attack
4.3.5reflection attack
4.3.6interleaving attack
4.3.7attack due to type flaw
4.3.8attack due to name omission
4.3.9attack due to misuse of cryptographic services
4.3.10security analysis of other protocols
references
security analysis of real world protocols
5.1secure socket layer and transport layer security
5.1.1ssl and tls overview
5.1.2the ssl handshake protocol
5.1.3security analysis of ssl based on trusted freshness
5.2internet protocol security
5.2.1ipsee overview
5.2.2internet key exchange
5.2.3security analysis of ike based on trusted freshness
5.3kerberos--the network authentication protocol
5.3.1kerberos overview
5.3.2basic kerberos network authentication service
5.3.3security analysis of kerberos based on trusted
freshness
5.3.4public-key kerberos
references
guarantee of cryptographic protocol security
6.1security definition of authentication
6.1.1formal modeling of protocols
6.1.2formal modeling of communications
6.1.3formal modeling of entity authentication
6.2security definition of sk-security
6.2.1protocol and adversary models in ck model
6.2.2sk-security in ck model
6.3authentication based on trusted freshness
6.3.1trusted freshness
6.3.2liveness of principal
6.3.3confidentiality of freshness identifier
6.3.4freshness of freshness identifier
6.3.5association of freshness identifier
6.3.6security analysis based on trusted freshness
6.3.7definition of security
6.3.8non-repudiation based on trusted freshness
references
7formalism of protocol security analysis
7.1ban logic
7.1.1basic notation
7.1.2' logical postulate
7.1.3steps for security analysis based on ban logic
7.1.4ban-like logic
7.2model checking
7.3theorem proving
7.4belief multisets based on trusted freshness
7.4.1belief logic language
7.4.2logical postulate
7.5applications of belief multiset formalism
7.5.1analysis of needham-schroeder public-key protocol
7.5.2analysis of kerberos pair-key agreement in dsns
7.5.3analysis of authentication in ieee 802.11i
7.6comparison
references
design of cryptographic protocols based on trusted
freshness
8.1previously known methods for protocol design
8.1.1a simple logic for authentication protocol design
8.1.2fail-stop protocol design
8.1.3authentication test
8.1.4canetti-krawczyk model
8.1.5models for secure protocol design and their compositions
8.2security properties to achieve in protocol design
8.2.1confidentiality
8.2.2data integrity
8.2.3data origin authentication
8.2.4entity authentication
8.2.5origin entity authentication
8.2.6non-repudiation
8.2.7access control
8.2.8key establishment
8.2.9fairness
8.3protocol design based on trusted freshness
8.3.1notations and descriptions
8.3.2design of cryptographie protocols
8.3.3lower bounds for sk-secure protocols
8.4application of protocol design via trusted freshness
8.4.1construction of a two-party key establishment protocol
references
9automated analysis of cryptographic protocols based on trusted freshness
9.1previously known methods for automated analysis
9.1.1automated analysis tool based on logic
9.1.2automated analysis tool based on model checking
9.1.3automated analysis tool based on theorem proving
9.1.4capsl specification language
9.2automated cryptographic protocol analysis based on
trusted freshness
9.2.1analyzer frame based on belief multiset formalism
9.2.2comparision of two initial implementations of bmf
9.2.3implementation of the belief multiset formalism
references
index