Logical Approach In The Security Analysis Of Cryptographic Protocols - A New Ban-like Logic

This paper discusses the shortcomings of the existed BAN-like logic systems, and then proposes a new semantics of BAN-like logic system which is designed to be more perfection.Firstly, my paper proposes the imperfection of existed BAN-like logic systems, and analyzes what reasons have caused the imperfection. Here the author gives lots of new opinions.Secondly, my paper establishes the theoretical basis of the BAN-like logic. In the paper a new symbol system, which includes a second order predicate, is given. And the authentication logic system is taken to be an interpretation to the symbol system, which is designed to be an extension of the arithmetic system and the formal set theory system. Therefore the mathematic logic theory is now becoming the basis of my authentication logic system.Thirdly, my paper clarifies the semantics of authentication logic system. In the paper, some simple and explicit statements, which can construct all other composite statements, are given for the first time.Fourthly, my paper proposes a new axiom system, which is made from forty axioms and two rules. All the axioms are divided to eighteen classes. Each class describes the functions of an authentication predicate or the properties of some special sets and cryptographic functions. The system is soundness, because every axiom is a true statement under the interpretation of the authentication logic system.Fiflhly, my paper classifies some cryptographic protocols more specifically. And then the goals of each class are defined uniformly. At last the protocol security is defined according to the respective goals.Finally, my paper analyzes the securities of many cryptographic protocols, especially the identification authentication protocols and the session key establishment protocols, and finds that many protocols is insecure. At the same time some other protocols are analyzed using my logic method, such as electronic voting protocol, email protocol and non-repudiation protocol. It shows that my logic method is effective and useful and is widely applicable to many kind of cryptographic protocols.The most important is that my logic method needn to idealize the protocol before analyzing it.