Satellite networks are recognized as the most essential communication infrastructures in the world today, which complement land networks and provide valuable services for their users. Extensive coverage and service stability of these networks have increased their popularity. Since eavesdropping and active intrusion in satellite communications are much easier than in terrestrial networks, securing satellite communications is vital. So far, several protocols have been proposed for authentication and key exchange of satellite communications, but none of them fully meet the security requirements. In this paper, we examine one of these protocols and identify its security vulnerabilities. Moreover, we propose a robust and secure authentication and session key agreement protocol using the elliptic curve cryptography (ECC). We show that the proposed protocol meets common security requirements and is resistant to known security attacks. Moreover, we prove that the proposed scheme satisfies the security features using the Automated Validation of Internet Security Protocols and Applications (AVISPA) formal verification tool and On-the fly Model-Checker (OFMC) and ATtack SEarcher (ATSE) model checkers. We have also proved the security of the session key exchange of our protocol using the Real or Random (RoR) model. Finally, the comparison of our scheme with similar methods shows its superiority.
Nowadays, mobile satellite networks are used to provide advanced personal communication services. These services complement terrestrial networks, providing benefits such as global coverage and increasing mobility and reliability for users. Satellite communications are valuable in an emergency and when other networks are unable to operate. Users can use satellite phones anytime and anywhere, including seas, islands, and high mountains, where land-based networks cannot provide services [
While there are many different types of satellites, Low-Earth-Orbit (LEO) satellites are used more in mobile communications. These satellites are at shorter distances from Earth, so they have higher signal strength and lower latency [
The LEO satellite is a land-based satellite located less than 2000 km above the earth, which enables communication between mobile devices and the network control center through gateways [
Because satellite communications are more susceptible to security attacks due to their broadcast nature, these communications need to be secure. Therefore, a session key is required for each communication session to encrypt the messages. There is also a need for strong authentication of both parties.
In recent years, various protocols for securing satellite communications have been proposed, most of which have security flaws. In particular, some authentication and key management protocols have provided ECC-based solutions leveraging the elliptic curve discrete logarithm problem (ECDLP) [
The contributions of this paper are as follows:
Analysis of key exchange protocol introduced by Qi et al. [ A secure ECC-based authentication and key exchange protocol that resists common attacks and meets common security requirements. A thorough security analysis of the proposed protocol and its resistance to various types of attacks. Formal security verification of the proposed protocol on AVISPA tool, considering different model checking techniques that the proposed protocol meets different security requirements. The proof of security of the proposed key exchange protocol using the RoR model.
The rest of the paper is structured as follows: In Section 2, some essential related works are discussed. Section 3 provides background information on elliptic curve cryptography and the threat models. Section 4 describes Qi et al.'s protocol [
To provide satellite communications over unsecured networks, Cruickshank [
Chen et al. [
Lee et al. [
Liu et al. [
Altaf et al. [
ECC uses the elliptic curve
The ECC
The building block for elliptic curve cryptography is the elliptic curve discrete logarithm problem: Given two points
To select a suitable elliptic curve, in addition to determining the values of
The most popular threat model is the Dolev-Yao model [
Suppose
The term syntax in Dolev-Yao model is defined in
The intruder in the Dolev-Yao model is one of the agents and has access to the hash function, public keys of all agents, his private key, and his shared key with other entities. Moreover, the intruder has full control over all communication messages between agents. He can eavesdrop, intercept, or replay the messages [
This section analyzes the protocol introdued by Qi et al. [
When the message is received, the NCC checks that the selected
We demonstrate that the protocol proposed by Qi et al. is vulnerable against attacks, as follows.
If the random parameters generated in a protocol are captured by the attacker, the session key should not be revealed. However, in the Qi et al.'s protocol, the session key
It is assumed that the internal attacker (here NCC) tries to obtain the password of each user. Since the user sends the
The proposed protocol uses elliptic curve encryption and consists of initialization, registration, and authentication and key agreement steps.
Symbol | Description | Symbol | Description |
---|---|---|---|
ECC parameters | The timestamp used by NCC in the |
||
Network control center | The timestamp used by the |
||
The low-earth-orbit satellite | NCC's public key | ||
The |
Ephemeral private key used by NCC in the |
||
The |
Ephemeral private key used by the |
||
The |
The cryptographic hash function | ||
The |
|| | The concatenation operation | |
NCC's ID | The bitwise XOR operation | ||
NCC's private key |
In this phase, the NCC sets some parameters to be used in authentication and key management. As explained in the previous section, to use the ECC cryptosystem, the NCC needs to set the five-tuple
To use the NCC services, the user needs to register first. The steps of user registration are depicted in
Finally, he sends the triple
Then, the NCC performs the XOR operation on
Finally, the NCC sends
Finally, he stores
Upon completion of the registration, the user and the NCC start a two-way authentication and key exchange process to communicate with each other via an insecure channel. A complete description of this phase is given in
If these two values are not the same, the user does not enter the correct ID and password, and the session ends. Here again, the primed form is used to indicate the recalculation of the variable in this step. Then the user's mobile device calculates the masked password
Then the mobile device calculates the masked identity of the user for this session as defined in
Finally, the mobile device sends the four-tuple
Moreover, the NCC computes
Note that here we use the double prime symbol to indicate that the variables are calculated in a new step of the protocol.
Then the NCC calculates
Then the NCC selects the ephemeral private key of the session,
Then, the mobile device checks whether
Finally, it sends
In this section, we describe the security features, the robustness against several security attacks of the proposed protocol, and formally verify the correctness of the proposed protocol in terms of satisfying security features using AVISPA.
Key agreement protocols require the parties to authenticate each other. In our proposed method, the user selects the ephemeral private key
The session key generated in the proposed method is shared between the user and the NCC, and no other entity can access the session key. The session key on the server-side is calculated with
The perfect forward secrecy guarantees the security of the session key, even though the long-term secret keys of parties are compromised. The proposed method preserves this feature because the session key is built using both long-term private keys and temporary secret keys. Even if the adversary
The proposed method does not send the user identity in plain text over insecure channels, but the masked user identity,
Our proposed method is resistant against the replay attack because, in addition to sending the timestamp
If the adversary
The user does not send the password to NCC in the registration phase explicitly but sends it in hidden form,
If the adversary
If the attacker accesses the temporary session parameters in any way, he should not be able to access the session key. Since the session key,
If the user's mobile device (or smart card) is stolen, the adversary
In our proposed method, NCC does not store any information about users other than their ID. Therefore, if the adversary accesses the NCC database, it will not receive any additional information.
Denial of Service attacks can be done on satellite communications entities, including the users and the NCC. By persuading the NCC to perform a large number of heavy-weight point multiplication operations on the elliptic curve, the attacker causes the NCC to crash and makes it impossible to provide services to authorized users. Our proposed protocol is resistant to this attack because if one of the users wants to carry out this attack against the NCC, he himself will suffer the same heavy-weight operations. Also, due to the resistance of the proposed method to replay attacks, the adversary is not able to resend the request message to the NCC. For the same reason, it is not possible to perform this attack on system users.
AVISPA is a role-based language that provides a formal language for specifying protocols and security properties and uses several back-ends to analyze them [
We have implemented our protocol in the HLPSL language. We have defined a role for the user,
The goal of
We examine semantic security of the session key of the proposed protocol using the Real-or-Random model [
Execute( Send( Reveal( Corrupt( Test(
G0. Game 0 is the real attack of
G1. In this game, we simulate passive attacks by the adversary. The adversary eavesdrops on messages between oracles
G2. In this game, in addition to simulating eavesdropping attacks, active attacks are also simulated with the Send query. Active attacks by the adversary can be one of three attacks: replay attack, man-in-the-middle, or impersonation attack. As stated in sections 6.2.1, 6.2.2, and 6.2.4, the proposed method is immune to these attacks. Therefore, the advantage of
G4. This game simulates the smart card loss attack. If the mobile device (or smart card) of the user is stolen,
Given that
In this section, we examine the computational complexity of the proposed method. The messages in the proposed protocol are obtained by combining xor, hash, and scalar multiplication on the elliptic curve. In calculating time complexity, we ignore the xor time execution, and we calculate the time required for hash and scalar multiplication based on the time reported in [
The time complexity of our protocol includes the time spent by the user's mobile device and the time spent by the NCC. The time spent by the mobile device is
To measure the communication cost of the proposed method, we need to measure the size of the messages exchanged between the different entities of the protocol. Messages consist of a combination of IDs, hash values, timestamps, and points on the elliptic curve. To calculate the communication cost, suppose each identifier is 64 bits long, the hash size is 256 bits, the timestamp is 64 bits, and the point size on the elliptic curve is 192 bits (due to secp192r1 selection).
To exchange the session key between the user and the NCC, it is necessary to send messages
At the end of this section, we compare the proposed method with several similar methods, which are all based on the ECDLP problem, in terms of security features and computational cost. As shown in
Tsai et al. [ |
Qi and Chen [ |
Qi et al. [ |
Altaf et al. [ |
Proposed | |
---|---|---|---|---|---|
Mutual authentication | ✓ | ✓ | ✓ | ✓ | ✓ |
Session key security | ✓ | ✓ | ✓ | ✓ | ✓ |
Perfect forward secrecy | ✓ | ✓ | |||
User anonymity | ✓ | ✓ | ✓ | ✓ | ✓ |
Replay attack resistance | ✓ | ✓ | ✓ | ✓ | ✓ |
Man-in-the-Middle attack resistance | ✓ | ✓ | ✓ | ✓ | ✓ |
Insider attack resistance | ✓ | ✓ | ✓ | ✓ | |
Impersonation attack resistance | ✓ | ✓ | ✓ | ✓ | ✓ |
Known-session-specific temporary information attack resistance | ✓ | ✓ | |||
Smart card loss attack resistance | ✓ | ✓ | ✓ | ✓ | ✓ |
Stolen verifier attack resistance | ✓ | ✓ | ✓ | ✓ | ✓ |
Dos attack resistance | ✓ | ✓ | ✓ | ||
Computational Cost (ms) | |||||
Communication Cost (bits) | 2560 | 2560 | 3712 | 2304 | 2816 |
This paper contributes towards the widespread deployment of satellite applications by tackling one of the main challenges, i.e., security issues. This paper first analyzed the authentication protocol for satellite communications proposed by Qi et al. and proved its vulnerability to two kinds of security attacks. Then this paper presented a robust secure authentication and key agreement protocol based on elliptic curve cryptography for secure satellite communications. Moreover, a thorough security analysis of the proposed protocol was performed. The security analysis showed that it is resistant to all known attacks. Besides, the formal verification of the proposed method proved that it satisfies the security requirements.
As future work, the protocol performance can be improved in terms of time execution by reducing the number of scalar multipliers while preserving the security requirements. Implementation on application in blockchain [