A Security Authentication Protocol for Trusted Domains in an Autonomous Decentralized System

Abstract

Software Defined Network (SDN) architecture has been widely used in various application domains. Aiming at the authentication and security issues of SDN architecture in autonomous decentralized system (ADS) applications, securing the mutual trust among the autonomous controllers, we combine trusted technology and SDN architecture, and we introduce an authentication protocol based on SDN architecture without any trusted third party between trusted domains in autonomous systems. By applying BAN predicate logic and AVISPA security analysis tool of network interaction protocol, we can guarantee protocol security and provide complete safety tests. Our work fills the gap of mutual trust between different trusted domains and provides security foundation for interaction between different trusted domains.

1. Introduction

Autonomous decentralized systems (ADS) have been extended and applied to a variety of domains [1–6]. The main extension in ADS is to implement the dynamic management and to optimize the allocation of virtualized computing, storage, device controllers, and cyber resources. The current major platforms are mature in management and optimization of traditional computing and storage resources. However, the dynamic management and the allocation of ADS devices as cyber resources are a new problem which has not been studied thoroughly. The problem is mainly from network architecture design. The traditional TCP/IP architecture cannot meet the increasing demands, especially the virtualized network and ADS services. Thus, ADS needs new network architecture and techniques with flexibility, robustness, security, and credibility to solve the problem.

In the next generation network architecture design, many experts and scholars have completed a series of remarkable research work. Specifically, OpenFlow [7], introduced by Nick McKeown, gave researchers a way to run experimental protocols in the networks. Based on Software Defined Network (SDN) and OpenFlow protocol, researchers implemented network management and security functions mainly in the aspects of control, traffic forwarding, and load balancing. But the security issue in OpenFlow design should be thoroughly concerned, especially the security interaction function between different controllers' nodes. The problem of security certification issues between the different single controllers limits the interaction range of a SDN architecture, which is only used in a single domain with a single controller, such as the Data Center.

In order to solve secure interaction issues, experts and scholars have completed a series of research work. Reference [7] proposed the SANE network architecture in which logic controllers could provide secure authentication for device access and loading strategy. Moreover, [8] further extended SANE network architecture with data forwarding strategy by using core controller method. The improved architecture implemented with data forwarding function, in a certain extent, could solve the security threats between controller layer and data forwarding layer.

Reference [9] implemented a new network architecture GENI and recognized that a large number of malicious attacks and flood attacks can be easily spread through logic control layers and data forwarding layers and lead to corresponding secure issues, for instance, DDoS attack.

Reference [10] evaluated the weakness of OpenFlow protocol. The author thought OpenFlow had an accurate secure certification method between controllers and switches, but this method did not provide security mechanisms under transport layer.

Based on SDN architecture, [11] did a comprehensive analysis for evaluating NOX, POX, Ryu, and Beacon [12–15] controllers in compatibility, reliability, security, and processing capacity. Focusing on the aspect of security, the authors pointed out that the reason to most controllers' security problems was forged stream message length, protocol version, or wrong type of message flow.

Besides, in [16], the authors analyzed the entire SDN security issues and pointed out that the new network architecture with a rapid response and antithreatening security mechanism was needed to be reestablished, especially in the differences of security threats between controllers and traditional network.

Based on the above issues, one of the key features of ADS is to allow content-based message broadcasting. In order to ensure the real-time system, message package could not be encrypted. The receiver node does not check whether the source address is valid or not, and whether the message package has been tampered or not. It means that an attacker can set up the entire attack in essentially one operation. While the security for ADS is drawing attention, it is an indisputable fact that there is a lack of effective methods to support those frameworks. The contributions of our paper are as follows:

• (1)

Our paper introduces a new architecture to increase the probability of guaranteeing the credibility for future network architecture by applying the ideas of trusted network to ADS. The new architecture with trusted function modules can measure sensitive information and provide a security interaction function between different SDN domains.

(2)

Based on the new architecture with trusted function modules, we propose a trusted domain authentication protocol that protects controllers' credibility among entire network architecture when communicating with a nontrusted third party. Trusted function modules, such as Trusted Measurement Module (TMM) and TCG Software Stack (TSS), could provide a set of services to ensure authentication protocol's security, for example, encryption, decryption, digital sign, or key management. The protocol gets trust certifications among different trusted domains and provides secure base in domain session.

(3)

We demonstrate security of our trusted domain authentication protocol by BAN logic and AVISPA security analysis system and perform a comparative analysis of our trusted domain authentication protocol against some prevalent protocols, namely, IKEv2 [17], IDAKE-MA, and SKAP [18], in performance analysis. We believe that the protocol performance, including calculating consumption and storage consumption, is an index which can give us obviously evidence to prove advantage of our protocol.

This paper is organized as follows. Section 2 introduces a SDN trusted domain network architecture and describes our trusted domain authentication protocol. In Section 3, we demonstrate security of our protocol by the BAN logic [19]. In Section 4, we analyze security of our protocol with different malicious test scenarios by AVISPA security analysis system [20]. Section 5 performs an analysis between our protocol and some authentication protocols.

2. Security Authentication Protocol for ADS Applications

As shown in Figure 1, we propose a SDN trusted domain network architecture which combines SDN and trusted computing. This architecture contains a single controller and a number of network devices. For solving the trust certification problem among trusted domains, we design some modules in SDN controller. TMM, based on TSS [21], is used to measure the sensitive information of SDN controller and connect network devices. Sensitive information includes controller platform hardware information, controller platform OS information, controller software information, and trusted function modules information. Controller Flow Rule (CFR) is trusted policy, including SDN data forwarding strategy and trusted measurement strategy, which was measured by TMM. Controller Communication Module (CCM) ensures controller authentication process between individual trusted domains.

Figure 1

SDN trusted domain network architecture.

In SDN trusted domain network architecture, we propose a domain secure certificated protocol between SDN trusted domains, and, in particular, our protocol can be utilized on nontrusted third party circumstance. From the viewpoint of the trusted chain [22], we can implement a consistency test of measuring information integrity about controller hardware, operating system, controller software, and CCM for trusted negotiation. After finishing trusted negotiation, we can adopt the method of multilevel authentication to guarantee security. More specific, controller authentication can be divided into two parts, controller platform authentication and controller software authentication, which protects the release of sensitive information and prevents unauthorized users from capturing sensitive information. The combination of sensitive information and random numbers, based on the strong protection of sensitive information, ensures that sensitive information is not being hijacked and not subject to replay attacks by unauthorized users, thereby avoiding the security of sensitive information by refusing the connection of those illegal or security risks.

2.1. Protocol Certification Process Overview

Before we design our security certification protocol, we present the three major aspects of our protocol certification process.

First, in accordance with the trust chain transfer rules in trusted computing, the TMM is based on TSS and will follow the orders by measuring sensitive information of SDN controller hardware, operating system, CCM, and storing measurement results into RTS (Root Trusted Storage) of the PCR register.

Second, the controller platform certification: when implementing different trusted domain controller authentication, authentication requester sends the HMAC calculation results of hardware information, operating system, and random numbers to the receiver, respectively, and expects the identical HMAC result with the receivers. If the controller platform's HMAC result of the receiver is consistent with that of the requester, then we complete the certification process of controller platform.

Finally, the controller software certification: in terms of implementing the trusted authentication of sensitive information in controller software, the requester sends HMAC calculation results, including controller software metrics, core controller module metrics, and random numbers, to the receiver. As shown in the controller platform certification in Figure 1, the receiver will compare the controller software HMAC results with that of the requester. If their results are consistent, we complete the certification of the controller software.

2.2. Specific Certification Process

First, we define the related symbols used in the certification process:

• (1)

R: authentication requester,

(2)

N: authentication receiver,

(3)

$N_{\mathrm{P}\mathrm{U}\mathrm{B}}$ : authentication requester public key,

(4)

$R_{\mathrm{P}\mathrm{U}\mathrm{B}}$ : authentication receiver public key,

(5)

$N^{-1}$ : authentication requester private key,

(6)

$R^{-1}$ : authentication receiver private key,

(7)

${\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_\mathrm{I}\mathrm{D}}_R$ : authentication requester platform ID,

(8)

${\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_\mathrm{I}\mathrm{D}}_N$ : authentication receiver platform ID,

(9)

${\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R$ : random number of authentication requester, used to measure HMAC and prevent replay attack,

(10)

${\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N$ : random number of authentication receiver, used to measure HMAC and prevent replay attack,

(11)

${\mathrm{A}\mathrm{K}}_R$ : random number of authentication requester, used to make a session key by authentication receiver,

(12)

AK: session key,

(13)

ACK: authentication successful symbol,

(14)

${\mathrm{C}\mathrm{S}\_\mathrm{I}\mathrm{D}}_R$ : controller software ID of authentication requester,

(15)

${\mathrm{C}\mathrm{S}\_\mathrm{I}\mathrm{D}}_N$ : controller software ID of authentication receiver,

(16)

$R\_\mathrm{P}\mathrm{C}\mathrm{R}$ : controller platform hardware/controller platform OS/controller software/controller application module measurement of authentication requester,

(17)

$N\_\mathrm{P}\mathrm{C}\mathrm{R}$ : controller platform hardware/controller platform OS/controller software/controller application module measurement of authentication receiver,

(18)

$\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}()$ : hash function based on HMAC_SHA-1 of TPM.

Figure 2 shows the specific certification process. More details will be introduced in following two subsections.

Figure 2

Trusted domain authentication process.

2.2.1. Controller Platform Certification Process

Controller platform certification process consists of the following steps.

Step 1 (R (the requesting controller) sends an authentication request to N (the receiving controller)).

First, R creates a digital signature for its own controller platform identity information ${\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_\mathrm{I}\mathrm{D}}_R$ , random numbers ${\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R$ , and hardware sensitive information $R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_1$ by its own private key. Then, the public key of N is expected to encrypt the HMAC value, and finally R sends the encrypted message to N:

$$\begin{array}{cc}& \begin{array}{c}R⟶N:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{1}},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\parallel {\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\parallel {\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_\mathrm{I}\mathrm{D}}_R\right\}{R}^{-\mathrm{1}}\right\}{N}_{\mathrm{P}\mathrm{U}\mathrm{B}}.\end{array}\end{array}$$

(1)

Step 2 (N receives the authorized information from R).

First, N receives the encrypted message including R's ID and $N_{\mathrm{P}\mathrm{U}\mathrm{B}}$ from Step 1. Then, N will implement a negotiated registration by using R's platform identity information. And then, aiming at the hardware sensitive information in the R's platform, N implements a credible verification which uses PCR values of N's hardware sensitive information to make HMAC with ${\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R$ . If the HMAC result is consistent with N received information in Step 1, R's hardware is trusted. Finally, if the verification is completed, N will create a digital signature for signing controller platform identity information ${\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_\mathrm{I}\mathrm{D}}_N$ , random numbers ${\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N$ , and hardware sensitive information $N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{1}}$ and correspondingly use the public key of R to encrypt them and send the result to R. On the contrary, the negotiation fails:

$$\begin{array}{cc}& \begin{array}{c}N⟶R:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{1}},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\right)\parallel {\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\parallel {\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_\mathrm{I}\mathrm{D}}_N\right\}{N}^{-\mathrm{1}}\right\}{R}_{\mathrm{P}\mathrm{U}\mathrm{B}}.\end{array}\end{array}$$

(2)

Step 3 (R receives the authorized information from N).

First, R receives the verification feedback from N, which is encrypted by the public key of R, indicating that there is a trusted negotiation between R and N. Second, ${\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_\mathrm{I}\mathrm{D}}_N$ could similarly implement its negotiated registration. Third, as shown in Step 2, R begins the credible verification with the hardware sensitive information of N; if the results are consistent, N can be trusted in hardware. Finally, if the verification passes, R will generate trust negotiation session random numbers; meanwhile N creates the negotiated private key and implements the next round trust negotiation. R will sign sensitive information of controller platform operating system HMAC value and encrypt the sensitive information by session key. The negotiation fails when the verification is not successfully passed:

$$\begin{array}{cc}& \begin{array}{c}R⟶N:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{2}},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\parallel {\mathrm{A}\mathrm{K}}_R\right\}{R}^{-\mathrm{1}}\right\}{N}_{\mathrm{P}\mathrm{U}\mathrm{B}}.\end{array}\end{array}$$

(3)

Step 4 (N receives the HMAC sensitive information of the controller platform operating system $R\_$ PCR₂ and key random numbers of R, AK_R).

First, N receives $R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{2}}$ and implements a credible verification, as shown in Step 2, with the operating system measurement result $N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{2}}$ of its own controller. Second, if the verification passes, N will produce a negotiated private key random number ${\mathrm{A}\mathrm{K}}_N$ . Then, using ${\mathrm{A}\mathrm{K}}_R$ , ${\mathrm{A}\mathrm{K}}_N$ , the pseudo random numbers, and function PRGF, N will create a controller software verification session private key AK, which is bound with the platform information of R. Finally, N's platform sends the sensitive information HMAC value of N to R. The negotiation fails if the credible verification is not successfully passed:

$$\begin{array}{cc}& \begin{array}{c}N⟶R:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{2}},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\right)\parallel \mathrm{A}\mathrm{C}\mathrm{K}\parallel \mathrm{A}\mathrm{K}\right\}{N}^{-\mathrm{1}}\right\}{R}_{\mathrm{P}\mathrm{U}\mathrm{B}}.\end{array}\end{array}$$

(4)

2.2.2. Controller Software Certification Process

In this subsection, we continue to explain the steps in certification process. These steps are related to the controller software certification process.

Step 5 (R receives the sensitive information HMAC value from the receiving controller platform operating system).

First, R receives the operating system sensitive information from the receiving controller platform and implements a credible verification, as shown in Step 2, with the operating system measurement result $R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{2}}$ of its own controller platform. Then, if the credible verification passes, the trust negotiation will enter into the controller software verification process, and, therefore, session private key AK will bind the information of N and also sign the encrypted information through R's private key. Finally, R returns the signed information to N. The negotiation fails if the credible verification fails:

$$\begin{array}{cc}& \begin{array}{c}R⟶N:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{3}},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\parallel {\mathrm{C}\mathrm{S}\_\mathrm{I}\mathrm{D}}_R\right\}\mathrm{A}\mathrm{K}\right\}{R}^{-\mathrm{1}}.\end{array}\end{array}$$

(5)

Step 6 (N receives the controller software verification request from R).

First, N decrypts the information by R's public key, proving the existing base of the trust negotiation between R and N. Then, using the decryption of the sensitive information HMAC value of the controller software, N implements a credible verification as shown in Step 2. If the credible verification passes, N will proceed a negotiated registration using the controller software information ${\mathrm{C}\mathrm{S}\_\mathrm{I}\mathrm{D}}_R$ of R, encrypt the sensitive information HMAC value of controller software and the controller software ID through session private key AK, and sign the encrypted information through R's private key. Finally, N returns the signed information to R. The negotiation fails if the credible verification is not successfully passed:

$$\begin{array}{cc}& \begin{array}{c}N⟶R:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{3}},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\right)\parallel {\mathrm{C}\mathrm{S}\_\mathrm{I}\mathrm{D}}_N\right\}\mathrm{A}\mathrm{K}\right\}{N}^{-\mathrm{1}}.\end{array}\end{array}$$

(6)

Step 7 (R receives the verification information from N).

First, as shown in Step 6, using the sensitive information HMAC value of the controller software, the receiving controller implements a credible verification as shown in Step 2. Then, if the credible verification passes, R will implement a negotiated registration using the controller software information of N. R encrypts the sensitive information HMAC value of $R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{4}}$ and ${\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R$ through session private key AK and signs the encrypted information by R's private key. Finally, N returns the signed information to R. The negotiation fails if the credible verification is not successfully passed:

$$\begin{array}{cc}& R⟶N:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{4}},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\right\}\mathrm{A}\mathrm{K}\right\}{R}^{-\mathrm{1}}.\end{array}$$

(7)

Step 8.

First, receiving controller software application modules HMAC value of R, N implements a credible verification as shown in Step 2. Then, if the credible verification passes, N will encrypt the sensitive information HMAC value of $N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{4}}$ and ${\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N$ by session private key AK and sign the encrypted information by R's private key. Finally, R implements a credible verification on application module sensitive information of N, shown in Step 2. If the verification passes, the verification of the controller software will be completed and the controller verification will pass. Otherwise, the negotiation fails:

$$\begin{array}{cc}& \begin{array}{c}N⟶R:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{4}},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\right)\parallel \mathrm{A}\mathrm{C}\mathrm{K}\right\}\mathrm{A}\mathrm{K}\right\}{N}^{-\mathrm{1}}.\end{array}\end{array}$$

(8)

3. BAN Logic Security Analysis

According to the BAN logic security analysis, this section analyzes whether our authentication protocol is secure or not.

3.1. BAN Logic Security Analysis

BAN predicate logic is composed of 10 basic syntax and semantic clauses:

• (1)

$Q\mid \equiv A\hspace{0.17em}\hspace{0.17em}Q$ believes that A is credible.

(2)

$Q⊲A\hspace{0.17em}\hspace{0.17em}Q$ receives message A.

(3)

$Q\mid ~A\hspace{0.17em}\hspace{0.17em}Q$ has sent message A.

(4)

$Q\mid \Rightarrow A\hspace{0.17em}\hspace{0.17em}Q$ has jurisdiction for message A.

(5)

$\#(A)$ : message A is fresh, which means that A is temporary value and not the first to be sent as the information.

(6)

$P\stackrel{\mathrm{K}\mathrm{e}\mathrm{y}}{\leftrightarrow }Q$ : the key is shared key between P and Q.

(7)

$\stackrel{\mathrm{K}\mathrm{e}\mathrm{y}}{\to }Q$ or $\mid \stackrel{\mathrm{K}\mathrm{e}\mathrm{y}}{\to }Q$ : key is Q's public key.

(8)

$P\stackrel{X}{\rightleftarrows }Q\hspace{0.17em}\hspace{0.17em}X$ events are shared secrets between P and Q.

(9)

${\left\{X\right\}}_{\mathrm{K}\mathrm{e}\mathrm{y}}$ : message X is encrypted by key.

(10)

${〈X〉}_Y$ is the cascade of information of X and Y.

3.2. BAN Logic Inference Rules

This section describes the four main specific rules of BAN logic to provide a theoretical basis for SDN trusted domains security authentication protocol. ⊢ is primitive symbol, such as $P⊢Q$ representing that P derives conclusions Q.

(1) Message Meaning Rule

Theorem 1.

Consider

$$\begin{array}{cc}& \begin{array}{c}P\left|\equiv \right.\stackrel{K}{\to }Q,\end{array}\\ \begin{array}{c}P\left.<\right|{\left\{X\right\}}_{K^{-\mathrm{1}}}⊢P\left|\equiv \right.Q\left|~\right.X.\end{array}\end{array}$$

(9)

Explanation. If P believes that Q's public key is K, and P has received the message ${\left\{X\right\}}_{K^{-\mathrm{1}}}$ which is encrypted by $K^{-1}$ , we can infer that P believes message X which was sent by Q.

(2) Temporary Value Validation Rules

Theorem 2.

Consider

$$\begin{array}{cc}& \begin{array}{c}P\left|\equiv \#\right.\left(X\right),\end{array}\\ P\left|\equiv \right.Q\left|~\right.X⊢P\left|\equiv \right.Q\left|\equiv \right.X.\begin{array}{c}\end{array}\end{array}$$

(10)

Explanation. If P believes that message X is fresh, and P believes that Q has sent message X, we can infer that P believes that Q believes the message X.

(3) Jurisdiction Rules

Theorem 3.

Consider

$$\begin{array}{cc}& \begin{array}{c}P\left|\equiv \right.Q\left|\Rightarrow \right.X,\end{array}\\ \begin{array}{c}P\left|\equiv \right.Q\left|\equiv \right.X⊢P\left|\equiv \right.X.\end{array}\end{array}$$

(11)

Explanation. If P believes that Q has jurisdiction for message X, and P believes that Q believes message X, we can infer that P believes the message X.

(4) Receive Messages Rules

Theorem 4.

Consider

$$\begin{array}{cc}& \begin{array}{c}P\left.<\right|\left(X,Y\right)⊢P\left.<\right|X.\end{array}\end{array}$$

(12)

Theorem 5.

Consider

$$\begin{array}{cc}& \begin{array}{c}P\left|\equiv \right.\stackrel{K}{\to }Q,\end{array}\\ \begin{array}{c}P\left.<\right|{\left\{X\right\}}_{K^{-1}}⊢P\left.<\right|X.\end{array}\end{array}$$

(13)

Theorem 6.

Consider

$$\begin{array}{cc}& \begin{array}{c}P\left|\equiv \right.P\stackrel{K}{\leftrightarrow }Q,\end{array}\\ \begin{array}{c}P\left.<\right|{\left\{X\right\}}_{K^{}}⊢P\left.<\right|X.\end{array}\end{array}$$

(14)

Explanation. The above theorem states that if a subject has received a formula, and the main part knows the relevant secret key, we can infer that the body has received part of the formula.

(5) Belief Rules

Theorem 7.

Consider

$$\begin{array}{cc}& \begin{array}{c}P\left|\equiv \right.Q\left|~\right.\left(X,Y\right)⊢P\left|\equiv \right.Q\left|~\right.X.\end{array}\end{array}$$

(15)

Explanation. If P believes that Q has sent a $(X,Y)$ , then P believes that Q has sent message X.

3.3. SDN Trusted Domain Security Authentication Protocol's Formal Presentation

In this section, we formalize SDN trusted domain security authentication protocol:

$$\begin{array}{cc}& \begin{array}{c}R⟶N:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_1,{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\parallel {\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\parallel \mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_{\mathrm{I}\mathrm{D}}_R\right\}{R}^{-1}\right\}{N}_{\mathrm{P}\mathrm{U}\mathrm{B}},\end{array}\\ \begin{array}{c}N⟶R:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_1,{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\right)\parallel {\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\parallel \mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_{\mathrm{I}\mathrm{D}}_N\right\}{N}^{-1}\right\}{R}_{\mathrm{P}\mathrm{U}\mathrm{B}},\end{array}\\ \begin{array}{c}R⟶N:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{2}},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\parallel {\mathrm{A}\mathrm{K}}_R\right\}{R}^{-\mathrm{1}}\right\}{N}_{\mathrm{P}\mathrm{U}\mathrm{B}},\end{array}\\ \begin{array}{c}N⟶R:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{2}},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\right)\parallel \mathrm{A}\mathrm{C}\mathrm{K}\parallel \mathrm{A}\mathrm{K}\right\}{N}^{-\mathrm{1}}\right\}{R}_{\mathrm{P}\mathrm{U}\mathrm{B}},\end{array}\\ \begin{array}{c}R⟶N:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{3}},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\parallel \mathrm{C}\mathrm{S}\_{\mathrm{I}\mathrm{D}}_R\right\}\mathrm{A}\mathrm{K}\right\}{R}^{-\mathrm{1}},\end{array}\\ \begin{array}{c}N⟶R:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{3}},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\right)\parallel \mathrm{C}\mathrm{S}\_{\mathrm{I}\mathrm{D}}_N\right\}\mathrm{A}\mathrm{K}\right\}{N}^{-\mathrm{1}},\end{array}\\ R⟶N:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{4}},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\right\}\mathrm{A}\mathrm{K}\right\}{R}^{-\mathrm{1}},\\ \begin{array}{c}N⟶R:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{4}},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\right)\parallel \mathrm{A}\mathrm{C}\mathrm{K}\right\}\mathrm{A}\mathrm{K}\right\}{N}^{-\mathrm{1}}.\end{array}\end{array}$$

(16)

3.4. BAN Logic Security Goals

For security requirements of SDN trusted domains security authentication protocol, this paper sets up multiple security goals:

• (1)

$N\mid \equiv R\mid \equiv R\_\mathrm{P}\mathrm{C}\mathrm{R}\text{:}\hspace{0.17em}\hspace{0.17em}N$ believes that R is credible to believe $R\_\mathrm{P}\mathrm{C}\mathrm{R}$ .

(2)

$R\mid \equiv N\mid \equiv N\_\mathrm{P}\mathrm{C}\mathrm{R}\text{:}\hspace{0.17em}\hspace{0.17em}R$ believes that N is credible to believe $N\_\mathrm{P}\mathrm{C}\mathrm{R}$ .

(3)

$N\mid \equiv R\mid \equiv {\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\text{:}\hspace{0.17em}\hspace{0.17em}N$ believes that R is credible to believe ${\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R$ .

(4)

$R\mid \equiv N\mid \equiv {\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\text{:}\hspace{0.17em}\hspace{0.17em}R$ believes that N is credible to believe ${\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N$ .

(5)

$N\mid \equiv R\mid \equiv {\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_\mathrm{I}\mathrm{D}}_R\text{:}\hspace{0.17em}\hspace{0.17em}N$ believes that R is credible to believe ${\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_\mathrm{I}\mathrm{D}}_R$ .

(6)

$R\mid \equiv N\mid \equiv {\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_\mathrm{I}\mathrm{D}}_N\text{:}\hspace{0.17em}\hspace{0.17em}R$ believes that N is credible to believe ${\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_\mathrm{I}\mathrm{D}}_N$ .

(7)

$N\mid \equiv {\mathrm{A}\mathrm{K}}_R\text{:}\hspace{0.17em}\hspace{0.17em}N$ believes that ${\mathrm{A}\mathrm{K}}_R$ is credible.

(8)

$R\mid \equiv \mathrm{A}\mathrm{K}\text{:}\hspace{0.17em}\hspace{0.17em}R$ believes that AK is credible.

(9)

$N\mid \equiv R\mid \equiv \mathrm{C}\mathrm{S}\_{\mathrm{I}\mathrm{D}}_R\text{:}\hspace{0.17em}\hspace{0.17em}N$ believes that R is credible to believe $\mathrm{C}\mathrm{S}\_{\mathrm{I}\mathrm{D}}_R$ .

(10)

$R\mid \equiv N\mid \equiv \mathrm{C}\mathrm{S}\_{\mathrm{I}\mathrm{D}}_N,\hspace{0.17em}\hspace{0.17em}R\mid \equiv N\mid \equiv \mathrm{A}\mathrm{C}\mathrm{K}\text{:}\hspace{0.17em}\hspace{0.17em}R$ believes that N is credible to believe $\mathrm{C}\mathrm{S}\_{\mathrm{I}\mathrm{D}}_N$ .

(11)

R believes that N is credible to believe ACK.

3.5. BAN Logic Initialization Assumptions

In order to verify the authentication protocol compliance with BAN logic, we make the initialization assumptions of BAN logic:

$$\begin{array}{cc}& \begin{array}{c}R\left|\equiv \right.\stackrel{N_{\mathrm{P}\mathrm{U}\mathrm{B}}}{\to }N,\end{array}\\ \begin{array}{c}N\left|\equiv \right.\stackrel{R_{\mathrm{P}\mathrm{U}\mathrm{B}}}{\to }R,\end{array}\\ \begin{array}{c}N\left|\equiv \right.R\left|\Rightarrow \right.{\mathrm{A}\mathrm{K}}_R,\end{array}\\ \begin{array}{c}N\left|\equiv \#\right.\left(R\_\mathrm{P}\mathrm{C}\mathrm{R}\right),\end{array}\\ \begin{array}{c}N\left|\equiv \#\right.\left({\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right),\end{array}\\ \begin{array}{c}N\left|\equiv \#\right.\left({\mathrm{A}\mathrm{K}}_R\right),\end{array}\\ \begin{array}{c}R\left|\equiv \#\right.\left(N\_\mathrm{P}\mathrm{C}\mathrm{R}\right),\end{array}\\ \begin{array}{c}R\left|\equiv \#\right.\left({\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\right).\end{array}\end{array}$$

(17)

3.6. BAN Logic Secure Analysis

This section will use the BAN predicate logic inference to verify the authentication protocol's security goals, which is based on the BAN logic initialization assumptions of Section 3.5.

(1) Inference 1: From Step 1

$$\begin{array}{cc}& R⟶N:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(R_{{\mathrm{P}\mathrm{C}\mathrm{R}}_1},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\parallel {\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\parallel {{\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}}_{\mathrm{I}\mathrm{D}}}_R\right\}{R}^{-1}\right\}{N}_{\mathrm{P}\mathrm{U}\mathrm{B}}.\end{array}$$

(18)

• 〈1〉

  $\because N\mid \equiv \stackrel{R_{\mathrm{P}\mathrm{U}\mathrm{B}}}{\to }R$ ,

  $$\begin{array}{cc}& N\left.<\right|\left\{\mathrm{H}\mathrm{a}\mathrm{s}\mathrm{h}\left(R_{{\mathrm{P}\mathrm{C}\mathrm{R}}_1},{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\parallel {\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\parallel {\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}}_{{\mathrm{I}\mathrm{D}}_R}\parallel {\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}}_{{\mathrm{I}\mathrm{D}}_R}\right\}{R}^{-1}.\end{array}$$

  (19)

• 〈2〉

  ∴ From Theorem 1, we can infer

  $$\begin{array}{cc}& \begin{array}{c}N\left|\equiv \right.R\left|~\right.\left\{\mathrm{H}\mathrm{a}\mathrm{s}\mathrm{h}\left(R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_1,{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\parallel {\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\parallel \mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_{\mathrm{I}\mathrm{D}}_R\right\}{R}^{-1}.\end{array}\end{array}$$

  (20)

• 〈3〉

  ∵ From Theorems 5 and 7 $\hspace{0.17em}\hspace{0.17em}\therefore$ we can infer

  $$\begin{array}{cc}& \begin{array}{c}N\left|\equiv \right.R\left|~\right.R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_{\mathrm{1}},\end{array}\\ \begin{array}{c}N\left|\equiv \right.R\left|~\right.{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R,\end{array}\\ \begin{array}{c}N\left|\equiv \right.R\left|~\right.\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_{\mathrm{I}\mathrm{D}}_R.\end{array}\end{array}$$

  (21)

• 〈4〉

  $\because N\mid \equiv \#\hspace{0.17em}\hspace{0.17em}(R\_\mathrm{P}\mathrm{C}\mathrm{R})$ and $N\mid \equiv \#\hspace{0.17em}\hspace{0.17em}({\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R)$ and $N\mid \equiv \#\hspace{0.17em}\hspace{0.17em}(\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_{\mathrm{I}\mathrm{D}}_R)$ .

• 〈5〉

  ∴ From Theorem 2, we can get the conclusions

  $$\begin{array}{cc}& \begin{array}{c}N\left|\equiv \right.R\left|\equiv \right.R\_\mathrm{P}\mathrm{C}\mathrm{R},\end{array}\\ \begin{array}{c}N\left|\equiv \right.R\left|\equiv \right.{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R,\end{array}\\ \begin{array}{c}N\left|\equiv \right.R\left|\equiv \right.\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_{\mathrm{I}\mathrm{D}}_R.\end{array}\end{array}$$

  (22)

(2) Inference 2: From Step 2

$$\begin{array}{cc}& \begin{array}{c}N⟶R:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_1,{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\right)\parallel {\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\parallel {\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_\mathrm{I}\mathrm{D}}_N\right\}{N}^{-1}\right\}{R}_{\mathrm{P}\mathrm{U}\mathrm{B}}.\end{array}\end{array}$$

(23)

• 〈1〉

  Same as inference 1, we can get the conclusions

  $$\begin{array}{cc}& \begin{array}{c}R\left|\equiv \right.N\left|\equiv \right.N\_\mathrm{P}\mathrm{C}\mathrm{R},\end{array}\\ \begin{array}{c}R\left|\equiv \right.N\left|\equiv \right.{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N,\end{array}\\ \begin{array}{c}R\left|\equiv \right.N\left|\equiv \right.\mathrm{P}\mathrm{l}\mathrm{a}\mathrm{t}\_{\mathrm{I}\mathrm{D}}_N.\end{array}\end{array}$$

  (24)

(3) Inference 3: From Step 3

$$\begin{array}{cc}& \begin{array}{c}R⟶N:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_2,{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\parallel {\mathrm{A}\mathrm{K}}_R\right\}{R}^{-1}\right\}{N}_{\mathrm{P}\mathrm{U}\mathrm{B}}.\end{array}\end{array}$$

(25)

• 〈1〉

  $\because N\mid \equiv \stackrel{R_{\mathrm{P}\mathrm{U}\mathrm{B}}}{\to }R$ ,

  $$\begin{array}{cc}& \begin{array}{c}N\left.<\right|\left\{\mathrm{H}\mathrm{a}\mathrm{s}\mathrm{h}\left(R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_2,{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\parallel {\mathrm{A}\mathrm{K}}_R\right\}{R}^{-1}.\end{array}\end{array}$$

  (26)

• 〈2〉

  ∴ From Theorem 1, we can infer

  $$\begin{array}{cc}& \begin{array}{c}N\left|\equiv \right.R\left|~\right.\left\{\mathrm{H}\mathrm{a}\mathrm{s}\mathrm{h}\left(R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_2,{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\parallel {\mathrm{A}\mathrm{K}}_R\right\}{R}^{-1}.\end{array}\end{array}$$

  (27)

• 〈3〉

  ∵ From Theorems 5 and 7

  ∴ we can infer $N\mid \equiv R\mid ~{\mathrm{A}\mathrm{K}}_R.$

• 〈4〉

  $\because N\mid \equiv \#\hspace{0.17em}\hspace{0.17em}({\mathrm{A}\mathrm{K}}_R)$ .

  ∴ From Theorem 2, we can infer

  $$\begin{array}{cc}& \begin{array}{c}N\left|\equiv \right.R\left|\equiv \right.{\mathrm{A}\mathrm{K}}_R.\end{array}\end{array}$$

  (28)

• 〈5〉

  $\because N\mid \equiv R\mid \Rightarrow {\mathrm{A}\mathrm{K}}_R$ and $N\mid \equiv R\mid \equiv {\mathrm{A}\mathrm{K}}_R$ .

From Theorem 3, we can infer $N\mid \equiv {\mathrm{A}\mathrm{K}}_R$ .

(4) Inference 4: From Step 4

$$\begin{array}{cc}& \begin{array}{c}N⟶R:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_2,{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\right)\parallel \mathrm{A}\mathrm{C}\mathrm{K}\parallel \mathrm{A}\mathrm{K}\right\}{N}^{-1}\right\}{R}_{\mathrm{P}\mathrm{U}\mathrm{B}}.\end{array}\end{array}$$

(29)

• 〈1〉

  Same as inference 3, we can get the conclusions

  $$\begin{array}{cc}& \begin{array}{c}R\left|\equiv \right.\mathrm{A}\mathrm{K}.\end{array}\end{array}$$

  (30)

(5) Inference 5: From Steps 5 and 6

$$\begin{array}{cc}& \begin{array}{c}R⟶N:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(R\_{\mathrm{P}\mathrm{C}\mathrm{R}}_3,{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R\right)\parallel \mathrm{C}\mathrm{S}\_{\mathrm{I}\mathrm{D}}_R\right\}\mathrm{A}\mathrm{K}\right\}{R}^{-1},\end{array}\\ \begin{array}{c}N⟶R:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_3,{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\right)\parallel \mathrm{C}\mathrm{S}\_{\mathrm{I}\mathrm{D}}_N\right\}\mathrm{A}\mathrm{K}\right\}{N}^{-1}.\end{array}\end{array}$$

(31)

• 〈1〉

  Same as inference 1, we can get the conclusions

  $$\begin{array}{cc}& \begin{array}{c}N\left|\equiv \right.R\left|\equiv \right.\mathrm{C}\mathrm{S}\_{\mathrm{I}\mathrm{D}}_R,\end{array}\\ \begin{array}{c}R\left|\equiv \right.N\left|\equiv \right.\mathrm{C}\mathrm{S}\_{\mathrm{I}\mathrm{D}}_N.\end{array}\end{array}$$

  (32)

(6) Inference 6: From Step 8

$$\begin{array}{cc}& \begin{array}{c}N⟶R:\left\{\left\{\mathrm{H}\mathrm{M}\mathrm{A}\mathrm{C}\left(N\_{\mathrm{P}\mathrm{C}\mathrm{R}}_4,{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N\right)\parallel \mathrm{A}\mathrm{C}\mathrm{K}\right\}\mathrm{A}\mathrm{K}\right\}{N}^{-1}.\end{array}\end{array}$$

(33)

• 〈1〉

  Same as inference 1, we can get the conclusions

  $$\begin{array}{cc}& \begin{array}{c}R\left|\equiv \right.N\left|\equiv \right.\mathrm{A}\mathrm{C}\mathrm{K}.\end{array}\end{array}$$

  (34)

From the above BAN predicate logic inference, we can get that the conclusions conform to the BAN logic security goals which are defined in Section 3.4. Obviously, PCR, random numbers, and session key are important to the authentication protocol. From the BAN predicate logic inference, we have proved that sensitive information can meet the demands of network security.

4. Protocol Security Testing

This section will use the Dolev-Yao (DY) attack model [23] for actual security testing. The DY attack model could have the following variety of knowledge:

• (1)

Attackers are familiar with encryption, decryption, hashing, and other cryptographic operations, and they have the public key and private key of themselves.

(2)

Attackers hold the network identity and public key of each subject.

(3)

Attackers have basic password analysis ability.

Attackers could perform a variety of attacks, such as replay attack.

4.1. Security Goals

The DY attack model can control the entire network and catch the data for tampering attack and replay attack. For ensuring the protocol security, the authentication protocol must be detected by DY attack model. To this end, this paper sets up multiple security objections [24] for the DY attack model:

• (1)

$N\_\mathrm{P}\mathrm{C}\mathrm{R}/R\_\mathrm{P}\mathrm{C}\mathrm{R}$ value is confidential during transmission.

(2)

Random number, ${\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R/{\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_N$ , is confidential during transmission.

(3)

${\mathrm{A}\mathrm{K}}_R$ is confidential during transmission.

(4)

Controller platform ID/controller software ID is confidential during transmission.

(5)

Controller software authentication session key is confidential.

(6)

Successful certification logo (ACK) is completed.

4.1.1. Security Goals Formalization

In response to these security goals, this paper will test the safety of the authentication protocol using AVISPA network analysis tool. For testing protocol security, the AVISPA network interaction protocol security analysis system makes a formalized definition about test method of protocol security goals. Description is shown below.

(1) Information Confidential Test

Secret (E, id, S). This is a statement which means that subject S shares information E, and this secret is named an unchanged id which will be used in the goals definition.

(2) Information Verification Test

Witness  (A, B, id, E). This is a weak authentication attribute, which means that A declares that A has sent a message E to B, and this statement is named an unchanged id which will be used in the goals definition.

Request  (B, A, id, E). This is a strong authentication attribute, which means that B declares that B has received a message E from A, and this statement is named an unchanged id which will be used in the goals definition.

WRequest  (B, A, id, E). This is a weak authentication attribute, which is similar to Request  (B, A, id, E), but it does not verify replay attacks.

4.1.2. Modeling and Simulating Security Goals

In this section we will use HLPSL to build security goals modeling, which is based on formal definition of security objectives.

• (1)

For testing the security goals in Section 4.1.1, the authentication requesting platform needs to verify PCR, random numbers, and platform id of the authentication received platform. The HLPSL code appears as shown in Box 1.

(2)

Obviously, the authentication receiving platform also needs to verify PCR, random numbers, and platform id of the authentication requesting platform. The HLPSL code appears as shown in Box 2.

Box 1

Role sdnTNap_Init(A,B  : agent,

Kab  :symmetric_key,

H  :hash_func,

Ap_Start, Ap_Init, Ap_aSuccess  : text,

       SND,RCV: channel(dy)

)

played_by A

init State  :=0

transition

∧request(A,B,b_a_K1ab,K1ab＇)

∧request(A,B,b_a_SIGKpubKb,SIGKpubKb＇)

∧secret(K1ab＇,k1ab,{A,B})

∧request(A,B,b_a_bNonce,BNonce＇)

∧request(A,B,bpcr1,H(BPcr1＇.BNonce＇))

∧request(A,B,bpcr2,H(BPcr2＇.BNonce＇))

∧request(A,B,bpcr3,H(BPcr3＇.BNonce＇))

∧request(A,B,bpcr4,H(BPcr4＇.BNonce＇))

end role

Box 2

role sdnTNap_reply(A,B  : agent,

        Kab  : symmetric_key,

        H  : hash_func,

Ap_Start,Ap_Init,Ap_aSuccess,Ap_bSuccess  :

text,

        SND,RCV:

channel(dy)

)

played_by B

init State  :=1

transition

∧request(B,A,a_b_SIGKpubKa,SIGKpubKa＇)

∧request(B,A,a_b_aNonce,ANonce＇)

∧request(B,A,apcr1,H(APcr1＇.ANonce＇))

∧request(B,A,apcr2,H(APcr2＇.ANonce＇))

∧request(B,A,apcr3,H(APcr3＇.ANonce＇))

∧request(B,A,apcr4,H(APcr4＇.ANonce＇))

15.State = 15∧RCV(Ap_aSuccess＇) = |>

State＇:=17∧SND(Ap_bSuccess)

end role

4.2. Security Test

4.2.1. Test Scenarios

For the security goals, this paper sets up three test scenarios to verify whether the protocol satisfies the security goals or not. As shown in Table 1, in Scenario 1, we implemented a single session with all the roles played by legitimate agents. In Scenario 2 and Scenario 3 we tested the situations, in which the intruder would impersonate each of the legitimate agents: the authentication requesting controller platform (Scenario 2) and the authentication receiving controller platform (Scenario 3).

Table 1

Scenario description of security test.

Scenario	Scenario description
(1)	session(a,b,kab,h, ap_start,ap_init,ap_Asuccess,ap_Bsuccess)
(2)	session(a,i,kai,h, ap_start,ap_init,ap_Asuccess,ap_Bsuccess)
(3)	session(i,b,kib,h, ap_start,ap_init,ap_Asuccess,ap_Bsuccess)

4.2.2. Test Results

As shown in Boxes 3 and 4, the authentication protocol passed OFMC security test and ATSE security test, and the authentication protocol is not attacked by DY model, so we can conclude that the authentication protocol is secure.

Box 3:Security test result of OFMC system.

% OFMC

% Version of 2006/02/13

SUMMARY

 SAFE

DETAILS

 BOUNDED_NUMBER_OF_SESSIONS

PROTOCOL

 D:∖…∖NPLAB∖temp∖130476350162500000.if

GOAL

 as_specified

BACKEND

 OFMC

COMMENTS

STATISTICS

 parseTime: 0.00s

 searchTime: 0.04s

 visitedNodes: 1 nodes

 depth: 0 plies

Box 4:Security test result of ATSE system.

TYPED_MODEL

PROTOCOL

 D:∖…∖NPLAB∖temp∖130476352862187500.if

GOAL

 As Specified

BACKEND

 CL-AtSe

STATISTICS

 Analysed : 4 states

 Reachable : 0 states

 Translation: 0.14 seconds

 Computation: 0.00 seconds

From the summary details of Boxes 3 and 4, we can see that our authentication protocol is tested by CL-AtSe model and OFMC system, based on constraint logic, and our protocol was analyzed by 4 states. So, the conclusion of our test is quite convincing.

5. Performance Analysis

5.1. Calculation Consumption

This section uses the authentication response time defined in [25] to evaluate the calculation overhead of the protocol. The authentication response time (T) is mainly composed of three parts: the authentication requesting platform computing time ( $T_R$ ), the authentication receiving platform computing time ( $T_N$ ), and the protocol transmission time ( $T_T$ ). The following relationship can be obtained through the above three variables:

$$\begin{array}{cc}& T=T_R+T_N+T_T.\end{array}$$

(35)

Thus, we define the authentication requesting platform computing time including operation overhead of HMAC, digital sign, and encryption and decryption.

Similarly, we define the authentication receiving platform computing time including operation overhead of HMAC, digital sign, and encryption and decryption.

In particular, we consider that the ideal transport network excludes the impact of network latency.

According to the above definition, the calculation overhead of authentication protocol is mainly composed of HMAC, digital sign, message encryption and decryption, and the network transmission. As shown in Table 2, we make a detailed comparison between IKEv2, IDAKE-MA [26], and SKAP in this paper.

Table 2

Comparison in the performance of protocols.

Protocol	Communication	Communication between domains	Encryption/decryption	Digital sign	Hash/index calculation
IKEv2	12	5	0	14	0/0
IDAKE-MA	14	6	6	5	0/2
SKAP	10	4	4	3	0/2
Our method	8	8	8	8	8/0

It can be seen in Table 2 that the authentication protocol of this paper has higher calculation consumption compared with other domain protocols. In particular, we propose a no third party certification method. So our approach has advantages in communication frequency, which effectively reduces the total number of communications and network overhead. Furthermore, the authentication protocol is based on trusted computing, which effectively protects the credibility of network domains, and the trusted authentication protocol could make more advantages in security. Last but not the least, the authentication protocol does not have index calculation. Compared with other protocols in Table 2, our approach could significantly improve computational efficiency and reduce the cost of computing.

5.2. Storage Consumption

For the authentication protocol of this paper, we assume that the average frequency of the requester connecting to the receiver under random conditions is $1/T_{\mathrm{a}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}}$ , and the process of receiving request can be modeled as a Poisson process, where the average frequency is $1/T_{\mathrm{a}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}}$ . Using the receiver as an example, when the receiver receives a request message, the receiver needs to store the public key of the requester ( $R_{\mathrm{p}\mathrm{u}\mathrm{b}\mathrm{l}\mathrm{i}\mathrm{c}}$ ), the random number of the requester ( ${\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{e}}_R$ ), and the session key (AK) until the session is completed or the timer is over. We assumed the time of wait timer is $T_{\mathrm{l}\mathrm{i}\mathrm{f}\mathrm{e}\mathrm{t}\mathrm{i}\mathrm{m}\mathrm{e}}$ , the response time of receiving the message is $T_{\mathrm{r}\mathrm{e}\mathrm{q}}$ , and the packet loss rate of experiment network is $P_{\mathrm{l}\mathrm{o}\mathrm{s}\mathrm{s}}$ , and we derived that the storage average amount of the receiver is

$$\begin{array}{cc}& 2\times \left[\frac{1}{T_{\mathrm{a}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}}}\times T_{\mathrm{l}\mathrm{i}\mathrm{f}\mathrm{e}\mathrm{t}\mathrm{i}\mathrm{m}\mathrm{e}}\times P_{\mathrm{l}\mathrm{o}\mathrm{s}\mathrm{s}}+\frac{1}{T_{\mathrm{a}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}}}\times T_{\mathrm{r}\mathrm{e}\mathrm{q}}\times \left(1-P_{\mathrm{l}\mathrm{o}\mathrm{s}\mathrm{s}}\right)\right].\end{array}$$

(36)

Assuming the time of the latency timer is two times that of the response message time, we can further simplify that the storage average amount of the receiver is $T_{\mathrm{l}\mathrm{i}\mathrm{f}\mathrm{e}\mathrm{t}\mathrm{i}\mathrm{m}\mathrm{e}}/T_{\mathrm{a}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}}\times \left(P_{\mathrm{l}\mathrm{o}\mathrm{s}\mathrm{s}}+1\right)$ .

According to the above formula, on the one hand, if $T_{\mathrm{l}\mathrm{i}\mathrm{f}\mathrm{e}\mathrm{t}\mathrm{i}\mathrm{m}\mathrm{e}}$ and $T_{\mathrm{a}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}}$ remain unchanged, the storage consumption is proportional to the network packet loss rate. If the network is stable and packet loss rate is not high, the authentication protocol of proposed in this paper does not require a low storage space to store data, and the storage consumption is in the ideal range.

On the other hand, as shown in Figure 3, if $P_{\mathrm{l}\mathrm{o}\mathrm{s}\mathrm{s}}$ remains unchanged, the storage consumption is proportional to $T_{\mathrm{l}\mathrm{i}\mathrm{f}\mathrm{e}\mathrm{t}\mathrm{i}\mathrm{m}\mathrm{e}}$ and $T_{\mathrm{a}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}}$ . It means that if controllers' processing time is too long, the controller will continue to receive request, and thus the storage consumption will increase sharply.

Figure 3

The storage consumption of our method.

So far we assumed that the $P_{\mathrm{l}\mathrm{o}\mathrm{s}\mathrm{s}}$ rate remains unchanged. We further perform a comparative analysis with IKEv2, IDAKE-MA, and SKAP. The results are shown in Figures 4, 5, and 6; our method has more advantages in terms of storage consumption.

Figure 4

The storage consumption of SKAP.

Figure 5

The storage consumption of IDAKE-MA.

Figure 6

The storage consumption of IKEv2.

6. Conclusion

In this paper, we introduced and demonstrated a security authentication protocol of SDN trusted domain in ADS applications and designed the trusted domain network architecture to solve the credential problem of SDN architecture. The trust negotiation concept with nontrusted third party is a prerequisite for communication between different SDN trusted domains in ADS applications.

The main contributions are as follows: $(1)$ Our protocol does not contain any unnecessary information. We analyzed the redundant information by BAN logical system. The results show that the protocol is a concise protocol. $(2)$ The protocol is secure in theory. The BAN logic security analysis has proved that our protocol is secure. $(3)$ The protocol is secure in experiment. We demonstrate the security of our trusted domain authentication protocol by BAN logic and AVISPA security analysis tool, and we compared our trusted domain authentication protocol with other prevalent protocols in performance analysis. Our work fills the gap of mutual trust between different trusted domains and provides security foundation for interaction between different trusted domains.

In the paper we considered replay attacks and intermediator attacks. In the future, we plan to consider other attacker behavior models including opportunistic collusion attacks, random attacks, and insidious attacks to further demonstrate superiority of our protocol.