A Security Analysis Method for Security Protocol Implementations Based on Message Construction

Security protocols are integral to the protection of cyberspace against malicious attacks. Therefore, it is important to be confident in the security of a security protocol. In previous years, people have worked on security of security protocol abstract specification. However, in recent years, people have found that this is not enough and have begun focusing on security protocol implementation. In order to evaluate the security of security protocol implementations, in this paper, firstly, we proposed the Message Construction to Security Protocol Implementation (MCSPI), a message construction method based on application programming interface (API) traces, which automatically generates the constructed client valid request messages. Then, we presented the Security Analysis Scheme (SAS), a security analysis scheme that generates an abstract model of a security protocol server. Next, we proposed a security analysis method to evaluate the security of security protocol implementations on the basis of constructed client request messages generated with MCSPI, corresponding to the server-side response message and server-side abstract model produced by SAS. Finally, we implemented the Security Protocol Implementation Analysis (SPIA) tool to generate client valid request messages and a server-side abstract model to assist in evaluating security protocol implementations. In our experiments, we tested Tencent QQ mail system version 2017 and RSAAuth system and found that RSAAuth is vulnerable and its server has only security checks for user password, while Tencent QQ mail system version 2017 is more secure and has strong security restrictions at server-side besides security checks for user password