# A New Method to Analyze the Security of Protocol Implementations Based on Ideal Trace

Authors: Fusheng Wu; Huanguo Zhang; Wengqing Wang; Jianwei Jia; Shi Yuan
Journal: Security and Communication Networks
 (2017)

---

## Abstract

The security analysis of protocols on theory level cannot guarantee the security of protocol implementations. To solve this problem, researchers have done a lot, and many achievements have been reached in this field, such as model extraction and code generation. However, the existing methods do not take the security of protocol implementations into account. In this paper, we have proposed to exploit the traces of function return values to analyze the security of protocol implementations at the source code level. Taking classic protocols into consideration, for example (like the Needham-Schroeder protocol and the Diffie-Hellman protocol, which cannot resist man-in-the-middle attacks), we have analyzed man-in-the-middle attacks during the protocol implementations and have carried out experiments. It has been shown in the experiments that our new method works well. Different from other methods of analyzing the security of protocol implementations in the literatures, our new method can avoid some flaws of program languages (like C language memory access, pointer analysis, etc.) and dynamically analyze the security of protocol implementations.


---

## Body

## 1. Introduction

With the fast development of the network communication, information security is becoming more and more important [1, 2]. To protect the network information from attacks, protocols are usually applied. However, general methods (e.g., formal method, computational model, and computational soundness formal) cannot guarantee the security of protocols during the process of their implementations. That is, even if protocols have been theoretically proved to be secure, some insecure factors (like the language characteristics of protocols’ source codes, the operating environments of the protocol implementations) arise when implementing them at the source code level. Therefore, researchers focus on the security analysis of protocol implementations at the source code level [3].During implementing at the source code level, it is difficult to guarantee the security of protocol specifications due to language characteristics (such as C language memory access, pointer analysis, etc.). Hence, it is more complex to analyze the security of protocol implementations at the source code level compared to that of protocols on the theoretical level. To avoid these insecure factors that languages bring, some methods have been proposed to analyze the security of protocol implementations at the source code level. Among them are two representatives: model extraction and code generation. Model extraction is applied to avoid the problem of concrete state space explosion. During the extracting process, an abstract mapping is set up to map a concrete protocol model onto a corresponding abstract model and its properties onto corresponding abstract properties. If the security properties of the protocols on the abstract model have been proved to be sound and the abstract mapping has been proved to be reliable, then the security properties on the concrete model are proved. It guarantees the security of the protocol implementation and provides its reliability’s demonstration. Related research achievements include [4–7]. Sometimes leaks arise in the process of protocol implementations due to the design imperfection, which leads protocol implementations to be insecure (such as the SSL protocol, the TLS protocol). To avoid these cases, code generation is applied. That is, protocol specifications are analyzed before implementations. After that, refined mapping and some related running choices (like concrete program languages or running environments) are applied to map a program abstract model onto a corresponding concrete model and its abstract properties onto corresponding concrete properties. If the security properties of the protocol on the abstract model have been proved to be sound and the mapping has been proved to be reliable, the properties on the concrete model are proved. Related research achievements include [8–10]. Now model extraction and code generation have been widely applied to protocol security analysis. However, neither model extraction nor code generation can guarantee the security of protocol implementations due to program language flaws, which causes the gap between the protocol security analysis on theoretical level and the security analysis of the protocol implementations at the source code level [11, 12].The thought of our new method to analyze the security of protocol implementations at the source code level derives from a daily life phenomenon. When an object moves from A to B in an environment without any barriers (called the ideal environment), a trace will be produced by the object, which is called the ideal trace. In nonideal environments, the object will be attacked by a third party, and its trace (called nonideal trace) will deviate from the ideal trace (the detailed definitions of ideal trace and nonideal trace are given in Section5). If the moving behavior is rectified after the object is attacked, the degree of deviation of its nonideal trace from the ideal trace will become smaller. Based on the thought above, we propose a new method to analyze the security of protocol implementations by means of the traces. The traces consist of the sets of function return values when implementing a protocol. Our new method is carried out like this: we exploit the ideal trace and the method of cluster analysis (including the degree of deviation and the similarity of the trace sequences) as the evaluated reference to analyze protocol security. To prove our new method, with strong simulation of π-calculus we refine the source codes of the Needham-Schroder protocol as an example and set up the security analysis model of protocol implementations with labelled transition systems [13]. Besides, taking the Needham-Schroder protocol and the Diffie-Hellman protocol, for example, we verify man-in-the-middle attacks on OpenSSL with our new method. To describe the specific steps of the security analysis in detail, a flow graph is drawn in Figure 1.Figure 1
The security analysis process of protocol implementations.Our original contributions are as follows:(1) We bring in the ideal trace as the evaluated reference of the security analysis of protocol implementations at the source code level and setting up a bijection of the mapping of events onto traces.(2) We propose a method for analyzing the security of protocol implementations by comparing the similarity and the deviation between nonideal traces and the ideal trace during implementing protocols at the source code level.The remaining work of our article is as follows: a summary of related works in Section2; the preliminaries in Section 3; building a new model in Section 4; the security analysis of protocols in Section 5; taking classical protocol implementations, for example, and doing experiments in Section 6; conclusion and future work in Section 7.


## 2. Related Work

It is practical and valuable to analyze the security of protocol implementations at the source code level. In recent years, researchers focus on this field and here we can find great achievements [14].The security analysis of protocol implementations at the source code level is very complex and different from common protocol security analysis [15], for it must take program language structure and running environment into account, which adds difficulty to the security analysis of protocol implementations. To solve this problem, literature [4] has done some researches, analyzing the security of implementing the Needham-Schroeder protocol written in C language. In literature [4], C language annotations act as trust assertions, and a trust assertion model is established for protocol security analysis by means of Horn Logic. Some researchers have used some function libraries and intermediate languages, like C language, to automatically analyze the security of protocol implementations. This method has avoided the problems that C language structure brings about (like pointer operation, buffer overflow, etc.). The related literatures are [5–7, 16, 17]. Similarly, some researchers have applied the latest techniques or tools to the security analysis of protocol implementations at the source code level, which is a new direction in this field. For example, based on VCC, C language application program interface (API) has been applied to the analysis security of protocol implementations at the source code level. Literature [18] has proposed a general method for protocol security analysis, which has distinguished two different items mapped onto the same array. In literature [19], a general verifying method has been applied to practical TPM and HSMs platforms. Literature [20] has exploited interface constraint and program logic reasoning to analyze the security of protocol implementations at the source code level. To reduce the difficulty brought about by C language structure when analyzing the security of protocol implementations, researchers have exploited C language complier to analyze the security of protocol implementation. The examples are [21, 22].Transport Layer Security (TLS) has been widely put into practice so it is a focus to analyze the security of protocol implementations on the base of TLS. For example, literature [23] has proposed that the OpenSSL crypto library can be applied to the security analysis of implementing TLS in the C language environment. Another example is literature [24], which has proposed to analyze the security of protocols on base of the control-flow integrity of the message authentication codes (MACs). This method has taken it into account that an adversary attack protocols by means of C/C++ pointer and memory leaks during the process of protocol implementations.The methods mentioned above have promoted the research of the security analysis of protocol implementations. However, they cannot settle the security problems that are caused by the inherent flaws of program language structures. Compared with them, our new method can avoid the flaws of program language structure and dynamically analyze the security of protocol implementations at the source code level. Hence, it is helpful and valuable for protocol design, security verification, and security evaluation [25].


## 3. Preliminaries

For better understanding of our new method, it is necessary to have a basic knowledge of labelled transition system, strong simulation, program refinement, and so on.


### 3.1. Labelled Transition System and Strong Simulation

According to the automata theory, a labelled transition system is a system transferring model which consists of start point, input label, and terminal point. But a labelled transition system has no fixed start states and accepting states, which is different from automata. Therefore, any state in a labelled transition system can act as a start state. Therefore, a labelled transition system has an advantage over other systems when dynamically analyzing the security of protocol implementations at the source code level.Definition 1 (labelled transition system [13]).
A labelled transition system (LTS) over Act is a pair(Q,T) consisting of
(1) a set Q of states;
(2) a ternary relation T⊆(Q×Act×Q), known as a transition relation.
If(q,α,q′)∈T, we write q→αq′, and we call q the source and q′ the target of the transition. If q→α1q1→α2⋯→αnqn, then we call qn a derivate of q under α1α2⋯αn.Definition 2 (strong simulation [13]).
Let(Q,T) be an LTS, and let S be a binary relation over Q. Then S is called a strong simulation over (Q,T); if, whenever pSq, p→αp′ then there exists q′∈Q such that q→αq′ and p′Sq′.
We say thatq strongly simulates p if there exists a strong simulation S such that pSq.Definition 3 (extended strong simulation).
Let(Q,T) be an LTS and (Q′,T′) be an LTS and S be a binary relation over Q×Q′, and let p,q∈Q. If pSq satisfies
(1) Q⊆Q′, T⊆T′,
(2) p′,q′∈Q′ and α=α′,α′∈Q′, and if p→αp′, then there exists q′ such that q→αq′ and p′Sq′. Then S is called an extended strong simulation over a 4-tuple (Q,Q′,T,T′).


### 3.2. Program Refinement

When implementing a protocol, it is very difficult to verify its properties in concrete program state space (called the state-explosion problem [26]). Program refinement is exploited to solve this problem. Program refinement, which simplifies two programs with refined relation, is an important technique of verifying programs and is useful to reduce program state space.Definition 4 (program refinement).
Letp be a concrete program, and then there exists p′, a refined program of p. That is, the process from p to p′ is recursive. The behaviors produced by program p′ belong to the subset of the behaviors produced by program p. Therefore, p′ will never produce the behaviors that p cannot produce, and wherever a program p is applied, p′ can be used to replace it. Hence, p′ is called a refined program of p.
According to Definition4, many program verification problems can be reduced to refined verification. For example, the verification of a program or an algorithm is always reduced to the refined relation between programs and protocol specifications. Similarly, there exists refined relation between a protocol implementation and its specifications. To reduce refined relation and refine source codes, we design a refining algorithm of protocol implementations, shown in Algorithm 1.Algorithm 1:The protocol source code refinement algorithm (written in C pseudocode).
Step 1. IniStack(S); // initiate a stack. Here,Srepresents stack.
Step 2. Input file.c; // input a file (protocol source codes)
Step 3. While (judge whether the file of protocol source codes is finished)
i
f (judge whether functions are true) Push(S,f); /∗functions push into the
stack. Here,
f
represents file.
c
.
∗
/
Continue to seek the functions of protocol source codes.
//while
Step 4. While (! StackEmpty(S)) //judge whether the stack is empty.
GetTop(S,f); //pop the functions which are on the top of the stack.
if (the top functions of the stack satisfy protocol specifications) /∗the functions
can reflect the code execution of protocol interactive communication, such as
send
and recv
of socket API.
∗
/
i
d
e
n
t
i
f
y
a
n
d
r
e
s
e
r
v
e
t
h
e
f
u
n
c
t
i
o
n
s
;
Else deletethefunctions;
//whileThe complexity analysis of the algorithm consists of two circulations. One circulation achieves the goal of choosing functions. The other labels the functions which satisfy the condition, and refines source codes. Assuming there existsN functions in the source codes, among these functions, M functions can satisfy protocol specifications (M≤N). The worst case is M=N. Hence, the complexity of the algorithm is O(2N)≈O(N), which is polynomial time. The algorithm can be achieved.


### 3.3. The Program Refinement of Protocol Source Codes

In most cases, the program source codes consist of functions, such as C language source codes, Java language source codes, and F# language source codes. According to the rules of C language program execution, when implementing a protocol, called function return values, the function behaviors are decided, and the sets of called function return values decide the behavior traces of protocol interactive communications. Therefore, if the functions of source codes are refined, the difficulty of the state-explosion problem will be reduced and the security properties of the protocol will not change after refinement. Hence, we can refine a protocol to analyze its security if the refinement relation of source codes exists.Proposition 5.
If the nonfunction part is removed from program source codes, the newly produced program source codes are the refinement of the previous program source codes.Proof.
Assume that the program running is a LTS. That is, let the LTS of the previous program source codes be(Q,T), and let the LTS of the program source codes obtained after removing the nonfunction part be (Q′,T′). Let S be a binary relation over Q×Q′. And there exist Q′⊆Q,  q,q′∈Q, and p, p′∈Q′. Here α and α′, respectively, are the input labels of two program source codes, and α=α′ (called α in the following). According to Definition 1, there exist p→αp′∈T and q→αq′∈T′, as well as qSp and q′Sp′. According to Definition 3, the behaviors generated by LTS (Q′,T′) are the subset of LTS (Q,T), and (Q′,T′) will never produce any behaviors that (Q,T) cannot produce. That is, wherever Q,T is applied, it can be replaced by (Q′,T′). Hence, the proposition is proved.


## 3.1. Labelled Transition System and Strong Simulation

According to the automata theory, a labelled transition system is a system transferring model which consists of start point, input label, and terminal point. But a labelled transition system has no fixed start states and accepting states, which is different from automata. Therefore, any state in a labelled transition system can act as a start state. Therefore, a labelled transition system has an advantage over other systems when dynamically analyzing the security of protocol implementations at the source code level.Definition 1 (labelled transition system [13]).
A labelled transition system (LTS) over Act is a pair(Q,T) consisting of
(1) a set Q of states;
(2) a ternary relation T⊆(Q×Act×Q), known as a transition relation.
If(q,α,q′)∈T, we write q→αq′, and we call q the source and q′ the target of the transition. If q→α1q1→α2⋯→αnqn, then we call qn a derivate of q under α1α2⋯αn.Definition 2 (strong simulation [13]).
Let(Q,T) be an LTS, and let S be a binary relation over Q. Then S is called a strong simulation over (Q,T); if, whenever pSq, p→αp′ then there exists q′∈Q such that q→αq′ and p′Sq′.
We say thatq strongly simulates p if there exists a strong simulation S such that pSq.Definition 3 (extended strong simulation).
Let(Q,T) be an LTS and (Q′,T′) be an LTS and S be a binary relation over Q×Q′, and let p,q∈Q. If pSq satisfies
(1) Q⊆Q′, T⊆T′,
(2) p′,q′∈Q′ and α=α′,α′∈Q′, and if p→αp′, then there exists q′ such that q→αq′ and p′Sq′. Then S is called an extended strong simulation over a 4-tuple (Q,Q′,T,T′).


## 3.2. Program Refinement

When implementing a protocol, it is very difficult to verify its properties in concrete program state space (called the state-explosion problem [26]). Program refinement is exploited to solve this problem. Program refinement, which simplifies two programs with refined relation, is an important technique of verifying programs and is useful to reduce program state space.Definition 4 (program refinement).
Letp be a concrete program, and then there exists p′, a refined program of p. That is, the process from p to p′ is recursive. The behaviors produced by program p′ belong to the subset of the behaviors produced by program p. Therefore, p′ will never produce the behaviors that p cannot produce, and wherever a program p is applied, p′ can be used to replace it. Hence, p′ is called a refined program of p.
According to Definition4, many program verification problems can be reduced to refined verification. For example, the verification of a program or an algorithm is always reduced to the refined relation between programs and protocol specifications. Similarly, there exists refined relation between a protocol implementation and its specifications. To reduce refined relation and refine source codes, we design a refining algorithm of protocol implementations, shown in Algorithm 1.Algorithm 1:The protocol source code refinement algorithm (written in C pseudocode).
Step 1. IniStack(S); // initiate a stack. Here,Srepresents stack.
Step 2. Input file.c; // input a file (protocol source codes)
Step 3. While (judge whether the file of protocol source codes is finished)
i
f (judge whether functions are true) Push(S,f); /∗functions push into the
stack. Here,
f
represents file.
c
.
∗
/
Continue to seek the functions of protocol source codes.
//while
Step 4. While (! StackEmpty(S)) //judge whether the stack is empty.
GetTop(S,f); //pop the functions which are on the top of the stack.
if (the top functions of the stack satisfy protocol specifications) /∗the functions
can reflect the code execution of protocol interactive communication, such as
send
and recv
of socket API.
∗
/
i
d
e
n
t
i
f
y
a
n
d
r
e
s
e
r
v
e
t
h
e
f
u
n
c
t
i
o
n
s
;
Else deletethefunctions;
//whileThe complexity analysis of the algorithm consists of two circulations. One circulation achieves the goal of choosing functions. The other labels the functions which satisfy the condition, and refines source codes. Assuming there existsN functions in the source codes, among these functions, M functions can satisfy protocol specifications (M≤N). The worst case is M=N. Hence, the complexity of the algorithm is O(2N)≈O(N), which is polynomial time. The algorithm can be achieved.


## 3.3. The Program Refinement of Protocol Source Codes

In most cases, the program source codes consist of functions, such as C language source codes, Java language source codes, and F# language source codes. According to the rules of C language program execution, when implementing a protocol, called function return values, the function behaviors are decided, and the sets of called function return values decide the behavior traces of protocol interactive communications. Therefore, if the functions of source codes are refined, the difficulty of the state-explosion problem will be reduced and the security properties of the protocol will not change after refinement. Hence, we can refine a protocol to analyze its security if the refinement relation of source codes exists.Proposition 5.
If the nonfunction part is removed from program source codes, the newly produced program source codes are the refinement of the previous program source codes.Proof.
Assume that the program running is a LTS. That is, let the LTS of the previous program source codes be(Q,T), and let the LTS of the program source codes obtained after removing the nonfunction part be (Q′,T′). Let S be a binary relation over Q×Q′. And there exist Q′⊆Q,  q,q′∈Q, and p, p′∈Q′. Here α and α′, respectively, are the input labels of two program source codes, and α=α′ (called α in the following). According to Definition 1, there exist p→αp′∈T and q→αq′∈T′, as well as qSp and q′Sp′. According to Definition 3, the behaviors generated by LTS (Q′,T′) are the subset of LTS (Q,T), and (Q′,T′) will never produce any behaviors that (Q,T) cannot produce. That is, wherever Q,T is applied, it can be replaced by (Q′,T′). Hence, the proposition is proved.


## 4. Establishing the Model

There are always some faults in a protocol due to its imperfect design. These faults make the protocol vulnerable to malicious third-party attacks. For example, the Needham-Schroeder protocol and the Diffie-Hellman protocol cannot resist man-in-the-middle attacks. To avoid these malicious attacks, it is necessary to analyze the security of a protocol on theory level before its implementations (such as formal, computational model, the computationally sound formal). However, a protocol is not secure when implementing it at the source code level, although it has been proved to be secure on theory level. That is, it is essential to analyze the security of protocol implementations at the source code level.In this paper, a method is proposed by us to analyze the security of protocol implementations at the source code level written in C. Our method establishes models in the following steps: ① describe a protocol symbolically; ② acquire the program source codes of the protocol; ③ refine these source codes; ④ draw the control-flow graph and the state diagram of the protocol; ⑤ establish the model of the traces of the protocol implementations. We take the classic Needham-Schroeder protocol, for example, to show how to establish a model with our new method.


### 4.1. The Protocol Symbolic Description

It is a basic requirement of protocol communications that at least two participants participate in an interactive communication in accordance with certain specifications. Generally, Message Sequence Charts (MSC) of protocol interactive communications are expressed by an ITU-standardized protocol specification language (ITU: International Telecommunication Union) [27] (in this paper, protocol specifications are expressed by the approaches from ITU and literature [28]). The symbolic description of the Needham-Schroeder protocol specifications is shown in Figure 2.Figure 2
The Needham-Schroeder protocol.In Figure2 A and B, respectively, denote two participants of a protocol; pk(A) and pk(B), respectively, denote the public keys of the participants; sk(A) and sk(B), respectively, denote the private keys of the participants; Fresh Na and Fresh Nb, respectively, denote temporary values of A and B; and Na,Apk(B) denotes the encryption of information {|Na,A|} with the public keys of B.


### 4.2. The Refinement of Source Codes

Taking the Needham-Schroeder source codes written in C, for example, we illustrate the refinement of source codes with Algorithm1 and then analyze the security of protocol implementations at the source code level. When writing protocol codes, we exploit the mechanism of RAS public key cryptography for encryption and decryption, and the functions of the OpenSSL crypto library are used while encrypting and decrypting. The protocol runs over OpenSSL. Due to the limited length of this paper, only main source codes are shown in Algorithm 2.Algorithm 2:The part source codes of the Needham-Schroeder protocol.
1int main(int,argc,char argv)
2
3WSADATA wsaData;
4SCOKET client;
5RSA∗R;
6serv.sin_family=AF_INET;
7serv.sin_port=htons(port);
8serv.sin_addr.S_un.S_addr=inet_addr(''127.0.0.1'');
9client=socket(AF_INET,SOCK_STREAM,0);
10connect(client,(structsockaddr∗)&serv,sizeof
(serv));
11Gene_Rand;
12Comp_Str;
13memcpy(plaitxt_A_E,Str_Id,1024);
14public_Encrypt(plaitxt_A_E);
15strcpy(Cipher_buf,(constchar∗)cipher);
16iSend=send(client,Cipher,sizeof(Cipher),0);
17iLen=recv(client,(char∗)cipher,sizeof(cipher),0);
18memcpy(Tcipher_Na_Nb,cipher_Na_Nb,1024);
19Private_Dencrypt_Na_Nb(R,Tciper_Na_Nb);
20memcpy(plaitxt_Nb,StrNb,1024);
21Public_Encrypt_Nb(plaitxt_Nb);
22strcpy(Cipher,(constchar∗)cipher);
23iSend=send(client,Cipher,sizeof(Cipher),0);
24
25int Gene_Rand
26
27BIGNUM∗n;
28int ret,bits=128;
29char∗sn;
30n=BN_new;
31ret=BN_pseudo_rand(n,bits,1,1);
32sn=BN_bn2dec(n);
33strcpy(RandNum,sn);
34return 0;
35
36int Com_Str
37
38strcat(Str_Id,RandNum);
39strcat(Str_Id, ''|A'');
40return 0;
41
42int Public_Encrypt(unsigned char∗s)
43
44RSA∗r;
45int ret,flent,len;
46BIGNUM∗bnn,∗bne;
47bnn=BN_new;
48bne=BN_new;
49ret=BN_dec2bn(&bnn,strn);
50ret=BN_dec2bn(&bnn,stre);
51r=RSA_new;
52r->n=bnn;
53r->e=bne;
54flen=RSA_size(r);
55len=RSA_public_encrypt(flen,s,cipher_A_E,r,3);
56return 0;
57
58int Private_Dencrypt_Na_Nb(RSA∗r,unsigned char∗s)
59
60int len,flen;
61flen=RSA_size(r);
62len=RSA_private_decrypt(flen,s,plaitxt_Na_Nb, r,3);
63return 0;
64
65int StrDivNb(char str)
66
67int k=0,i=0,j=0;
68int strlen=0;
69int Publi_Encrypt_Nb(usigned char∗s)
70
71RSA∗r;
72int ret,flen,len;
73BIGNUM∗bnn,∗bne;
74bnn=BN_new;
75bne=BN_new;
76ret=BN_dec2bn(&bnn,strn);
77ret=BN_dec2bn(&bne,strn);
78r=RSA_new;
79r->n=bnn;
80r->e=bne;
81flen=RSA_size(r);
82len=RSA_public_encrypt(flen,s,cipher_Nb,r,3);
83return 0;
84As is shown in Algorithm2, the source codes of the Needham-Schroeder protocol include many redundant ones. According to Proposition 5 and Algorithm 1, the security analysis of protocol implementations will not be influenced if those redundant codes are deleted. After deletion, the left source codes of the Needham-Schroeder protocol are mainly function codes (shown in Algorithm 3). According to Definition 4, the source codes in Algorithm 3 are the refinement of the source codes in Algorithm 2. In the example of the Needham-Schroeder protocol implementations, the behaviors produced by the source codes in Algorithm 3 are the subset in those produced by the source codes in Algorithm 2. Therefore, we can exploit the traces of function return values produced by the source codes in Algorithm 3 to dynamically analyze the security of the Needham-Schroeder protocol implementations at the source code level.Algorithm 3:The refined part source codes of the Needham-Schroeder protocol.
1int main(int argc,char argc)
2
3connect(client,(struct sockaddr∗)&serv,sizeof(serv));
4Gene_Rand;
5Comp_Str;
6memcpy(plaitxt_A_E,Str_Id,1024);
7Public_Encrypt(plaitxt_A_E);
8strcpy(Cipher_buf,(const char∗)cipher);
9iSend=send(client,Cipher,sizeof(cipher),0);
10iLen=recv(client,(char∗)cipher,sizeof(cipher),0);
11memcpy(Tcipher_Na_Nb,cipher_Na_Nb,1024);
12Private_Dencrypt_Na_Nb(R,Tcipher_Na_Nb);
13memcpy(plaitxt_Nb,StrNb,1024);
14Public_Encrypt_Nb(plaitxt_Nb);
15strcpy(Cipher,(const char∗)cipher);
16iSend=send(client,Cipher,sizeof(Cipher),0);
17
18int Gene_Rand
19
20n=BN_new;
21ret=BN_pseudo_rand(n,bits,1,1);
22sn=BN_bn2dec(n);
23strcpy(RandNum,sn);
24
25int Comp_Str;
26
27strcat(Str_Id,RandNum);
28strcat(Str_Id, ''|A'');
29
30int Public_Encrypt(unsigned char∗s)
31
32bnn=BN_new;
33bne=BN_new;
34ret=BN_dec2bn(&bnn,strn);
35ret=BN_dec2bn(&bne,stre);
36r=RSA_new;
37flen=RSA_size(r);
38len=RSA_public_encrypt(flen,s,cipher_A_E,r,3);
39
40int Private_Dencrypt_Na_Nb(RSA∗r,unsigned char ∗s);
41
42flen=RSA_size(r);
43len=RSA_private_decrypt(flen,s,plaitext_Na_Nb, r,3);
44
45int Public_Encrypt_Nb(unsigned char∗s)
46
47bnn=BN_new;
48bne=BN_new;
49ret=BN_dec2bn(&bnn,strn);
50ret=BN_dec2bn(&bne,stre);
51r=RSA_new;
52flen=RSA_size(r);
53len=RSA_public_encrypt(flen,s,cipher_Nb,r,3);
54According to Definition4 and Proposition 5, the security analysis of protocol implementations after refinement is consistent with that before refinement.


### 4.3. Program Control-Flow Graph

To clearly see the traces of the function return values generated during the protocol implementations, taking the source codes gained after the refinement (in Algorithm3), for example, we draw a program control-flow graph to show the process of calling functions after the refinement, shown in Figure 3.Figure 3
The program control-flow graph.In Figure3, ➜ denotes the control-flow direction of program main functions; “→” denotes the control-flow direction of calling functions; and “⇠” denotes the control-flow direction of function returning.As is shown in the program control-flow graph, there are only two types of function return values: ① deterministic return values (like numerical values, alphabets, symbols, etc.); ② nondeterministic return values (such as calling functions directly or indirectly). When function return values are not deterministic, functions will continue to call other functions until the function return values become deterministic.


### 4.4. From the Control-Flow Graph to the State Graph

From Figure3, we can clearly see the traces of the protocol implementations at the source code level and the state of how functions are called. According to C language grammar and program executive rules, in the normal process of program implementations every called function has a return value (deterministic or nondeterministic) and the implementation of every function is related to its return value. When a function receives its return value, the program will execute next step in order. Every function can be regarded as a state node, and function return values can be regarded as input labels. In this case, the program control-flow graph is just like an automata state graph. As mentioned above, function return values are clarified into deterministic values (like numbers, symbols, character strings, etc.) and nondeterministic values (such as functions). Here, we use {identify} to denote a deterministic value set and {unidentify} to denote a nondeterministic value set. Then after refinement, the control-flow graph of source codes is transferred into the state graph of a LTS, whose input label is identify,unidentify∗. A LTS has no initial state and receiving state. It only has starting point and terminal point, and any state can be regarded as its starting state. Hence, let function Gene_Rand be the starting point of a LTS and let Send function be its terminal point. The state graph of the Needham-Schroeder protocol is obtained after refinement, shown in Figure 4.Figure 4
The LTS of part source codes.In Figure4 “S” denotes a state, and its subscript denotes the state of its corresponding function point. For example, SMy denotes the state of memcpy function. If a called function does not call other functions any more, its return value is deterministic, and {identify} is written to denote its input label. If a called function continues to call other functions, then its return value is nondeterministic, and {unidentify} is written to denote its input label. Here, “unidentify=identify|unidentify” can be used to denote the constitution of nondeterministic input labels. Its final return value is deterministic {identify}. For example, the return value of the state SGR is not deterministic at first, for it calls other functions, like BN_new function. Then, the input label of the state SGR is {unidentify}.


### 4.5. The Traces of Protocol Implementations

As is shown in Section4.4, a LTS can be established on the base of the function return values in the program control-flow graph. A LTS is denoted by a 4-tuple S,L,→,S0. We define the LTS of protocol implementations as follows:(1) S denotes a function node state set; S0 denotes the starting point state of the LTS; and Se denotes the terminal point state of the LTS.(2) Si denotes other functions, and there exists Si∈S. Si→αSi+1 denotes the transition relation between any two adjacent states Si, Si+1. α denotes an input label. Let α=identify|undentify∗. If α is unidentify, there exists a substitute function σ, and σ(α)={identify}. Then final function return value is deterministic.According to the LTS of protocol implementations, after protocol implementations there exist the traces of function return values:traces={identify1,identify2,…,identifyn}  n∈N. Then the security of protocol implementations at the source code level can be dynamically analyzed on the base of these traces.


## 4.1. The Protocol Symbolic Description

It is a basic requirement of protocol communications that at least two participants participate in an interactive communication in accordance with certain specifications. Generally, Message Sequence Charts (MSC) of protocol interactive communications are expressed by an ITU-standardized protocol specification language (ITU: International Telecommunication Union) [27] (in this paper, protocol specifications are expressed by the approaches from ITU and literature [28]). The symbolic description of the Needham-Schroeder protocol specifications is shown in Figure 2.Figure 2
The Needham-Schroeder protocol.In Figure2 A and B, respectively, denote two participants of a protocol; pk(A) and pk(B), respectively, denote the public keys of the participants; sk(A) and sk(B), respectively, denote the private keys of the participants; Fresh Na and Fresh Nb, respectively, denote temporary values of A and B; and Na,Apk(B) denotes the encryption of information {|Na,A|} with the public keys of B.


## 4.2. The Refinement of Source Codes

Taking the Needham-Schroeder source codes written in C, for example, we illustrate the refinement of source codes with Algorithm1 and then analyze the security of protocol implementations at the source code level. When writing protocol codes, we exploit the mechanism of RAS public key cryptography for encryption and decryption, and the functions of the OpenSSL crypto library are used while encrypting and decrypting. The protocol runs over OpenSSL. Due to the limited length of this paper, only main source codes are shown in Algorithm 2.Algorithm 2:The part source codes of the Needham-Schroeder protocol.
1int main(int,argc,char argv)
2
3WSADATA wsaData;
4SCOKET client;
5RSA∗R;
6serv.sin_family=AF_INET;
7serv.sin_port=htons(port);
8serv.sin_addr.S_un.S_addr=inet_addr(''127.0.0.1'');
9client=socket(AF_INET,SOCK_STREAM,0);
10connect(client,(structsockaddr∗)&serv,sizeof
(serv));
11Gene_Rand;
12Comp_Str;
13memcpy(plaitxt_A_E,Str_Id,1024);
14public_Encrypt(plaitxt_A_E);
15strcpy(Cipher_buf,(constchar∗)cipher);
16iSend=send(client,Cipher,sizeof(Cipher),0);
17iLen=recv(client,(char∗)cipher,sizeof(cipher),0);
18memcpy(Tcipher_Na_Nb,cipher_Na_Nb,1024);
19Private_Dencrypt_Na_Nb(R,Tciper_Na_Nb);
20memcpy(plaitxt_Nb,StrNb,1024);
21Public_Encrypt_Nb(plaitxt_Nb);
22strcpy(Cipher,(constchar∗)cipher);
23iSend=send(client,Cipher,sizeof(Cipher),0);
24
25int Gene_Rand
26
27BIGNUM∗n;
28int ret,bits=128;
29char∗sn;
30n=BN_new;
31ret=BN_pseudo_rand(n,bits,1,1);
32sn=BN_bn2dec(n);
33strcpy(RandNum,sn);
34return 0;
35
36int Com_Str
37
38strcat(Str_Id,RandNum);
39strcat(Str_Id, ''|A'');
40return 0;
41
42int Public_Encrypt(unsigned char∗s)
43
44RSA∗r;
45int ret,flent,len;
46BIGNUM∗bnn,∗bne;
47bnn=BN_new;
48bne=BN_new;
49ret=BN_dec2bn(&bnn,strn);
50ret=BN_dec2bn(&bnn,stre);
51r=RSA_new;
52r->n=bnn;
53r->e=bne;
54flen=RSA_size(r);
55len=RSA_public_encrypt(flen,s,cipher_A_E,r,3);
56return 0;
57
58int Private_Dencrypt_Na_Nb(RSA∗r,unsigned char∗s)
59
60int len,flen;
61flen=RSA_size(r);
62len=RSA_private_decrypt(flen,s,plaitxt_Na_Nb, r,3);
63return 0;
64
65int StrDivNb(char str)
66
67int k=0,i=0,j=0;
68int strlen=0;
69int Publi_Encrypt_Nb(usigned char∗s)
70
71RSA∗r;
72int ret,flen,len;
73BIGNUM∗bnn,∗bne;
74bnn=BN_new;
75bne=BN_new;
76ret=BN_dec2bn(&bnn,strn);
77ret=BN_dec2bn(&bne,strn);
78r=RSA_new;
79r->n=bnn;
80r->e=bne;
81flen=RSA_size(r);
82len=RSA_public_encrypt(flen,s,cipher_Nb,r,3);
83return 0;
84As is shown in Algorithm2, the source codes of the Needham-Schroeder protocol include many redundant ones. According to Proposition 5 and Algorithm 1, the security analysis of protocol implementations will not be influenced if those redundant codes are deleted. After deletion, the left source codes of the Needham-Schroeder protocol are mainly function codes (shown in Algorithm 3). According to Definition 4, the source codes in Algorithm 3 are the refinement of the source codes in Algorithm 2. In the example of the Needham-Schroeder protocol implementations, the behaviors produced by the source codes in Algorithm 3 are the subset in those produced by the source codes in Algorithm 2. Therefore, we can exploit the traces of function return values produced by the source codes in Algorithm 3 to dynamically analyze the security of the Needham-Schroeder protocol implementations at the source code level.Algorithm 3:The refined part source codes of the Needham-Schroeder protocol.
1int main(int argc,char argc)
2
3connect(client,(struct sockaddr∗)&serv,sizeof(serv));
4Gene_Rand;
5Comp_Str;
6memcpy(plaitxt_A_E,Str_Id,1024);
7Public_Encrypt(plaitxt_A_E);
8strcpy(Cipher_buf,(const char∗)cipher);
9iSend=send(client,Cipher,sizeof(cipher),0);
10iLen=recv(client,(char∗)cipher,sizeof(cipher),0);
11memcpy(Tcipher_Na_Nb,cipher_Na_Nb,1024);
12Private_Dencrypt_Na_Nb(R,Tcipher_Na_Nb);
13memcpy(plaitxt_Nb,StrNb,1024);
14Public_Encrypt_Nb(plaitxt_Nb);
15strcpy(Cipher,(const char∗)cipher);
16iSend=send(client,Cipher,sizeof(Cipher),0);
17
18int Gene_Rand
19
20n=BN_new;
21ret=BN_pseudo_rand(n,bits,1,1);
22sn=BN_bn2dec(n);
23strcpy(RandNum,sn);
24
25int Comp_Str;
26
27strcat(Str_Id,RandNum);
28strcat(Str_Id, ''|A'');
29
30int Public_Encrypt(unsigned char∗s)
31
32bnn=BN_new;
33bne=BN_new;
34ret=BN_dec2bn(&bnn,strn);
35ret=BN_dec2bn(&bne,stre);
36r=RSA_new;
37flen=RSA_size(r);
38len=RSA_public_encrypt(flen,s,cipher_A_E,r,3);
39
40int Private_Dencrypt_Na_Nb(RSA∗r,unsigned char ∗s);
41
42flen=RSA_size(r);
43len=RSA_private_decrypt(flen,s,plaitext_Na_Nb, r,3);
44
45int Public_Encrypt_Nb(unsigned char∗s)
46
47bnn=BN_new;
48bne=BN_new;
49ret=BN_dec2bn(&bnn,strn);
50ret=BN_dec2bn(&bne,stre);
51r=RSA_new;
52flen=RSA_size(r);
53len=RSA_public_encrypt(flen,s,cipher_Nb,r,3);
54According to Definition4 and Proposition 5, the security analysis of protocol implementations after refinement is consistent with that before refinement.


## 4.3. Program Control-Flow Graph

To clearly see the traces of the function return values generated during the protocol implementations, taking the source codes gained after the refinement (in Algorithm3), for example, we draw a program control-flow graph to show the process of calling functions after the refinement, shown in Figure 3.Figure 3
The program control-flow graph.In Figure3, ➜ denotes the control-flow direction of program main functions; “→” denotes the control-flow direction of calling functions; and “⇠” denotes the control-flow direction of function returning.As is shown in the program control-flow graph, there are only two types of function return values: ① deterministic return values (like numerical values, alphabets, symbols, etc.); ② nondeterministic return values (such as calling functions directly or indirectly). When function return values are not deterministic, functions will continue to call other functions until the function return values become deterministic.


## 4.4. From the Control-Flow Graph to the State Graph

From Figure3, we can clearly see the traces of the protocol implementations at the source code level and the state of how functions are called. According to C language grammar and program executive rules, in the normal process of program implementations every called function has a return value (deterministic or nondeterministic) and the implementation of every function is related to its return value. When a function receives its return value, the program will execute next step in order. Every function can be regarded as a state node, and function return values can be regarded as input labels. In this case, the program control-flow graph is just like an automata state graph. As mentioned above, function return values are clarified into deterministic values (like numbers, symbols, character strings, etc.) and nondeterministic values (such as functions). Here, we use {identify} to denote a deterministic value set and {unidentify} to denote a nondeterministic value set. Then after refinement, the control-flow graph of source codes is transferred into the state graph of a LTS, whose input label is identify,unidentify∗. A LTS has no initial state and receiving state. It only has starting point and terminal point, and any state can be regarded as its starting state. Hence, let function Gene_Rand be the starting point of a LTS and let Send function be its terminal point. The state graph of the Needham-Schroeder protocol is obtained after refinement, shown in Figure 4.Figure 4
The LTS of part source codes.In Figure4 “S” denotes a state, and its subscript denotes the state of its corresponding function point. For example, SMy denotes the state of memcpy function. If a called function does not call other functions any more, its return value is deterministic, and {identify} is written to denote its input label. If a called function continues to call other functions, then its return value is nondeterministic, and {unidentify} is written to denote its input label. Here, “unidentify=identify|unidentify” can be used to denote the constitution of nondeterministic input labels. Its final return value is deterministic {identify}. For example, the return value of the state SGR is not deterministic at first, for it calls other functions, like BN_new function. Then, the input label of the state SGR is {unidentify}.


## 4.5. The Traces of Protocol Implementations

As is shown in Section4.4, a LTS can be established on the base of the function return values in the program control-flow graph. A LTS is denoted by a 4-tuple S,L,→,S0. We define the LTS of protocol implementations as follows:(1) S denotes a function node state set; S0 denotes the starting point state of the LTS; and Se denotes the terminal point state of the LTS.(2) Si denotes other functions, and there exists Si∈S. Si→αSi+1 denotes the transition relation between any two adjacent states Si, Si+1. α denotes an input label. Let α=identify|undentify∗. If α is unidentify, there exists a substitute function σ, and σ(α)={identify}. Then final function return value is deterministic.According to the LTS of protocol implementations, after protocol implementations there exist the traces of function return values:traces={identify1,identify2,…,identifyn}  n∈N. Then the security of protocol implementations at the source code level can be dynamically analyzed on the base of these traces.


## 5. The Security Analysis of Protocol Implementations

Functions are an important part of the source codes of a program design language, especially C language. If the behaviors of called program functions are regarded as the events of a protocol implementation, function return values can act as the conditions for running an event during the process of protocol implementations. In this paper, operational semantics are exploited to analyze the behaviors’ security of protocol implementations at the source code level.


### 5.1. The Operational Semantics of Function Return Values

Operational semantics clearly display the traces of function return values of a protocol implementation. That is, they display concrete behaviors of protocol implementations. Therefore, operational semantics have an advantage over other methods and are competent to analyze the security of protocol implementations.(1) The function return values of protocol implementations is as follows.F
=
P
(
R
u
n
F
u
n
c
)
×
P
(
R
u
n
)
×
R
e
t
u
r
n
V
a
l
u
e. Here P(RunFunc) denotes the functions of a protocol, P(Run) denotes running it, and ReturnValue denotes its function return values.(2) The BNF forms of function return values (ReturnValue) during protocol implementations are as follows:ReturnValue⩴ Identity|UnidentifyUnidentify⩴ Function|IdentifyFunction ≔ Self_Func|Libr_FuncSelf_Func ≔ Function|IdentifyLibr_Func ≔ Function|IdentifyIdentify ≔ number|alphabet|stringHere,Self_Func denotes self-defined functions and Libr_Func denotes library functions. Every function has a return value (deterministic or nondeterministic). Every function return value is an element of a trace (ReturnValue∈Traces). After a protocol is implemented, all the function return values constitute its traces. Here is the definition of the BNF form of the traces:Traces⩴ number|alphabet|symbolAccording to the relation between called function events of C language and return values, every called function has a return value, including void values. Then there exists the bijectionM between called function events and return values: CallEvent∣→ReturnValue. According to the traces obtained after the protocol implementations, ∀ReturnValue∈Trace is true. Therefore, there exists the bijection: {e∣→t,∣∀e∈CallEvent,∀t∈Trace}. That is, every event corresponds to an element of the traces of protocol implementations.Definition 6 (event trace).
Let every eventε of protocol implementations correspond to a function return value ν. There exists a set t, which consists of all the function return values. The set t denotes an event trace.Once the bijection between called function events of protocol implementations and function return values is set up, there exists the bijection between the event set and the elements of the traces:Trace={t∣∀e∣→∀ν∈t}. If the event is not secure, its trace is not secure either, which will inevitably lead to the insecurity of the protocol implementations.


### 5.2. Ideal Trace and Nonideal Trace

Generally, it depends on the Dolev-Yao model assumption to decide whether a protocol is secure or not. Equally, the trace of function return values is obtained on the base of the Dolev-Yao model assumption. We are the first to propose “the ideal trace” as the reference of protocol security evaluation for the precise security analysis of protocol implementations at the source code level.In the following definitions, the symbol≺ denotes the ordinal relation of called functions during the protocol implementations. As Definition 6 shows, ≺ denotes the ordinal relation of the events during the protocol implementations. ≺ is a binary relation over e×e. ≺ satisfies partial ordering relation on event sequences {e0,e1,…,en}: ① reflexivity (there exists e≺e for any event e); ② antisymmetry (if there exists e1≺e2ande2≺e1 for any events e1 and e2, then there exists e1=e2); ③ transmissibility (if there exists e1≺e2  and e2≺e3 for e1,e2,e3, then there exists e1≺e3).Definition 7 (nonideal trace).
The protocols are implemented in the following environments:(1)
The environments are based on the Dolev-Yao model (adversaries have the capacity to attack actively or passively).(2)
The environments of implementing protocols are insecure.
①
The environments are insecure due to the flaws of implementing program language structures, such as memory overflow and pointer operation.②
There are malicious code attacks in the environments.The trace obtained in such environments is called a nonideal trace.Definition 8 (ideal trace).
The trace of general protocol implementations satisfies the following conditions.
(1) In an ideal communication environment (there are no adversary attacks in an ideal communication environment, passive attacks, or active attacks; i.e., there is no Dolev-Yao model assumption in the environment), all the participants of a protocol are honest. The information sent or received by these participants is protected and read by encrypting and decrypting techniques.
(2) Partial ordering relation: e0≺e1≺e2,…,ei   0≤i≤n. Here ≺ denotes that the events of protocol implementations satisfy partial order relation.
Generally, if a trace of protocol implementations satisfies both condition (1) and condition (2), it is called the ideal trace.Definition 9 (the similarity between a nonideal trace and the ideal trace).
Letα, β be ordered sequences, respectively, obtained in an ideal environment or a nonideal environment. According to the clustering method, the similarity between the ideal trace and a nonideal trace is defined as follows:(1) Let the Euclidean distance between ordered sequences α and β be dαβ.(2) Let the similarity between ordered sequences α and β be sαβ, and sαβ=δdαβ-1. δ denotes the similarity coefficient.The biggersαβ is, the smaller the degree of deviation between α and β is. This shows that the similarity between the ideal trace and the nonideal trace is bigger, and vice versa.According to Definitions7, 8, and 9, the ideal trace consists of function return values obtained in an ideal environment. In practice, most communications are carried out in nonideal environments. If the trace produced in a nonideal communication environment deviates from the ideal trace, it indicates that the protocol is attacked by a third party. If the attacked protocol is improved, its trace will deviate less from the ideal trace. That is, after its improvement, the similarity between its trace and the ideal trace is bigger. It means that the improved protocol is more secure than the original protocol.


## 5.1. The Operational Semantics of Function Return Values

Operational semantics clearly display the traces of function return values of a protocol implementation. That is, they display concrete behaviors of protocol implementations. Therefore, operational semantics have an advantage over other methods and are competent to analyze the security of protocol implementations.(1) The function return values of protocol implementations is as follows.F
=
P
(
R
u
n
F
u
n
c
)
×
P
(
R
u
n
)
×
R
e
t
u
r
n
V
a
l
u
e. Here P(RunFunc) denotes the functions of a protocol, P(Run) denotes running it, and ReturnValue denotes its function return values.(2) The BNF forms of function return values (ReturnValue) during protocol implementations are as follows:ReturnValue⩴ Identity|UnidentifyUnidentify⩴ Function|IdentifyFunction ≔ Self_Func|Libr_FuncSelf_Func ≔ Function|IdentifyLibr_Func ≔ Function|IdentifyIdentify ≔ number|alphabet|stringHere,Self_Func denotes self-defined functions and Libr_Func denotes library functions. Every function has a return value (deterministic or nondeterministic). Every function return value is an element of a trace (ReturnValue∈Traces). After a protocol is implemented, all the function return values constitute its traces. Here is the definition of the BNF form of the traces:Traces⩴ number|alphabet|symbolAccording to the relation between called function events of C language and return values, every called function has a return value, including void values. Then there exists the bijectionM between called function events and return values: CallEvent∣→ReturnValue. According to the traces obtained after the protocol implementations, ∀ReturnValue∈Trace is true. Therefore, there exists the bijection: {e∣→t,∣∀e∈CallEvent,∀t∈Trace}. That is, every event corresponds to an element of the traces of protocol implementations.Definition 6 (event trace).
Let every eventε of protocol implementations correspond to a function return value ν. There exists a set t, which consists of all the function return values. The set t denotes an event trace.Once the bijection between called function events of protocol implementations and function return values is set up, there exists the bijection between the event set and the elements of the traces:Trace={t∣∀e∣→∀ν∈t}. If the event is not secure, its trace is not secure either, which will inevitably lead to the insecurity of the protocol implementations.


## 5.2. Ideal Trace and Nonideal Trace

Generally, it depends on the Dolev-Yao model assumption to decide whether a protocol is secure or not. Equally, the trace of function return values is obtained on the base of the Dolev-Yao model assumption. We are the first to propose “the ideal trace” as the reference of protocol security evaluation for the precise security analysis of protocol implementations at the source code level.In the following definitions, the symbol≺ denotes the ordinal relation of called functions during the protocol implementations. As Definition 6 shows, ≺ denotes the ordinal relation of the events during the protocol implementations. ≺ is a binary relation over e×e. ≺ satisfies partial ordering relation on event sequences {e0,e1,…,en}: ① reflexivity (there exists e≺e for any event e); ② antisymmetry (if there exists e1≺e2ande2≺e1 for any events e1 and e2, then there exists e1=e2); ③ transmissibility (if there exists e1≺e2  and e2≺e3 for e1,e2,e3, then there exists e1≺e3).Definition 7 (nonideal trace).
The protocols are implemented in the following environments:(1)
The environments are based on the Dolev-Yao model (adversaries have the capacity to attack actively or passively).(2)
The environments of implementing protocols are insecure.
①
The environments are insecure due to the flaws of implementing program language structures, such as memory overflow and pointer operation.②
There are malicious code attacks in the environments.The trace obtained in such environments is called a nonideal trace.Definition 8 (ideal trace).
The trace of general protocol implementations satisfies the following conditions.
(1) In an ideal communication environment (there are no adversary attacks in an ideal communication environment, passive attacks, or active attacks; i.e., there is no Dolev-Yao model assumption in the environment), all the participants of a protocol are honest. The information sent or received by these participants is protected and read by encrypting and decrypting techniques.
(2) Partial ordering relation: e0≺e1≺e2,…,ei   0≤i≤n. Here ≺ denotes that the events of protocol implementations satisfy partial order relation.
Generally, if a trace of protocol implementations satisfies both condition (1) and condition (2), it is called the ideal trace.Definition 9 (the similarity between a nonideal trace and the ideal trace).
Letα, β be ordered sequences, respectively, obtained in an ideal environment or a nonideal environment. According to the clustering method, the similarity between the ideal trace and a nonideal trace is defined as follows:(1) Let the Euclidean distance between ordered sequences α and β be dαβ.(2) Let the similarity between ordered sequences α and β be sαβ, and sαβ=δdαβ-1. δ denotes the similarity coefficient.The biggersαβ is, the smaller the degree of deviation between α and β is. This shows that the similarity between the ideal trace and the nonideal trace is bigger, and vice versa.According to Definitions7, 8, and 9, the ideal trace consists of function return values obtained in an ideal environment. In practice, most communications are carried out in nonideal environments. If the trace produced in a nonideal communication environment deviates from the ideal trace, it indicates that the protocol is attacked by a third party. If the attacked protocol is improved, its trace will deviate less from the ideal trace. That is, after its improvement, the similarity between its trace and the ideal trace is bigger. It means that the improved protocol is more secure than the original protocol.


## 6. The Method and the Experiment

According to Algorithm1, in the process of protocol implementations, source codes are refined. After that, labelled function return values are obtained and constitute the sequences. When analyzing the security of protocol implementations, we exploit the ideal trace as the reference of security evaluation. According to the clustering method, the sequences can be used as samples to analyze the security of protocol implementations at the source code level by means of the deviation of Euclidean distance and the similarity.


### 6.1. The Steps of Our New Method

(1) Supposing that source codes are executed in an ideal communication environment: after an execution, function return values are obtained and form a sequence. It is called the sequence of ideal trace data.(
2) Supposing that source codes are executed in a nonideal communication environment: after an execution, function return values are obtained and form a sequence. It is called the sequence of nonideal trace data.(3) With the clustering method [29], the Euclidean distance [30] dij between the ideal trace and the nonideal trace is calculated. The following is the formula of the Euclidean distance:(1)dxi-xj=∑k=1pxik-xjk21/2.Letdij=d(xi,xj), and let D=(dij)p×p be a distance matrix:(2)0,d12,…,d1n-1,d1nd21,0,…,d2n-1,d2n⋮dn1,dn2,…,dnn-1,0.Heredij=dji. If dij=0, the nonideal trace does not deviate from the ideal trace.(4) Supposing that, after implementing the protocols α and β, their sequences of trace data are obtained: let sαβ be the similarity between the ideal trance and a nonideal trance. The similarity between the sequence of α and the sequence of β is (3)sαβ=11+dαβ.Formula (3) satisfies the following: ① If dαβ→∞, sαβ→0; ② if dij→0, sαβ→1.Therefore, their similarity is inversely proportional to their deviation. That is, the smaller the similarity is, the easier the protocol implementation is attacked.With our new method, when analyzing the security of protocol implementations, there are two cases: ① Ifdik>dij, the nonideal trace {tk} deviates from the ideal trace {ti}  (dik denotes the deviation between the ideal trace {ti} and a nonideal trace {tk}). It means that the protocol is attacked during implementations. ② The bigger sαβ is, the closer the trace of the protocol α gets to the trace of the protocol β. It means that the protocol implementations are more secure.


### 6.2. The Experiments

We carry out experiments with classical protocols and their improvements (written in C). In the experiments, we analyze the cases in which these protocols are attacked by man-in-the-middle attacks during implementations. The running environment is Win7, Visual studio 2010, Intel(R) CPU G3240, memory 4 GB, openssl-1.0.1s. The protocols run by using the functions and the big number in OpenSSL function library. The data of the protocols are encrypted and decrypted with the mechanism of the RSA public key. Participants communicate by linking TCP of Socket API. Simulate experiments are carried out with the pattern of client/server. The function return values are transformed into numerical values and then used as experiment data, which will not influence the result of the security analysis of protocol implementations.(1) We analyze man-in-the-middle attacks of the Needham-Schroeder protocol implementations and the Needham-Schroeder-Lowe protocol implementations.Experiments are carried out in two types of environments: ① the ideal environment and ② nonideal environments. In the ideal environment, the Needham-Schroeder protocol is called INS for short and the Needham-Schroeder-Lowe protocol is called INSL for short. In nonideal environments, the Needham-Schroeder protocol is called MANS for short and the Needham-Schroeder-Lowe protocol is called MANSL for short. NSL is the improvement of the Needham-Schroeder protocol. Theoretically, NSL can resist man-in-the-middle attacks. After running these protocols, their traces are obtained, shown in Table1.Table 1
The trace of function return values of protocol implementations.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
INS (1)
80
1
136
216
144
176
53
5
192
128
128
128
128
208
1
168
216
16
48
53
1
192
MANS (2)
112
1
216
216
176
208
53
5
80
128
128
128
128
240
1
187
216
48
80
53
1
47
INSL (3)
80
1
136
216
144
176
53
5
192
128
128
128
128
208
1
175
216
16
48
53
1
200
MANSL (4)
112
1
240
216
176
208
53
5
80
128
128
128
128
240
1
178
216
48
80
53
1
147
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
INS (1)
128
128
128
128
176
208
53
5
208
128
128
173
241
0
0
128
128
244
191
0
0
1
MANS (2)
128
128
128
208
208
240
53
5
128
128
128
128
128
0
0
0
1
216
0
0
216
0
INSL (3)
128
128
128
128
176
208
53
5
208
128
210
210
244
16
0
128
128
244
149
0
0
1
MANSL (4)
128
128
128
128
208
240
53
5
128
128
128
128
128
0
0
0
1
216
0
0
216
0The illustration of the data in Table1: ① the numbers in the first line are the serial numbers of the functions of the protocol implementations; ② the first row corresponds to the names of the protocols and their serial numbers; ③ the values at the intersections are the function return values of each protocol implementation. For example, INS (1) (5) = 144 means that, during the implementation of INS, the fifth function return value is 144.As is shown in Table1, the traces of the Needham-Schroeder protocol implementations and of the Needham-Schroeder-Lowe protocol implementations deviate from the traces of their implementations in the ideal environments. According to formula (1), we, respectively, calculate each Euclidean distance dij between INS and MANSL, INSL and MANSL, and MANS and MANSL. dij=dji, and i,j∈N,1≤N≤44. The results of calculation are shown in Table 2.Table 2
Euclidean distance between protocols.
INS
MANS
INSL
MANSL
INS
0
439
102
412
MANS
439
0
439
152
INSL
102
439
0
410
MANSL
412
152
410
0According to formula (2), we, respectively, calculate each similarity between INS and MANSL, INSL and MANSL, and MANS and MANSL. The results are shown in Table 3.Table 3
Similarity between protocols.
INS
MANS
INSL
MANSL
INS
1
2.27 × 10−3
9.71 × 10−3
2.41 × 10−3
MANS
2.27 × 10−3
1
2.27 × 10−3
6.54 × 10−3
INSL
9.71 × 10−3
2.27 × 10−3
1
2.43 × 10−3
MANSL
2.41 × 10−3
6.54 × 10−3
2.43 × 10−3
1As is shown in Table2, d12=439 means that the trace of INS deviates from the trace of the MANS protocol implementations; d34=410 means that the trace of INSL deviated from the trace of MANSL. As is shown in Table 3, 2.43 × 10−3 > 2.27 × 10−3 means that the similarity between INSL and MANSL is bigger than the similarity between INS and MANS.(2) We analyze man-in-the-middle attacks of the Diffie-Hellman protocol implementations and the Diffie-Hellman-Signature protocol implementations.The protocols are carried out in two types of environments: ① the ideal environments and ② nonideal environments. In the ideal environment, Diffie-Hellman is called IDH for short and Diffie-Hellman-Signature is called IDHS for short; in nonideal environments, Diffie-Hellman is called MADH for short and Diffie-Hellman-Signature is called MADHS for short. DHS is the improvement of the Diffie-Hellman protocol and, theoretically, it can resist man-in-the-middle attacks. After running these protocols, their traces are obtained, shown in Table4.Table 4
The traces of function return values of protocol implementations.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
IDH (1)
1
1
32
1
1
0
0
77
32
128
136
0
1
1
32
1
1
0
77
32
69
8
MADH (2)
0
1
1
32
1
1
0
77
32
40
8
1
1
32
1
1
0
0
77
32
112
40
IDHS (3)
1
1
32
1
1
0
0
77
32
112
104
0
1
1
32
1
1
0
77
32
112
40
MADHS (4)
0
1
1
32
1
1
0
77
32
114
120
1
1
32
1
1
0
0
77
32
144
142According to formula (1), we, respectively, calculate each Euclidean distance dij between IDH and MADHS, IDHS and MADHS, and MADH and MADHS. dij=dji, and i,j∈N,1≤N≤22. The results of calculation are shown in Table 5.Table 5
Euclidean distance between protocols.
IDH
MADH
IDHS
MADHS
IDH
0
176
64
167
MADH
176
0
135
187
IDHS
64
135
0
129
MADHS
167
187
129
0According to formula (2), we, respectively, calculate the similarity between IDH and MADHS, IDHS and MADHS, and MADH and MADHS. The results are shown in Table 6.Table 6
The similarity between protocols.
IDH
MADH
IDHS
MADHS
IDH
1
5.67 × 10−3
1.529 × 10−2
5.59 × 10−3
MADH
5.67 × 10−3
1
7.40 × 10−3
5.33 × 10−3
IDHS
1.529 × 10−2
7.40 × 10−3
1
7.71 × 10−3
MADHS
5.59 × 10−3
5.33 × 10−3
7.71 × 10−3
1As is shown in Table5, d12=176 means that the trace of IDH deviates from the trace of MADH; d34=129 means that the trace of IDHS deviates from the trace of MADHS. As is shown in Table 6, 7.71×10-3>5.67×10-3 means that the similarity between IDHS and MADHS is bigger than the similarity between IDH and MADH.(3) We analyze the performance of our new method.To illustrate the performance of our new method, we only list the time overhead of each protocol implementation in the ideal environment and nonideal environments (shown in Table7) and discuss the relation between the time overhead and the similarity (shown in Figures 5 and 6). Due to the limited length of this paper, we only list and discuss the time overhead and the similarity of each protocol implementation in the simulated experiments mentioned above.Table 7
The time overhead of implementing protocols.
Name
IDH
IDHS
MADH
MADHS
INS
INSL
MANS
MANSL
Time
0.916
0.789
1.567
0.132
0.037
0.030
0.100
0.096Figure 5
The change of similarity andΔT of the time overhead.Figure 6
The change of similarity andΔT of the time overhead.As is shown in Table7, the time overhead of implementing protocols in the ideal environment is less than the time overhead of implementing protocols in the nonideal environments.We calculate the absolute valuesΔT of the difference of the time between implementing protocols in the ideal environment and implementing protocols in the nonideal environments. We list ΔT of the time overhead and Sαβ of the Needham-Schroeder protocol and its improvement (shown in Table 3), as well as ΔT of the time overhead and Sαβ of Diffie-Hellman protocol and its improvement (shown in Table 6). By comparing their changes, we can see their relation clearly, shown in Figures 5 and 6.This shows that the relation betweenSαβ and ΔT tends to be in inverse proportion. It means that Sαβ is related to the performance of protocol implementations in different environments.As is shown in experiments (1), (2), and (3), the security of protocol implementations can be analyzed through the traces of function return values obtained when implementing the protocols in the ideal environment and in the nonideal environments. From the experiments, we can conclude the following:① Third-party attacks can be found.② The deviation of the improved protocols is smaller than the deviation of the original ones. This means that the improved protocols are more secure than the original ones in the process of implementations at the source code level.③ The protocols are insecure during implementations at the source code level, even though they are proved to be secure on theory level.④ In the ideal environment and nonideal environments, the performance of protocol implementations is related to the similarity. It is in accordance with the security thought defined by software.This paper aims to analyze the security of protocol implementations at the source code level. With our method, attacks can be discovered by analyzing whether there are abnormal behavior characteristics when implementing protocols, such as memory overflow and malicious code (shellcode) attacks. This paper mainly analyzes man-in-the-middle attacks.Man-in-the-middle attacks are a common type of attacks which protocols widely suffer from [31]. It is typical to analyze the security of protocol implementations which are attacked by man-in-the-middle attacks. The thought of our new method comes from life phenomena and the theory is on the base of LTS, program operational semantics, and program refinement. And we propose Algorithm 1. The purpose of analysis is to discover whether a protocol is attacked by third-party attacks, impersonation attacks, or other attacks during the implementation at the source code level. We discover that the similarity of the improved protocols, which can resist man-in-the-middle attacks, is bigger than that of the original ones. Hence, our method is competent to analyze the protocols attacked by man-in-the-middle attacks during the implementations at the source code level.


## 6.1. The Steps of Our New Method

(1) Supposing that source codes are executed in an ideal communication environment: after an execution, function return values are obtained and form a sequence. It is called the sequence of ideal trace data.(
2) Supposing that source codes are executed in a nonideal communication environment: after an execution, function return values are obtained and form a sequence. It is called the sequence of nonideal trace data.(3) With the clustering method [29], the Euclidean distance [30] dij between the ideal trace and the nonideal trace is calculated. The following is the formula of the Euclidean distance:(1)dxi-xj=∑k=1pxik-xjk21/2.Letdij=d(xi,xj), and let D=(dij)p×p be a distance matrix:(2)0,d12,…,d1n-1,d1nd21,0,…,d2n-1,d2n⋮dn1,dn2,…,dnn-1,0.Heredij=dji. If dij=0, the nonideal trace does not deviate from the ideal trace.(4) Supposing that, after implementing the protocols α and β, their sequences of trace data are obtained: let sαβ be the similarity between the ideal trance and a nonideal trance. The similarity between the sequence of α and the sequence of β is (3)sαβ=11+dαβ.Formula (3) satisfies the following: ① If dαβ→∞, sαβ→0; ② if dij→0, sαβ→1.Therefore, their similarity is inversely proportional to their deviation. That is, the smaller the similarity is, the easier the protocol implementation is attacked.With our new method, when analyzing the security of protocol implementations, there are two cases: ① Ifdik>dij, the nonideal trace {tk} deviates from the ideal trace {ti}  (dik denotes the deviation between the ideal trace {ti} and a nonideal trace {tk}). It means that the protocol is attacked during implementations. ② The bigger sαβ is, the closer the trace of the protocol α gets to the trace of the protocol β. It means that the protocol implementations are more secure.


## 6.2. The Experiments

We carry out experiments with classical protocols and their improvements (written in C). In the experiments, we analyze the cases in which these protocols are attacked by man-in-the-middle attacks during implementations. The running environment is Win7, Visual studio 2010, Intel(R) CPU G3240, memory 4 GB, openssl-1.0.1s. The protocols run by using the functions and the big number in OpenSSL function library. The data of the protocols are encrypted and decrypted with the mechanism of the RSA public key. Participants communicate by linking TCP of Socket API. Simulate experiments are carried out with the pattern of client/server. The function return values are transformed into numerical values and then used as experiment data, which will not influence the result of the security analysis of protocol implementations.(1) We analyze man-in-the-middle attacks of the Needham-Schroeder protocol implementations and the Needham-Schroeder-Lowe protocol implementations.Experiments are carried out in two types of environments: ① the ideal environment and ② nonideal environments. In the ideal environment, the Needham-Schroeder protocol is called INS for short and the Needham-Schroeder-Lowe protocol is called INSL for short. In nonideal environments, the Needham-Schroeder protocol is called MANS for short and the Needham-Schroeder-Lowe protocol is called MANSL for short. NSL is the improvement of the Needham-Schroeder protocol. Theoretically, NSL can resist man-in-the-middle attacks. After running these protocols, their traces are obtained, shown in Table1.Table 1
The trace of function return values of protocol implementations.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
INS (1)
80
1
136
216
144
176
53
5
192
128
128
128
128
208
1
168
216
16
48
53
1
192
MANS (2)
112
1
216
216
176
208
53
5
80
128
128
128
128
240
1
187
216
48
80
53
1
47
INSL (3)
80
1
136
216
144
176
53
5
192
128
128
128
128
208
1
175
216
16
48
53
1
200
MANSL (4)
112
1
240
216
176
208
53
5
80
128
128
128
128
240
1
178
216
48
80
53
1
147
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
INS (1)
128
128
128
128
176
208
53
5
208
128
128
173
241
0
0
128
128
244
191
0
0
1
MANS (2)
128
128
128
208
208
240
53
5
128
128
128
128
128
0
0
0
1
216
0
0
216
0
INSL (3)
128
128
128
128
176
208
53
5
208
128
210
210
244
16
0
128
128
244
149
0
0
1
MANSL (4)
128
128
128
128
208
240
53
5
128
128
128
128
128
0
0
0
1
216
0
0
216
0The illustration of the data in Table1: ① the numbers in the first line are the serial numbers of the functions of the protocol implementations; ② the first row corresponds to the names of the protocols and their serial numbers; ③ the values at the intersections are the function return values of each protocol implementation. For example, INS (1) (5) = 144 means that, during the implementation of INS, the fifth function return value is 144.As is shown in Table1, the traces of the Needham-Schroeder protocol implementations and of the Needham-Schroeder-Lowe protocol implementations deviate from the traces of their implementations in the ideal environments. According to formula (1), we, respectively, calculate each Euclidean distance dij between INS and MANSL, INSL and MANSL, and MANS and MANSL. dij=dji, and i,j∈N,1≤N≤44. The results of calculation are shown in Table 2.Table 2
Euclidean distance between protocols.
INS
MANS
INSL
MANSL
INS
0
439
102
412
MANS
439
0
439
152
INSL
102
439
0
410
MANSL
412
152
410
0According to formula (2), we, respectively, calculate each similarity between INS and MANSL, INSL and MANSL, and MANS and MANSL. The results are shown in Table 3.Table 3
Similarity between protocols.
INS
MANS
INSL
MANSL
INS
1
2.27 × 10−3
9.71 × 10−3
2.41 × 10−3
MANS
2.27 × 10−3
1
2.27 × 10−3
6.54 × 10−3
INSL
9.71 × 10−3
2.27 × 10−3
1
2.43 × 10−3
MANSL
2.41 × 10−3
6.54 × 10−3
2.43 × 10−3
1As is shown in Table2, d12=439 means that the trace of INS deviates from the trace of the MANS protocol implementations; d34=410 means that the trace of INSL deviated from the trace of MANSL. As is shown in Table 3, 2.43 × 10−3 > 2.27 × 10−3 means that the similarity between INSL and MANSL is bigger than the similarity between INS and MANS.(2) We analyze man-in-the-middle attacks of the Diffie-Hellman protocol implementations and the Diffie-Hellman-Signature protocol implementations.The protocols are carried out in two types of environments: ① the ideal environments and ② nonideal environments. In the ideal environment, Diffie-Hellman is called IDH for short and Diffie-Hellman-Signature is called IDHS for short; in nonideal environments, Diffie-Hellman is called MADH for short and Diffie-Hellman-Signature is called MADHS for short. DHS is the improvement of the Diffie-Hellman protocol and, theoretically, it can resist man-in-the-middle attacks. After running these protocols, their traces are obtained, shown in Table4.Table 4
The traces of function return values of protocol implementations.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
IDH (1)
1
1
32
1
1
0
0
77
32
128
136
0
1
1
32
1
1
0
77
32
69
8
MADH (2)
0
1
1
32
1
1
0
77
32
40
8
1
1
32
1
1
0
0
77
32
112
40
IDHS (3)
1
1
32
1
1
0
0
77
32
112
104
0
1
1
32
1
1
0
77
32
112
40
MADHS (4)
0
1
1
32
1
1
0
77
32
114
120
1
1
32
1
1
0
0
77
32
144
142According to formula (1), we, respectively, calculate each Euclidean distance dij between IDH and MADHS, IDHS and MADHS, and MADH and MADHS. dij=dji, and i,j∈N,1≤N≤22. The results of calculation are shown in Table 5.Table 5
Euclidean distance between protocols.
IDH
MADH
IDHS
MADHS
IDH
0
176
64
167
MADH
176
0
135
187
IDHS
64
135
0
129
MADHS
167
187
129
0According to formula (2), we, respectively, calculate the similarity between IDH and MADHS, IDHS and MADHS, and MADH and MADHS. The results are shown in Table 6.Table 6
The similarity between protocols.
IDH
MADH
IDHS
MADHS
IDH
1
5.67 × 10−3
1.529 × 10−2
5.59 × 10−3
MADH
5.67 × 10−3
1
7.40 × 10−3
5.33 × 10−3
IDHS
1.529 × 10−2
7.40 × 10−3
1
7.71 × 10−3
MADHS
5.59 × 10−3
5.33 × 10−3
7.71 × 10−3
1As is shown in Table5, d12=176 means that the trace of IDH deviates from the trace of MADH; d34=129 means that the trace of IDHS deviates from the trace of MADHS. As is shown in Table 6, 7.71×10-3>5.67×10-3 means that the similarity between IDHS and MADHS is bigger than the similarity between IDH and MADH.(3) We analyze the performance of our new method.To illustrate the performance of our new method, we only list the time overhead of each protocol implementation in the ideal environment and nonideal environments (shown in Table7) and discuss the relation between the time overhead and the similarity (shown in Figures 5 and 6). Due to the limited length of this paper, we only list and discuss the time overhead and the similarity of each protocol implementation in the simulated experiments mentioned above.Table 7
The time overhead of implementing protocols.
Name
IDH
IDHS
MADH
MADHS
INS
INSL
MANS
MANSL
Time
0.916
0.789
1.567
0.132
0.037
0.030
0.100
0.096Figure 5
The change of similarity andΔT of the time overhead.Figure 6
The change of similarity andΔT of the time overhead.As is shown in Table7, the time overhead of implementing protocols in the ideal environment is less than the time overhead of implementing protocols in the nonideal environments.We calculate the absolute valuesΔT of the difference of the time between implementing protocols in the ideal environment and implementing protocols in the nonideal environments. We list ΔT of the time overhead and Sαβ of the Needham-Schroeder protocol and its improvement (shown in Table 3), as well as ΔT of the time overhead and Sαβ of Diffie-Hellman protocol and its improvement (shown in Table 6). By comparing their changes, we can see their relation clearly, shown in Figures 5 and 6.This shows that the relation betweenSαβ and ΔT tends to be in inverse proportion. It means that Sαβ is related to the performance of protocol implementations in different environments.As is shown in experiments (1), (2), and (3), the security of protocol implementations can be analyzed through the traces of function return values obtained when implementing the protocols in the ideal environment and in the nonideal environments. From the experiments, we can conclude the following:① Third-party attacks can be found.② The deviation of the improved protocols is smaller than the deviation of the original ones. This means that the improved protocols are more secure than the original ones in the process of implementations at the source code level.③ The protocols are insecure during implementations at the source code level, even though they are proved to be secure on theory level.④ In the ideal environment and nonideal environments, the performance of protocol implementations is related to the similarity. It is in accordance with the security thought defined by software.This paper aims to analyze the security of protocol implementations at the source code level. With our method, attacks can be discovered by analyzing whether there are abnormal behavior characteristics when implementing protocols, such as memory overflow and malicious code (shellcode) attacks. This paper mainly analyzes man-in-the-middle attacks.Man-in-the-middle attacks are a common type of attacks which protocols widely suffer from [31]. It is typical to analyze the security of protocol implementations which are attacked by man-in-the-middle attacks. The thought of our new method comes from life phenomena and the theory is on the base of LTS, program operational semantics, and program refinement. And we propose Algorithm 1. The purpose of analysis is to discover whether a protocol is attacked by third-party attacks, impersonation attacks, or other attacks during the implementation at the source code level. We discover that the similarity of the improved protocols, which can resist man-in-the-middle attacks, is bigger than that of the original ones. Hence, our method is competent to analyze the protocols attacked by man-in-the-middle attacks during the implementations at the source code level.


## 7. Conclusion and Future Work

In the paper, we have proposed a new method to dynamically analyze the security of protocol implementations at the source code level. First, we have refined protocol source codes through strong simulation relation and have established a model for the security analysis of protocol implementations. Second, when implementing protocols, we have obtained the function return values, which constitute the sequences of trace data. We propose the ideal trace as the evaluating reference for protocol security analysis. The clustering method is exploited to analyze the sequences of trace data. We propose to exploit the deviation of the Euclidean distance between the ideal trace and nonideal traces and the similarity between the ideal trace and nonideal traces to analyze the security of protocol implementations. Last, taking some classical protocols, for example, we have carried out experiments. Our experiments show that third-party attacks can be found by analyzing the deviation and similarity of the traces of the function return values obtained when implementing protocols. It is also shown through our experiments that the improved protocols are more secure than the original ones. Our method exploits the traces of protocol implementations to analyze its security and differs from other methods mentioned in the literature. It will be helpful and valuable for protocol design, security verification, and security evaluation.The future study in this field lies in the automatic security analysis of protocol implementations [32] and the security analysis of parallel protocol implementations [33]. It requires improving existing protocol automatic analysis tools or developing new automatic tools for the security analysis of protocol implementations. On the other hand, since the flaws of language structures will make the security analysis of protocol implementations more complex, more studies should be carried out to solve these complex problems, such as C language memory access and pointer analysis. This field should be focused on.



---

*Source: 7042835-2017-10-18.xml*