| Third-party payment is convenient and practical,which makes plenty of mobile applications choose to embed the third-party payment functions,but its security lacks of systematic and comprehensive analysis,which makes it difficult to guarantee the security of payment.To solve this issue,we present a formal analysis of five third-party payment protocols based on Android platform by formalizing its security assumptions and security goals,and modeling the protocol flows using ProVerif.Our analysis results show that the implementation of the protocol on Android platform is difficult to resist the attacks of order tampering,order replacement and notification forgery.Secondly,after testing 210 Apps that use In-app third-party payment protocols,14% of them are found to be unable to resist these attacks.Finally,in order to resist the above attacks,specific suggestions are put forward for the implementation of the third-party payment protocol.The main research work and achievements of this paper are as follows:1)Combing the third-party online payment protocol process:the third-party payment platform does not provide standardized protocol process.This paper combs out the third-party online payment protocol process by referring to the access documentation and API interface documentation provided by the third-party payment platform.2)This paper analyzes the security assumptions and goals of the protocol:the documents of the third-party payment platform do not explicitly describe the security assumptions and goals of the protocol.This paper refines the documents and obtains the security assumptions and goals of the protocol based on the actual situation of the protocol.3)Formal modeling and analysis of the third-party online payment protocol:This paper uses ProVerif formal analysis tool to model the protocol process and security objectives,and questions the security objectives.The results show that the security objectives can not be achieved under some security assumptions.At the same time,three kinds of potential attack paths are obtained by formal analysis.This paper proves that the attack can be realized by attack measurement.4)Suggestions for the third-party payment platform and developers are provided:on the basis of the above work,suggestions on protocol standardization for the third-party payment platform and security development for the developers are put forward. |