Security Analysis Of Security Protocol Implementations Based On Massage Construction

Security protocol is the necessary part of Cyberspace security,which is the key issue to protect Cyberspace security from evil attacking.About the aspect of designation and the security analysis of abstract specification of security protocol implementations(programing code),people's researches mainly focus on security analysis and verification of the abstract specifications of security protocol.But,these works cannot mainly focus on the secrecy of security protocol implementations which have strong practicalities.The reasons is that although the secrecy of abstract specification of security protocol has been proved,there maybe have some security issues when security protocol have been implemented in some security system.To prevent the occurrence of these problems,the implementations of security protocol need to analyzed to get the strongly practicality implementations of security protocol.So far,implementation of security protocol mainly extracted and understudied by hand,which existing some error in implementation exactly understanding,because the limitations of the pre-acknowledge mode of security protocol.Even,some user-defined cryptographic primitives were adopted by some private protocol to enhance security of security protocol,because the non-integrity of pre-acknowledgement of user-defined cryptographic primitives,which are difficult understanding the semantic features and protocol specification of security protocols implementations.Therefore,a security analysis method based on message construction was presented for the implementations of security protocol in this thesis,the mainly works are as follows:(1)Present a security protocol message construction method based on API trace-MCSPI.Firstly,we intercept communication message of security protocol and parse it to generate message tokens.Next,we extract cryptographic primitive implementations through scanning client implementations of security protocol to generate dependences of cryptographic primitive implementations and API traces using API tracing technology,meanwhile,and propose an API trace parse algorithm-ATPA to parse generated API traces and build a stack to store parsed data.Then,we locate and label message token to be replaced in the process of message construction.Besides,we reconstruct output of cryptographic primitive implementations on the basis of built stack and dependences.Finally,we use reconstructed output to replace labeled message token to generate constructed request message.(2)Propose a method to analyze security of security protocol implementations based on MCSPI to generate abstract model of security protocol server.Firstly,we intercept and parse response message sent to client by server.Then,we extract process methods about cryptographic primitive contain in request message.Finally,we produce abstract model of security protocol using extracted process methods.(3)Design and develop SPIA tool based on proposed methods to evaluate secrecy of security protocol implementations,which consists of net-trace parse module,API trace parse module,token location module,function output reconstruction module and server abstract model generation module.(4)We analyze five security systems using SPIA tool and generate corresponding abstract model.Apart from that,the analyzed security systems have the correspongding process to cryptgraphic primitives contained in client request messages,but these security systems are vulnerable to password brute-forcing except Tencent QQ mail system version 2017.Besides that,Tencent QQ mail system strictly limit the livetime of login request,the login session will invalidate if request message can not login system in livetime,which can reduce the success rate of password brute-forcing and it can slowdown the password bruteforcing in some degree.