Cryptographic Protocol Engineering Andprotocol Security Based On Trusted Freshness

The security research of cryptographic protocols is becoming one of the hottest reasearch spots in network security field. This dissertation mainly discusses how to analyze and design cryptographic protocols based on the idea of system engineering and formal methods. The main results that the author obtainted are as follows:1. Based on the idea of system engineering and the previous presented principles, we present and illustrate 10 cryptographic protocol engineering principles in three groups: 5 cryptographic protocol security requirement analysis principles, 4 detailed protocol design principles and 1 provable security principle. Cryptographic protocol engineering is a new notion introduced in this thesis for cryptographic protocol design, which is derived from software engineering idea. The idea is useful in that it can indicate implicit assumptions behind cryptographic protocol design, and present operational principles on uncovering these subtleties.2. A novel freshness principle based on trusted freshness component is presented: for each participant of a cryptographic protocol, the security of the protocol depends only on the sent or received one-way transformation of a message, which includes certain trusted freshness component. The freshness principle indicates an efficient and easy method to analyze the security of cryptographic protocols and the analysis results of 20 classical cryptographic protocols are illustrated while 12 possible attacks or flaws are new. The freshness principle has following characteristic: it could efficiently distinguish the freshness of the messages to avoid replay attacks and interleaving attacks etc., and the analysis procedure is independent of the concrete formalization of the protocol concurrent runs and the adversarys' possible behaviors. The security analysis results based on the freshness principle can either establish the correctness of the protocol when it is in fact correct, or identify the absence of the security properties and the structure to construct attacks based on the absence.3. Based on the freshness principle, a belief multisets formalism is presented. We have shown the efficiency, rigorousness, automation possibility of the belief multisets formalism by illustrating it via the Needham-Schroeder public key protocol. With the open medium transmission and packet loss considerations in mind, we present an extensible belief multisets formalism including DOS-tolerant property and consistency property analysis that is suitable for wireless protocol analysis.4. Security goals are presented accurately, which are proved not only necessary but also substantial to guarantee the security adequacy of the cryptographic protocols to 4 security definitions under the computational model. These 4 definiitons are presented based on matching conversation definition and indistinguishability security definition.5. A general model for automation of the belief multisets fomalism is presented. Via the comparison of our two partial implementations of the automation of the belief multisets fomalism under the different development environments, a detail implementation approach is determined. The developing automation of the belief multisets fomalism has successfully analyzed several cryptographic protocols.6. Based on the freshness principle and the treatment of the distributed logic time causal consistency, a model for designing cryptographic protocols is also proposed. We exemplify the usability of the model via redesigning the Needham-Schroeder public-key protocol, and prove that the reconstructed challenge-response key exchange protocol achieves the lower bounds of three messages and three rounds.