1 Introduction

With the continuous improvement of the mobile telecommunications industry, the study of wireless mobile network application has been a trending research topic. Mobile wireless networks have also been increasingly applied in human communications. The application of such networks overthrows traditional business models and motivates the exploration of new business opportunities. Meanwhile, people’s consumption habits and way of life are changing slowly. Smart cities have been constructed following the trend of mobile internet development. As a result, such cities have high intelligence, high resource utilization, affordable cost of living, and improved quality of life by utilizing information and communication technologies.

From the perspective of technology development, the construction of smart cities requires the realization of comprehensive perception, ubiquitous interconnection, pervasive computing, and integration application of Internet of Things(IoT) and cloud computing. Global Mobility Network (GLOMONET) based on 5G [1,2,3] mobile communication technology are the network infrastructure of smart cities. Such networks provide wireless connection maintenance anytime and anywhere and relay services to mobile users (MUs). A typical GLOMONET scenario has three participants, namely, the MU, the home agent (HA), and the foreign agent (FA). The authentication model of GLOMONET is called three-party authentication [4], which involves the three participants. In other words, the mutual authenticate of MU and FA require the help of HA.

Fig. 1
figure 1

Typical security scenarios of smart cities

A MU who registered in HA don’t usually stay in one place all the time, he/she can travel to anywhere within the scope of global mobile communication network and obtain the registered network service through the visited foreign agent. AS the MU enters the wireless network coverage of the FA, the FA can authenticate the MU through HA. On the other hand, MU can also verify the authenticity of FA and avoid connecting to Pseudo Base Stations (PBS). Mutual authentication is a very important security measure. It requires MU, FA and HA to authenticate each other before providing any network services, so as to avoid the risk of information leakage.

The GLOMONET suffers from various malicious attacks due to the opening and sharing characters of the wireless channel. Such attacks result in sensitive information leakage and communication failure. Currently, user authentication and privacy preserving are considered as both contact and contradiction issue when referring to GLOMONET. Therefore, designing a secure and robust protocol for roaming services in smart cities is a challenging task. Figure 1 indications some typical security scenarios that require identity authentication in smart cities, such as vehicle network, mobility network and telemedicine network.

Smart cities also have a few disadvantages. As the cities become smarter, they need more and more devices, such as street lights, public displays and so on, to integrate sensors, screens, batteries and processors. Once these devices run out of power or malfunctions, they will likely be thrown away and become e-waste. The components in electronic products contain a variety of toxic substances, which bring serious hazards to the environment and human health.

1.1 Related works

Numerous researchers have analyzed and designed security protocols and proposed various authentication protocols for GLOMONET. However, cryptanalysis shows that most protocols are insecure and cannot resist possible attacks, especially the denial of service (DoS) attacks.

Since Zhu et al. [5] presented a first authentication protocol for wireless network environment, many similar schemes have been put forward in decades. In these protocols, two-factor schemes based on passwords and smart cards have gained considerable attention because of their higher security compared with password-based schemes.

In 2011, He et al. [6] proposed an authentication scheme for GLOMONET environment, but Jiang et al. [7] indicated that this scheme have two security flaws and unable to achieve two-factor security. Subsequently they proposed an improved scheme based on quadratic residue. However, Wen et al. [8] found that the scheme in [7] cannot withstand spoofing, stolen verifier, and replay attacks. Then they designed a new authentication scheme for roaming environment. Farash et al. [9] and Gope et al. [10] exposed that the scheme in [8] is suffering from offline password guessing and forge attacks, and unfair key agreement. Then, they independently improved the scheme to fix these security flaws. However, Youngseok et al. [11] and Karuppiah et al. [12] individually proved that the scheme in [9] also has some weaknesses and cannot protect user privacy.

Authors of [13] analyzed the drawbacks in Mun et al.’s scheme [14]. They also pointed out that this scheme can neither prevent forgery and insider attacks nor provide mutual authentication. Then, they presented an improvement scheme without timestamp. Later, Wen et al. [15] found that the scheme in [16] is insecure against offline password guessing and impersonation attacks. After analyzing the security flaws of Miyoung et al.’s protocol [17], Karuppiah et al. [18, 19] put forward two enhanced authentication schemes for GLOMONET.

In 2016, Gope et al. [20] indicated that the scheme in [21] suffers from forgery and insider attacks. Then, on the basis of this scheme, a new lightweight authentication scheme is presented by Gope et al. Later, they proposed a new two-factor authentication scheme [22] to fix the security flaws in He et al.’s scheme [23]. However, Wu et al. [24] and Xu et al. [25] showed that Gope et al.’s scheme remains insecure because it is vulnerable to desynchronization and replay attacks.

Subsequently, Chaudhry et al. [26] designed a novel scheme to make up for the flaws of Farash et al.’s scheme [9]. However, Lee et al. [27] revealed that Chaudhry et al.’s scheme cannot withstand impersonation and stolen-mobile-device attacks. Later on, Fraz et al. [28] indicated that the protocol in [29] cannot provide user-anonymous and mutual authentication and resist replay and DoS attack. Then, Fraz et al. [28] presented a similar lightweight authentication scheme to fix the security weaknesses. In the same year, Chen et al. [30] discovered that a recent scheme [31] have several security flaws and unable to achieve mutual authentication. Hence, Chen improved the scheme for wireless communications networks.

In 2018, Madhusudhan et al. [32] discussed the security issues in Shin et al.’s scheme [18] and indicated that this scheme is inefficient and unsafe to stolen verifier, impersonation, DoS, insider, and synchronization attacks. Then, Madhusudhan enhanced the scheme to remedy these security drawbacks existing in [18]. Later on, a provable security scheme that utilizes random numbers to resist the desynchronization attack was proposed by Wu et al. [33].

Since 2020, a lot of authentication protocols for various IoT scenarios are proposed, such as IoT-based telemedicine network and intelligent transportation system. Li et al. [34] presented an identity based signature scheme for the IoT networks and claimed that their scheme can satisfy user anonymity and strong unforgeability. With regard to the limited resources of sensing nodes in IoT environment, Aydin et al. [35] proposed a lightweight group authentication schemes for wireless communication environments, which can be applied to different group authentication scenarios.

That same year, Kumar et al. [36] designed an authentication protocol based on Electrocardiogram (ECG) or Electroencephalogram (EEG) signals for Body Sensor Network (BSN). Everyone has different ECG and EEG signal which can be used for creating secure connection between patients and telemedicine system. Deebak et al. [37] found that the scheme in [38] cannot provide patient anonymity and suffers from health-report revelation and health-report forgery attacks. Then they put forward an improved service authentication framework for the Telecare Medical Information System (TMIS) and evaluated the algorithm efficiency by using Field Programmable Gate Array (FPGA) platform. Jangirala et al. [39] proposed a three-factor authentication scheme for IoT-based Intelligent Transportation System (ITS) which provides data transmission service and authentication service between vehicles to semi-trusted Cloud-Gateway (CG) node.

Recently, Physical Unclonable Functions (PUF) has been interested to many researchers by its unique physical characteristics. Several mutual authentication schemes [40,41,42,43] based on PUF have been proposed in the last year. Bansal et al. [40] presented a lightweight and privacy-preserving authentication scheme for Vehicle-to-Grid ecosystem (V2G) systems. Their scheme uses PUFs to verify the identity of an electric vehicles and the power grid. Shortly afterward, Alladi et al. [41, 42] put forward two lightweight mutual authentication schemes for Unmanned Aerial Vehicles (UAV) communication network. Focus of their studies are the research on security wireless data transmission between UAVs and its ground station. A more recent study [44] presented an anonymous ligthweight authentication scheme for group data sharing in opportunistic mobile social networks(OMSN), which provide privacy preservation of group users while sharing data in OMSN scenarios.

1.2 Our contributions

Main contributions of this study include:

  • Through a comprehensive analysis of relevant literature, we summarize and analyze the exclusive relationship between user anonymity and DoS attack resistance. The achievement of user untraceability must lead to DoS attack, and the achievement of DoS attack resistance is at the cost of sacrificing user anonymity.

  • Some security flaws in Xie et al.’s scheme [47], such as lack of local verification in the login phase and missing session key update phase, are highlighted. In addition, their scheme cannot work when numerous MUs from a same HA flood into an FA simultaneously.

  • An enhanced authentication protocol has been presented to balance the anonymous and security demand.

  • The proposed protocol is secured on the basis of the analysis of automated tools, namely, ProVerif and BAN logic. Moreover, the performance analysis shows that the new protocol has better efficiency compared with some current authentication protocols.

1.3 Organization of the paper

The remainder of this article is arranged as follows. Section 2 shows the mutually exclusive relationships of anonymous and DoS attack resistance. Section 3 discusses the scheme in [47] and analyzes its security flaws. A detailed description of the proposed scheme and its security analysis and formal security proof are provided in Sects. 4 and 5. Section 6 gives the functional and performance comparisons and some conclusions are drawn in the last section.

2 Anonymous and DoS attack

As in the description in [45], the definition of user anonymity is primarily directed against the client instead of the server. In addition, the notion of user anonymity in an authentication scheme has different scopes and meanings in different application scenarios. In general, user anonymity can be divided into two kinds, namely, weak and strong anonymity. The former refers to user identity protection, which ensures that no one is able to get the real identity of the MU except the respective HA. Meanwhile, the latter refers to user untraceability. User untraceability contains the user identity protection and unlinkable message. On this basis, the adversary neither obtains the real identities of users nor their current location and moving history through the user activities in roaming. Therefore, most researchers have designed anonymous authentication protocols with user untraceability because such protocols provide high-level user privacy protection. To achieve this goal and realize privacy protection, the MU must take some measures, such as dynamic identity and random number techniques, which can provide effective protection against eavesdropping and intercept attacks.

Through the above two techniques, the login request messages sent by the MU are different from each other. Thus, the message receiver, except for the HA, cannot identify the message senders. Even though numerous login request messages from the same MU are received, the FA also cannot identify the MU because each message is unique. Hence, the adversary can launch DoS attacks and send large amounts of randomly generated invalid login data intentionally to overwhelm the FA and HA because the FA believes that these messages belong to different MUs and forwards these messages to the HA following the rules of authentication protocol. This actions quickly exhaust network bandwidth and resources, possibly frustrating legal users to use the resources they needed. In accordance with references and research, user untraceability and DoS attack resistance is hardly achieved simultaneously because the two requirements are mutually exclusive. However, majority of current studies [6,7,8,9,10, 15,16,17,18, 18,19,22, 24, 29, 32, 33, 46,47,51] focuses on strong user anonymity. Hence, these studies fail to consider DoS attack prevention. As user anonymity is achieved, it becomes vulnerable to DoS attacks because the authentication protocols in GLOMONET require an FA to forward the login request messages of the MU to the HA unconditionally [4, 52]. Therefore, DoS attacks can be easily launched by an adversary to an HA through an FA.

An effective method to prevent DoS attacks is to use message-specific puzzles (i.e., client puzzles [53]). This method requires the FA to identify the message sender and send puzzle problems to the MU if the number of request messages exceeds a previously set threshold value. Evidently, the client puzzle techniques cannot provide user anonymity.

In this article, we discuss this topic and find measures to solve the problem, thus balancing the requirement of user untraceability and DoS attack resistance.

3 Brief review and security analysis of Xie et al.’s scheme

3.1 Brief review of Xie et al.’s Scheme

The scheme of Xie et al. [47] has three main phases, namely, registration, login, and authentication. Table 1 shows the notations of this paper.

Table 1 Notations

3.1.1 Registration

The MU should register with the HA to access the network services or obtain roaming services when visiting an FA. The registration process is depicted in Fig. 2.

3.1.2 Login and authentication

When an MU enters the coverage of an FA and wants to obtain the registered services from the FA, then the MU and the FA need to authenticate each other through the HA and establish the shared session key for securing communication. The detailed steps of this process are depicted in Fig. 3.

Fig. 2
figure 2

Registration process of Xie et al’s scheme

Fig. 3
figure 3

Login and authentication phases of Xie et al’s scheme

3.2 Security analysis of Xie et al.’s Scheme

3.2.1 Lack of input validation during the login process

To obtain the registered network services from the visited FA, the MU should first enter the user information (i.e. \( ID_{MU} \) and \( PW_{MU} \)), then generates the login message and send it to the FA. However, the user information is never inspected by the smart card in Xie et al.’s scheme. Therefore, even if user enters problematic data, accidentally or purposely, the login and the authentication are still performed until the HA discovers that the login message is illegal. These additional authentication steps reduce the efficiency of the authentication system and result in extra communication and computational overhead. We can avoid unnecessary operations by verifying the input information locally during login.

3.2.2 Lack of identification when numerous MUs visit an FA simultaneously

For instance, in a short period, numerous MUs from the same HA simultaneously roam into the coverage of the FA. These MUs send login requests to the FA, and the FA forwards these messages to the HA. After the successful authentication of login data, the HA replies \( \{E_{7}, E_{8}\} \) for every login message to the FA in a short period. However, the FA cannot identify every MU through the reply message \( \{E_{7}, E_{8}\} \) because the two hash values do not match the MU individually. Hence, Xie et al.’s scheme cannot complete the authentication under the circumstances.

3.2.3 Vulnerability to DoS attack

To achieve strong user anonymity, the scheme in [47] adopts the random number technique. Hence, every login request message based on a randomly selected number is different from each other. This weak point can result in adversary or malicious MUs to launch a DoS attack easily by generating substantial illegal login requests to the FA, and the FA directly forwards any unauthenticated login message to the HA. Lastly, the available service resources of the HA and the FA are exhausted quickly. As a result, these resources can no longer provide normal services to legitimate MUs.

3.2.4 Lack of session key update phase

If an MU stays in the coverage of an FA for a long period and keeps in touch with the FA, the MU and the FA must regularly update the session key for security reasons. However, the scheme in [47] disregards the issue on update session key and provides the specific update method.

4 Outline of our scheme

A new improved authentication scheme for smart city environment is put forward in this section.

4.1 Initialization

HA first selects the public parameters \( \{F_{p}, n, E, P, G, h(.), f() \} \), then generates a random number \( x \in Z_{n}^{*} \) as secret key. Next, HA establish the shared key \( K_{FH} \) with FA through a secure key agreement protocol. Finally, HA publishes the public parameters and keeps x secret.

4.2 Registration

When an MU joins the authentication system, the following steps should be performed to register on their HA. The details of the registration phases are shown in Fig. 4.

  1. Step 1.

    The MU first selects \( ID_{MU} \) and generates a random number \( r \in Z_{n}^{*} \). Next, the MU calculates \( PID_{MU}=h(ID_{MU} \parallel r) \) and sends \( \{ID_{MU}, PID_{MU}\} \) as a registration message to the HA.

  2. Step 2.

    Once the registration message is received, the HA computes \( Q_{MU}=h(PID_{MU} \parallel x) \), then generates a random nonce \( n_{HA} \in Z^{*} \) and calculates \( DID_{MU}=h(x) \oplus (PID_{MU} \parallel n_{HA}) \). Then, the HA stores \( \{DID_{MU}, Q_{MU}, h(.), P, ID_{HA}\} \) into a smart card (SC) and submits it to the MU.

  3. Step 3.

    The MU selects a password \( PW_{MU} \) and computes \( r^{*} = h(ID_{MU} \parallel PW_{MU}) \oplus r, V_{MU}=h(ID_{MU} \parallel PW_{MU} \parallel r), Q_{MU}^{*}=Q_{MU} \oplus r \) and finally stores \( \{r^{*}, V_{MU}, Q_{MU}^{*}, DID_{MU}, h(.), P, ID_{HA}\} \) into the SC.

Fig. 4
figure 4

Registration phase of the proposed scheme

Fig. 5
figure 5

Login and authentication phases of the proposed scheme

Fig. 6
figure 6

Session key update phase of the proposed scheme

4.3 Login and authentication

If an MU visits an FA and tries to obtain the registered services. At this time, the MU and the FA should complete mutual authentication through the HA. The details of this process is demonstrated in Fig. 5.

  1. Step 1.

    The MU enters \( ID_{MU} \) and \( PW_{MU} \) into the device terminal. Then, the SC in the terminal computes \( r=h(ID_{MU} \parallel PW_{MU}) \oplus r^{*} \) and checks \( V_{MU} ?= h(ID_{MU} \parallel PW_{MU} \parallel r)\). If the two values are unequal and the amount of password retries reached the predefined threshold(e.g. 3), then the login action is canceled; otherwise, the MU calculates \( PID_{MU}=h(ID_{MU} \parallel r) \) and \( Q_{MU}=Q_{MU}^{*} \oplus r \). Then, the MU takes the current timestamp \( T_{seed} \) as seed to generate a random number \( a=f(ID_{MU} \parallel T_{seed}) \), where f() is a number-generating function. The timestamp \( T_{seed} \) is stored for a certain period to resist the DoS attack (we use \( T_{AUTH} \) to represent the average time of authentication process, then the time interval can be set to \( T_{AUTH} \)). Later, the MU computes \( A_{1} =aP, A_{2}=h(DID_{MU} \parallel Q_{MU} \parallel A_{1} \parallel PID_{MU} \parallel ID_{FA} \parallel ID_{HA}) \) and sends \( M_{1}=\{ID_{FA}, ID_{HA}, DID_{MU}, A_{1}, A_{2}\} \) to FA.

  2. Step 2.

    Upon getting \( M_{1} \), FA first verifies the message to resist a potential DoS attack. The values \( A_{1} \) do not change during a given period (\( T_{AUTH} \)); thus, the FA has enough time to identify the MUs by comparing \( A_{1} \) in received messages. If the number of incoming messages from the same MU is greater than a previously set threshold value, then the FA can determine whether he/she is under DoS attack, terminate the session, and inform the HA. Otherwise, the FA generates a nonce \( b \in Z_{n}^{*} \) and further computes \( B_{1}=bP, B_{2}=h(M_{1} \parallel B_{1} \parallel K_{FH} \parallel ID_{FA} \parallel ID_{HA}) \). Then, the FA forwards \( M_{2}=\{M_{1}, B_{1}, B_{2}\} \) to the HA.

  3. Step 3.

    Upon receiving \( M_{2} \) from the FA, the HA initially checks whether \( B_{2} \) is equal to \( h(M_{1} \parallel B_{1} \parallel K_{FH} \parallel ID_{FA} \parallel ID_{HA}) \). The session is terminated if the two values are unequal; otherwise, the HA computes \( \{PID_{MU}, n_{HA}\} = h(x) \oplus DID_{MU}, Q_{MU}=h(PID_{MU} \parallel x) \) and checks \( A_{2}?=h(DID_{MU} \parallel Q_{MU} \parallel A_{1} \parallel PID_{MU} \parallel ID_{FA} \parallel ID_{HA}) \). If the result is equal, then the HA generates a random number \( n_{HA}^{new} \in Z^{*} \) and calculates \( DID_{MU}^{new}=h(x) \oplus (PID_{MU} \parallel n_{HA}^{new}) \). Then, the HA computes \( C_{1}=h(Q_{MU}) \oplus DID_{MU}^{new}, C_{2}=h(Q_{MU} \parallel A_{1} \parallel B_{1} \parallel DID_{MU}^{new}), C_{3}=h(K_{FH} \parallel A_{1} \parallel B_{1} \parallel ID_{FA} \parallel ID_{HA} \parallel C_{1} \parallel C_{2}) \). Lastly, the HA sends the message \( M_{3}=\{A_{1}, C_{1}, C_{2}, C_{3}\} \) to the FA.

  4. Step 4.

    After obtaining the reply message, the FA initially checks the validation of \( C_{3} \) by comparing it with \( h(K_{FH} \parallel A_{1} \parallel B_{1} \parallel ID_{FA} \parallel ID_{HA} \parallel C_{1} \parallel C_{2}) \). After successful verification, the FA generates the secret session key \(SK_{FA}=h(bA_{1})=h(abP) \) and \( B_{3}=h(SK_{FA} \parallel C_{1} \parallel C_{2}) \) and sends \( M_{4}=\{C_{1} \parallel C_{2} \parallel B_{1} \parallel B_{3}\} \) to the MU.

  5. Step 5.

    After \( M_{4} \) is received, the MU computes \( DID_{MU}^{new}=C_{1} \oplus h(Q_{MU}) \) and verifies \( C_{2}?=h(Q_{MU} \parallel A_{1} \parallel B_{1} \parallel DID_{MU}^{new}) \). If they are the same, then the MU computes the session key \( SK_{MU}=h(aB_{1})=h(abP) \) and checks \( B_{3} ?= h(SK_{MU} \parallel C_{1} \parallel C_{2} \) to authenticate FA. Lastly, the MU replaces \( DID_{MU} \) with \( DID_{MU}^{new} \). The mutual authentication procedure is then completed, and the shared session key \( SK_{FA}{/}SK_{MU} \) is established.

4.4 Password update

MU can update the password at any time through these steps.

  1. Step 1.

    MU first puts SC into the terminal device and enters \( ID_{MU}, PW_{MU} \).

  2. Step 2.

    SC computes \(r=h(ID_{MU} \parallel PW_{MU}) \oplus r^{*} \) and compares \( V_{MU} \) with \( h(ID_{MU} \parallel PW_{MU} \parallel r)\). If they are unequal, the phase is cancelled.

  3. Step 3.

    SC asks MU for new password \( PW_{MU}^{new} \).

  4. Step 4.

    Upon receiving \( PW_{MU}^{new} \), SC calculates \( r^{new*}=h(ID_{MU} \parallel PW_{MU}^{new}) \oplus r, V_{MU}^{new}=h(ID_{MU} \parallel PW_{MU}^{new} \parallel r), \) and replaces \( \{r^{*}, V_{MU} \}\) with \( \{r^{new*}, V_{MU}^{new} \} \).

4.5 Session key update

The shared session key should be updated regularly if MU stays in FA for a long period. Their ith session key \(SK_{i}(i=2;\ldots ;n) \) can be generated as follows. Figure 6 gives a detailed description about this phase.

  1. Step 1.

    MU first generates a number \( a_{i} \in Z_{n}^{*} \) randomly and calculates \( A_{i}=a_{i}P, A_{1}=h(A_{i} \parallel SK_{i-1})\) where \( SK_{i-1} \) is the \( (i-1)\)th session key, then MU sends \( M_{1}=\{A_{i}, A_{1}\}\) to FA.

  2. Step 2.

    FA compares \( A_{1} \) with \( h(A_{i} \parallel SK_{i-1})\). If they are unequal, the phase is cancelled. Otherwise, FA generates a random number \( b_{i} \in Z_{n}^{*} \) and computes \( B_{i}=b_{i}P, SK_{i}=h(b_{i}A_{i})=h(a_{i}b_{i}P), V_{i}=h(SK_{i} \parallel SK_{i-1}) \), then FA sends \( M_{2}=\{B_{i}, V_{i}\} \) back to MU.

  3. Step 3.

    When getting \( M_{2} \), MU calculates \( SK_{i}=h(a_{i}B_{i})=h(a_{i}b_{i}P) \) and checks \( V_{i}?=h(SK_{i} \parallel SK_{i-1}) \). If the two values are equal, the MU replaces \( SK_{i-1} \) with \( SK_{i} \).

5 Security analysis of our proposed scheme

This section first gives a formal proof using the BAN logic [54] and Proverif tool [55], and then provides an informal security analysis of the proposed scheme.

The significance of formal proof is to prove the security of the scheme logically, while the significance of informal security analysis is that some flaws cannot be discovered by formal security. Hence, the informal(traditional) analysis can be regarded as beneficial supplement to formal proof in terms of the aspect of security analysis.

5.1 Formal security analysis

We will provide a formal security proof with the BAN logic [54], which can prove whether a protocol can reach the target and help with the further improvement of the protocol.

To implement the BAN logic usually need to complete four steps: idealize the proposed scheme, make assumption, setting goal and analysis of the protocol. Table 2 lists the notations used in BAN logic.

Table 2 Notations of BAN logic

(1) The idealized form of the messages:

\( M_{1}.MU \rightarrow FA: \langle PID_{MU}, n_{HA} \rangle _{h(x)} , (ID_{FA}, ID_{HA}, A_{1})_{Q_{MU}} \)

\( M_{2}.FA \rightarrow HA: \langle PID_{MU}, n_{HA} \rangle _{h(x)} , (ID_{FA}, ID_{HA}, A_{1})_{Q_{MU}}, \{ \langle PID_{MU}, n_{HA} \rangle _{h(x)}, \) \((ID_{FA}, ID_{HA}, A_{1})_{Q_{MU}}, B_{1}\}_{K_{FH}} \)

\( M_{3}.HA \rightarrow FA: (A_{1}, B_{1},ID_{FA},ID_{HA},\langle DID_{MU}^{new} \rangle _{Q_{MU}},(A_{1},B_{1},DID_{MU}^{new})_{Q_{MU}},\)

\(MU {\mathop {\longleftrightarrow }\limits ^{A_{1}}} FA )_{K_{FH}}, \langle DID_{MU}^{new} \rangle _{h(Q_{MU})}, (A_{1},B_{1},DID_{MU}^{new})_{Q_{MU}} \)

\( M_{4}.FA \rightarrow MU: \langle DID_{MU}^{new} \rangle _{Q_{MU}}, (A_{1},B_{1},DID_{MU}^{new}, MU {\mathop {\longleftrightarrow }\limits ^{B_{1}}} FA )_{Q_{MU}},\)

\(( \langle DID_{MU}^{new} \rangle _{Q_{MU}}, (A_{1},B_{1},DID_{MU}^{new})_{Q_{MU}}, MU {\mathop {\longleftrightarrow }\limits ^{SK}} FA)_{SK} \)

(2) Initiative premises:

\(A_{1}: MU \ |\!\!\equiv \#(a)\). \(A_{2}: FA \ |\!\!\equiv \#(b) \).

\(A_{3}: FA \ |\!\!\equiv FA {\mathop {\longleftrightarrow }\limits ^{K_{FH}}} HA \). \(A_{4}: MU \ |\!\!\equiv MU {\mathop {\longleftrightarrow }\limits ^{Q_{MU}}} HA \).

\(A_{5}: FA \ |\!\!\equiv HA \Rightarrow MU {\mathop {\longleftrightarrow }\limits ^{A_{1}}} FA \). \(A_{6}: MU \ |\!\!\equiv HA \Rightarrow MU {\mathop {\longleftrightarrow }\limits ^{B_{1}}} FA \).

\(A_{7}: FA \ |\!\!\equiv MU \Rightarrow a \).

(3) Establishment of security goals:

\(G_{1}: MU \ |\!\!\equiv MU {\mathop {\longleftrightarrow }\limits ^{SK}}FA \)

\(G_{2}: FA \ |\!\!\equiv MU {\mathop {\longleftrightarrow }\limits ^{SK}}FA \)

\(G_{3}: MU \ |\!\!\equiv FA \ |\!\!\equiv MU {\mathop {\longleftrightarrow }\limits ^{SK}}FA \)

\(G_{4}: FA \ |\!\!\equiv MU \ |\!\!\equiv MU {\mathop {\longleftrightarrow }\limits ^{SK}}FA \)

(4) Scheme analysis:

From \( M_{3} \), we have

\( S_{1}: FA \triangleleft (A_{1}, B_{1},ID_{FA},ID_{HA},\langle DID_{MU}^{new} \rangle _{Q_{MU}}, (A_{1},B_{1},DID_{MU}^{new})_{Q_{MU}},\)

\(MU {\mathop {\longleftrightarrow }\limits ^{A_{1}}} FA)_{K_{FH}}\)

From \( S_{1} \) and \( A_{3} \) and message-meaning rule, we have:

\( S_{2}: FA\ |\!\!\equiv HA |\!\!\sim (A_{1}, B_{1},ID_{FA},ID_{HA},\langle DID_{MU}^{new} \rangle _{Q_{MU}},\)

\((A_{1},B_{1},DID_{MU}^{new})_{Q_{MU}},MU {\mathop {\longleftrightarrow }\limits ^{A_{1}}} FA)_{K_{FH}}\)

From \( S_{2} \) and \( A_{2} \) and the freshness conjuncatenation rule, we have

\( S_{3}: FA\ |\!\!\equiv HA\ |\!\!\equiv (A_{1}, B_{1},ID_{FA},ID_{HA},\langle DID_{MU}^{new} \rangle _{Q_{MU}},\)

\((A_{1},B_{1},DID_{MU}^{new})_{Q_{MU}},MU {\mathop {\longleftrightarrow }\limits ^{A_{1}}} FA)_{K_{FH}}\)

From \( S_{3} \) and the belief rule, we have

\(S_{4}: FA\ |\!\!\equiv HA\ |\!\!\equiv MU {\mathop {\longleftrightarrow }\limits ^{A_{1}}} FA \)

From \( S_{4} \) and \( A_{5} \) and the jurisdiction rule, we have

\(S_{5}: FA\ |\!\!\equiv MU {\mathop {\longleftrightarrow }\limits ^{A_{1}}} FA\)

According to \( S_{5} \) and \( SK=h(bA_{1})=h(aB_{1})=h(abP) \), we have

\(S_{6}: FA\ |\!\!\equiv MU {\mathop {\longleftrightarrow }\limits ^{SK}} FA \) \(\qquad (G_{2}) \)

From \( M_{4} \), we have

\( S_{7}: MU \triangleleft (A_{1},B_{1},DID_{MU}^{new},MU {\mathop {\longleftrightarrow }\limits ^{B_{1}}} FA)_{Q_{MU}} \)

From \( S_{1} \) and \( A_{4} \) and message-meaning rule, we have:

\( S_{8}: MU\ |\!\!\equiv HA |\!\!\sim (A_{1},B_{1},DID_{MU}^{new},MU {\mathop {\longleftrightarrow }\limits ^{B_{1}}} FA)_{Q_{MU}} \)

From \( S_{8} \) and \( A_{1} \) and the freshness conjuncatenation rule, we have

\( S_{9}: MU\ |\!\!\equiv HA\ |\!\!\equiv (A_{1},B_{1},DID_{MU}^{new},MU {\mathop {\longleftrightarrow }\limits ^{B_{1}}} FA)_{Q_{MU}} \)

From \( S_{9} \) and the belief rule, we have

\( S_{10}: MU\ |\!\!\equiv HA\ |\!\!\equiv MU {\mathop {\longleftrightarrow }\limits ^{B_{1}}} FA \)

From \( S_{10} \) and \( A_{6} \) and the jurisdiction rule, we have

\( S_{11}: MU\ |\!\!\equiv MU {\mathop {\longleftrightarrow }\limits ^{B_{1}}} FA \)

According to \( S_{11} \) and \( SK=h(aB_{1})=h(bA_{1})=h(abP) \), we have

\( S_{12}: MU\ |\!\!\equiv MU {\mathop {\longleftrightarrow }\limits ^{SK}} FA \) \(\qquad (G_{1}) \)

From \( M_{4} \), we have

\( S_{13}: MU \triangleleft ( \langle DID_{MU}^{new} \rangle _{Q_{MU}}, (A_{1},B_{1},DID_{MU}^{new})_{Q_{MU}}, MU {\mathop {\longleftrightarrow }\limits ^{SK}} FA)_{SK} \)

From \( S_{11} \) and \( S_{13} \) and the message-meaning rule, we have

\( S_{14}: MU\ |\!\!\equiv FA |\!\!\sim ( \langle DID_{MU}^{new} \rangle _{Q_{MU}}, (A_{1},B_{1},DID_{MU}^{new})_{Q_{MU}}, MU {\mathop {\longleftrightarrow }\limits ^{SK}} FA)_{SK} \)

From \( S_{14} \) and \( A_{1} \) and the freshness conjuncatenation rule, we have

\( S_{15}: MU\ |\!\!\equiv FA |\!\!\equiv ( \langle DID_{MU}^{new} \rangle _{Q_{MU}}, (A_{1},B_{1},DID_{MU}^{new})_{Q_{MU}}, MU {\mathop {\longleftrightarrow }\limits ^{SK}} FA)_{SK} \)

From \( S_{15} \) and the belief rule, we have

\( S_{16}: MU\ |\!\!\equiv FA\ |\!\!\equiv MU {\mathop {\longleftrightarrow }\limits ^{SK}} FA \qquad (G_{3}) \)

According \( S_{9} \) and \( A_{6} \) and belief rule, we have

\( S_{17}: FA |\!\!\equiv MU |\!\!\equiv B_{1} \)

From \( A_{7} \) and \( SK=h(aB_{1})=h(abP) \), we have

\( S_{18}: FA\ |\!\!\equiv MU |\!\!\equiv SK \)

From \( S_{6} \) and \( S_{18} \), we have

\( S_{19}: FA\ |\!\!\equiv MU |\!\!\equiv MU {\mathop {\longleftrightarrow }\limits ^{SK}} FA \qquad (G_{4}) \)

5.2 Security analysis with ProVerif

ProVerif is a popular and powerful formal protocol analysis tool that can automatically analyze protocols based on imported PV files. If the protocol has vulnerabilities, then the ProVerif tool obtains test result and a corresponding attack sequence. We will formally verify our protocol using the latest version of ProVerif tool (Ver2.00). A brief description of the code is provided as follows:

First, the used components, such as communication channels, shared keys, constants, function and equations, events, and queries, are defined in Fig. 7. Our verification code has four events and six queries. The four events are used to verify the authentication property of the MU and the FA. The first two queries are used to verify the secrecy of the session key. The middle two queries are used to test the security of the identity and password of the MU. The last two queries are used to test whether the events occur correctly. The processes of the MU, FA, and HA are illustrated in Figs. 89 and 10, respectively. We execute all the codes using the instruction “process !MU| !HA| !FA”. The execution results of the ProVerif tool only have two states: true and false. Any proposition must be either true or false. A true result indicates that the protocol has required an authentication property, whereas a false result means the protocol has vulnerabilities. Figure 11 shows the verification results of queries and events. As shown in the picture, all output results of the six queries are true. Therefore, the session key and privacy information of the MU are safe against a network attack. The first two results demonstrate that the adversary cannot obtain the shared session key. The third and fourth results demonstrate that the identity and password of the MU is secure. The last two results demonstrate that the events about the MU and the FA are started and terminated in the right order. Figure 12 shows the whole workflow of the ProVerif algorithms and the four dotted lines at the top indicates the flow of data. The authentication data set out from MU and return to MU.

Fig. 7
figure 7

Definitions

Fig. 8
figure 8

Process of MU

Fig. 9
figure 9

Process of FA

Fig. 10
figure 10

Process of HA

Fig. 11
figure 11

Results of the queries

Fig. 12
figure 12

The flowchart of the ProVerif algorithms

5.3 Informal security analysis

We will show that the proposed scheme can overcome the defect of the original scheme and satisfy all the secure requirements.

5.3.1 User anonymity and untraceability

The real identity of the MU is included in \( DID_{MU} \) and \( A_{2} \). The acquisition of hash value \( A_{2} \) is an one-way process from which we cannot get the original string back. In addition, the adversary cannot obtain \( ID_{MU} \) by computing \( DID_{MU} \) without the secret key x and random number \( n_{HA} \) of HA. Our scheme also supports user untraceability because every login request message and response message contain a randomly selected number. As such, the communication messages \( \{M_{1}, M_{2}, M_{3}, M_{4}\} \) are different every time and unlinkable. This unlinkability is the property that makes the attacker unable to trace user’s moving history. Hence, user anonymity and untraceability can be achieved in our scheme.

5.3.2 Local password verification

In the proposed protocol, the SC verifies the correctness of the entered user information of the MU through \( V_{MU} \) before sending a login request message to the FA. Without correct user information, the adversary cannot generate the correct r from \( r^{*} \) and pass the verification, thereby resulting in the immediate termination of the login phase. Hence, the proposed scheme supports local password verification and avoids unnecessary system overhead in communication and performance.

5.3.3 Resistance to DoS attacks

As stated in Section 1.2, user anonymity and resistance to DoS attacks are mutually contradictory. Thus, we take a middle-of-the-road approach to solve this difficult problem. In the login phase, the random number a is generated by \( f(ID_{MU} \parallel T_{seed}) \), where \( T_{seed} \) is kept in a preset time threshold (e.g., \( T_{AUTH} \)). Hence, the login request message \(M_{1}={ID_{FA}, ID_{HA}, DID_{MU}, A_{1}, A_{2}} \) does not change within this period. The FA can quickly find out the DoS attack through verifying the login messages sent from the MUs. A legal MU does not send numerous login request messages to the FA. Hence, our method does not decrease user anonymity. Above all, the proposed protocol can effectively prevent a DoS attack while protecting the MU’s privacy.

5.3.4 Resistance to impersonation attack

If an adversary wants to impersonate the MU, then the adversary must forge \( Q_{MU}=Q_{MU}^{*} \oplus r \). However, the value \( Q_{MU} \) cannot be forged because it is generated by the HA with the secret key x and \( PID_{MU} \). Therefore, our scheme can resist impersonation attacks. Without the secret keys \( K_{FH} \) and x, the adversary cannot forge a legal message \( B_{2}, C_{1}, C_{2} \), and \( C_{3} \). Therefore, impersonation attacks can be prevented in our protocol.

5.3.5 Mutual authentication

All the three entities can achieve mutual authentication through the transmitted messages. The HA can authenticate the FA by checking \( B_{2} \) and the MU through \( PID_{MU}, Q_{MU} \), and \( A_{2} \). Similarly, the FA can also authenticate the HA directly and the MU indirectly by checking the hash value \( C_{3} \). Lastly, the MU can authenticate the HA and the FA by examining \( C_{2} \) and \( B_{3} \), respectively.

5.3.6 Resistance to offline password guessing attacks with smart card security breach

We suppose the attacker gets \( \{r^{*}, V_{MU}, Q_{MU}^{*}, DID_{MU}\} \) from the MU’s smart card and the transmitted messages \( \{M_{1}, M_{2}, M_{3}, M_{4}\} \). The password of the MU is contained in \( r^{*}=h(ID_{MU} \parallel PW_{MU}) \oplus r, V_{MU}=h(ID_{MU} \parallel PW_{MU} \parallel r), Q_{MU}^{*}=Q_{MU} \oplus r= h(PID_{MU} \parallel x) \oplus r, DID_{MU}=h(x) \oplus (PID_{MU} \parallel n_{HA})=h(x) \oplus (h(ID_{MU} \parallel r) \parallel n_{HA}) \) and \( A_{2} \). As shown in these data, the adversary cannot retrieve the \( PW_{MU} \) unless he/she has \( ID_{MU} \) and r or obtains the secret key x, which is held by the HA. Hence, our scheme can prevent this type of guessing attack.

5.3.7 Resistance to replay attack

The numbers a and b in our scheme are individually chosen by the MU and the FA for each login and authentication. Thus, the transmitted messages constantly change in different sessions. If the adversary replays the eavesdropped messages, such as \( M_{1}, M_{2}, M_{3} \), and \( M_{4} \), then the MU, the FA, and the HA can easily detect this type of attack by comparing the received messages with the old messages.

5.3.8 Resistance to insider attack

In the registration phase, MU computes \( PID_{MU}=h(ID_{MU} \parallel r) \) and submits \( \{ID_{MU}, PID_{MU}\} \) to the HA. The password \( PW_{MU} \) of the MU is never sent to the HA. Evidently, a malicious insider user won’t get \( PW_{MU} \) and the proposed scheme is secure against this kind of attack.

5.3.9 Strong forward secrecy

Assume that an adversary obtains the previous session keys and retrieves the data in the smart card and long-term secret information of the MU and the HA, such as x. The adversary still cannot generate the current session key \(SK_{MU}(SK_{FA})\) because it contains one-time random nonce a and b. The current session key cannot be linked with previous session keys or any other secret data. Thus, the improved protocol achieves strong forward secrecy.

5.3.10 Fair key agreement

The shared session key in our scheme is \( SK_{MU}=SK_{FA}=h(abP) \), which is composed of two numbers and a public parameter P. The two numbers are generated by the MU and the FA independently. Hence, our scheme achieves fair key agreement.

5.3.11 Support the concurrent visit through many MUs

When numerous MUs from the same HA visits an FA in a short period, the visited FA receives numerous reply messages sent by the HA. Hence, we must take effective measures to help the FA match the reply messages with the MUs; otherwise, login and authentication end during the FA verification. In our improved scheme, each reply message from the HA to the FA contains value \(A_{1}\), which is generated by the MU. Hence, the FA can easily map every received message to every visited MU. Therefore, our scheme can cope with this issue.

5.3.12 Session key update regularly

If an MU stays in the network coverage of an FA for a long period, then the MU and the FA should update the shared session key periodically in case of potential network attacks and sensitive information leaks. The proposed scheme provides an efficient method to update the shared session key between the MU and the FA by taking advantage of previous session key and randomly chosen numbers.

5.3.13 Password update freely

Given people’s limited memory, the password chosen by the MU is usually short and easily remembered. Such password is vulnerable to brute force password attacks. In the proposed scheme, the password of the MU can be changed freely, thereby providing users with safe network services.

6 Functional and performance comparison

In this section, we analyze the functionality and give the performance comparison of the proposed scheme with recently works.

6.1 Functional analysis

The results of functionality comparisons are listed in the Table 3. As shown in the table, the new protocol satisfies all functionality requirements and more secure than other schemes.

Table 3 Functionality comparison

6.2 Performance analysis

We provide a simple performance comparison of the new protocol with those of other studies.

Some notations used to evaluate the performance are listed as follows:

  • \(T_{H}\): The time for a one-way hash operation.

  • \(T_{SE}\): The time for a symmetric encryption/decryption.

  • \(T_{M}\): The time for a multiplication operation in ECC.

  • \(T_{EXP}\): The time for a modular exponent.

Table 4 Time cost of related operations (ms)
Table 5 The comparisons of computation cost (ms)

Table 4 shows the execution time of the related operations following [56], which provides the computation cost of common operation and algorithm, such as hash, encryption/decryption, elliptic curve cryptography (ECC), and modular exponent. These results are to be achieved by using Pairing-Based Cryptography (PBC) library, as well as RSA and AES algorithm etc. The computer (Intel CPU E2200 2.20 GHz, 2 GB of RAM) used in [56] is not up-to-date, but all the results are obtained under the same test condition. Thus, these data are sufficient for comparison between different schemes.

Table 5 presents the performance comparison result between our scheme and those of other relevant studies. The table indicates that the new scheme has a lower computation cost compared with all other schemes, except for the scheme in [28]. However, the scheme in [28] has many security weaknesses, such as no resistance to replay attack and poor user anonymity.

7 Conclusion

In this study, we initially present a brief introduction of authentication protocols in smart cities based on GLOMONETs. Then, we summarize and analyze the contradictory relationships between user anonymity and DoS attack resistance. We find that many recent studies can achieve user anonymity, but they are vulnerable to DoS attacks. We analyze the security weaknesses of a recent authentication scheme and propose an improved one that balances DoS attack resistance and user anonymity to some extent. Results of security analyses and performance comparison illustrate that the improved scheme is secure and also meets all known security requirements. Furthermore, the proposed scheme has higher execution efficiency compared other schemes. It also has remarkable application potential to smart cities.