## 1 Introduction  
Security protocols constitute a key part of cyberspace security [1] and are an important method to protect the cyberspace security against malicious attacks. Hence, people are very interested in their security. The classic method for analyzing security protocols is the formal method. However, some researchers have shown that many security protocols proved with formal methods are still not secure in practice owing to incorrect implementations [2]. Apart from that, due to the capability limitation of developers, there may be inconsistencies between security protocol implementations and the abstract specification of security protocols. So, just proof of security properties of a security protocol with formal methods is not enough to provide confidence in its security. Therefore, verifying security and detecting vulnerabilities of security protocol implementations are significant to cyberspace security [3] and have attracted widespread attention from researchers and developers. In general, security protocol implementation consists of client-side and server-side implementation. Thus, we can study the security of security protocol implementations based on one of the following four assumptions:  
1. Do not have client-side implementations and server-side implementations. 2. Have both client-side implementations and server-side implementations. 3. Have the client-side implementations but not the server-side implementation. 4. Have the server-side implementations but not the client-side implementation. After examining many security applications, especially based on browser/server (B/S) model applications, we found that assumption (3) is suitable for most cases because it is very difficult for researchers to get the server-side implementations in practical applications, but it is relatively easy to get the client-side implementations. Hence, we focus on security analysis with assumption (3). The methods of analyzing the security of a security protocol mainly include program analysis (code analysis), software test analysis, a model extraction method [4], execution trace analysis, and net-trace analysis [5]. [PERSON] et al. [6] analyzed the security of the Facebook login protocol in Android and recovered a specification of the Facebook login protocol based on Client JavaScript implementations, but it is not suitable for PC platforms. [PERSON] et al. [7] proposed an approach to detect vulnerabilities by modifying the arguments of request messages from client to server. [PERSON] et al. [8] developed AuthScan to recover abstract specifications of security protocols using security protocol client JavaScript implementations; however, AuthScan does not fully dig into the knowledge of cryptographic primitive JavaScript implementations. [PERSON] et al. [9] proposed a model extraction method to transform security protocol ProScript implementations to Applied PI calculus and Blanchet calculus, respectively. Then, ProVerif and CryptoVerif were used to analyze the security of security protocol ProScript implementations, but they also did not pay attention to the internal structures of cryptographic primitive ProScript implementations. Based on the previous typical analysis, we found that the client-side implementations were not fully used to evaluate the security of security protocol implementations and to extract accurately the abstract model from client-side implementations for analyzing security protocol implementations. Therefore, we proposed a security analysis method based on API traces in which we used the knowledge of the internal structures of cryptographic primitive implementations to reconstruct its outputs for evaluating the security protocol implementations. The main contributions are as follows:  
1. Present the state-of-the-art security analysis method of security protocol implementations and point out that existing researchers have not taken into consideration the internal structures of cryptographic primitive implementations to analyze the security of security protocol implementations. 2.