Research On Design And Analysis Of Security Protocol For Mobile Banking

The security protocol, which is a crucial basis in mobile banking services, determines the security properties or even the fate of whole system. Thus, in the development of a mobile banking system, elaborate designing and complete analyzing of its security protocol are undoubtedly indispensable. But at present, many mobile banking systems only use some cryptographic algorithms as security measures, without depicting the procedure of message exchanging as a secuity protocol, needless to say how to analyze it or provide the correctness proof of it. Moreover, the method of choosing and using cryptographic algorithms fail to make customers feel safe. And besides, the whole system can't resist all the possible attacks, especially replay attack.Therefore, in this thesis, we investigate the runtime environment of mobile banking systems, study the design and analysis methods of security protocols and the security properties of cryptographic algorithms required, choose a suite of cryptographic algorithms deliberately, and hereby propose a security protocol for mobile banking services - the MB protocol. We discuss the important designing technologies used in MB-protocol and compare it with protocols related.Then we give a rigorous proof of correctness MB protocol based on strand space model. The correctness of MB protocol can be considered as the following two aspects: correspondence and secrecy. Correspondence means that each time a principal B completes a run of the protocol as responder using x, which to B appears to be a run with A, then there is a unique run of the protocol with the principal A as initiator using x, which to A appears to be a run with B. Secrecy means that messages protected by the protocol can be known by any penetrator. One thing should be pointed out is that the correctness proof based on Strand space is valid only on the attack set already known.In addition, we give the nonrepudiation proof using Kailar logic. Although the proof based on logic is only a prerequisite to security, it can enhance users' confidence considerably. Furthermore, we analyze its efficiency and its ability to resist replay attacks. Finally, we realize a prototype of mobile banking system using MB protocol. The conclusions we have drawn is that MB protocol achieves its security goals, has the ability to resist usual attacks and enjoys high efficiency.The main research works are as follows: We study the mathematic background, basic principles and security properties of common cryptographies, and explain the reason why they are chosen to construct the MB protocol. We study the concept, characteristics, design and analysis method of security protocols and describe detailedly the Kailar logic and the strand space model theory, which represents the trend of formal methods of security protocols. According to the principles of security protocols designing and the characteristics of the true runtime environment of mobile banking, we design a security protocol for mobile banking systems and discuss the important techniques used in designing. Then we compare it with other related protocols. Give out a correctness proof for the protocol based on the strand space model theoryand Kailar logic. Using mobile telephone simulator, we realize a prototype of mobile banking system based on J2ME platform.