The Research On BAN-like Logics

Along with the rapid development of e-commerce in the global, e-commerce security problems are attracting increasing attention. Secure protocols are the base to ensure the security of e-commerce activities. Formal Analysis of secure protocol is a powerful tool for testing the security. Meanwhile, with the development of e-commerce, lots of new cryptographic algorithms and signature scheme are proposed, which cause more attention to the nature of security.Secure protocol used mainly symmetric cryptography, public-key cryptography, signatures and hash function. These apply to different use of cryptography. Symmetric cryptography is suitable for a large number of data encryption, but its transmission is the key issue; public-key encryption system as slowly, generally is used for authentication or key distribution; hash function is used in testing the integrity of the messages, testing origin certification of messages; the signature is used to authenticate participants in the e-commerce.Formal analysis of two models: a symbols methods model and a calculation methods model. One of the symbols methods model, the logic method is an effective formal analysis method which mainly includes BAN-like logics. BAN logic, GNY logic, AT logic, VO logic and SVO logic is typical in the BAN-like logic. These logics are based on BAN logic. Among them, SVO logic is the most perfect in BAN-like logic, simple and easy to expand. This paper is mainly an analysis of BAN-like logic.The following is the main work of this paper:1) The natures of the secure protocol are confidentiality, integrity, authentication and non-repudiation and so on. In this paper, we propose that BAN-like logics have two obvious flaws: the lack of the environment model and the lack of the analysis of the integrity. In the BAN-like logics, the participation of protocol is assumed to be honest, this could negate some of the attackers were the main means of the possibility that protocol, but in the world of networks, this assumption is not completely realized. So we need to build an environment model for BAN-like logics. In addition, In BAN-like logics, they assume the cryptographic algorithm used is perfect. Researchers generally believe under these conditions the integrity and confidentiality of the protocol has been guaranteed; however, due to the different natures of various cryptographic systems, integrity cannot be assured through encryption. Especially, BAN-like logics are based on the assumption that the two ciphertext messages arrived in two pieces, this has not guarantee the integrity of the information.2) To build an environment models, we made a model improved Dolev-Yao model to be the environment model of BAN-like logics. One of the improvements is that not the specific algorithms but the cryptographic system used in the analysis should be considered while doing the protocol analysis. The other improvement is to build a fairly complete saboteur behavior model to make the environment more realistic.3) To the lack of integrity analysis, this paper improve the SVO logic , establishing the semantics, syntax of integrity and the integrity axioms, improving the Nonce Verification axioms. Finally, we improve the Otway-Rees protocol increasing the integrity and analysis it using the improved SVO logic.