sensors

Article
Drone Secure Communication Protocol for Future Sensitive
Applications in Military Zone
Yongho Ko 1,† , Jiyoon Kim 2,† , Daniel Gerbi Duguma 2 , Philip Virgil Astillo 2 , Ilsun You 2, * and Giovanni Pau 3

1 Jeju Free International City Development Center, Jeju Island 63309, Korea; koyh0911@gmail.com
2 Department of Information Security Engineering, Soonchunhyang University, Asan-si 31538, Korea;
74jykim@sch.ac.kr (J.K.); 20189512@sch.ac.kr (D.G.D.); 20189093@sch.ac.kr (P.V.A.)
3 Faculty of Engineering and Architecture, Kore University of Enna, 94100 Enna, Italy; giovanni.pau@unikore.it
* Correspondence: isyou@sch.ac.kr
† These authors contributed equally to this work.

Abstract: Unmanned Aerial Vehicle (UAV) plays a paramount role in various fields, such as military,
aerospace, reconnaissance, agriculture, and many more. The development and implementation
of these devices have become vital in terms of usability and reachability. Unfortunately, as they
become widespread and their demand grows, they are becoming more and more vulnerable to
several security attacks, including, but not limited to, jamming, information leakage, and spoofing.
In order to cope with such attacks and security threats, a proper design of robust security protocols
is indispensable. Although several pieces of research have been carried out with this regard, there
are still research gaps, particularly concerning UAV-to-UAV secure communication, support for
perfect forward secrecy, and provision of non-repudiation. Especially in a military scenario, it
is essential to solve these gaps. In this paper, we studied the security prerequisites of the UAV





 communication protocol, specifically in the military setting. More importantly, a security protocol
(with two sub-protocols), that serves in securing the communication between UAVs, and between
Citation: Ko, Y.; Kim, J.; Duguma,
D.G.; Astillo, P.V.; You, I.; Pau, G.
a UAV and a Ground Control Station, is proposed. This protocol, apart from the common security
Drone Secure Communication requirements, achieves perfect forward secrecy and non-repudiation, which are essential to a secure
Protocol for Future Sensitive military communication. The proposed protocol is formally and thoroughly verified by using the
Applications in Military Zone. Sensors BAN-logic (Burrow-Abadi-Needham logic) and Scyther tool, followed by performance evaluation
2021, 21, 2057. https://doi.org/ and implementation of the protocol on a real UAV. From the security and performance evaluation, it
10.3390/s21062057 is indicated that the proposed protocol is superior compared to other related protocols while meeting
confidentiality, integrity, mutual authentication, non-repudiation, perfect forward secrecy, perfect
Academic Editor: Jingon Joung backward secrecy, response to DoS (Denial of Service) attacks, man-in-the-middle protection, and
D2D (Drone-to-Drone) security.
Received: 29 January 2021
Accepted: 10 March 2021
Keywords: drone; security; formal verification; vulnerability; D2D; D2GCS; attacks
Published: 15 March 2021

Publisher’s Note: MDPI stays neutral

with regard to jurisdictional claims in
1. Introduction
published maps and institutional affil-
iations. Unmanned Aerial Vehicles (UAVs) occupy an essential place in both military and
civilian applications by playing a core role in criminal investigations, public safety organi-
zations, transportation management facilities, and surveillance forces [1]. With the ability
of dynamic mobility, quick reaction, and ease of deployment, UAVs offer new possibilities
Copyright: © 2021 by the authors.
for different applications at a viable expense. In the last few years alone, networked UAVs
Licensee MDPI, Basel, Switzerland.
have been a dominating area of research for different business organizations, such as
This article is an open access article
Google, Facebook, Boeing, and Amazon.
distributed under the terms and High portability is one reason for interface twisting in UAV networking. Regardless
conditions of the Creative Commons of this, UAV-enabled systems support remote networks in the regions where physical
Attribution (CC BY) license (https:// interaction is troublesome or costly. It is apparent from the current research that UAVs
creativecommons.org/licenses/by/ are suitable for plenty of use cases, yet their deployments face a ton of difficulties and
4.0/). criticisms. Initially, the majority of the researches contend on the architectural structure

Sensors 2021, 21, 2057. https://doi.org/10.3390/s21062057 https://www.mdpi.com/journal/sensors

Sensors 2021, 21, 2057 2 of 25

of drone communication, which at present comes up short with regard to standard and
unification. In addition, UAV-aided communication systems experience the ill effects of
issues related to spectrum sharing [2].
Aside from these, UAV communications face specific issues identified with the architec-
tural plan, deployment, and consistency, with broad and dependable networks alongside
their security [3]. Normally, UAVs function remotely by receiving commands from the
ground control stations. These command and control messages are transmitted over various
channels with a variable transmission rate [4]. Since that information transmitted to/by
UAVs is mainly over the air, and most of the information transferred are highly sensitive and
critical [5], security is a primary concern in UAV communications. Therefore, the security of
these channels in UAV systems is one of the essential requirements for robust communication
between UAVs and/or between UAVs and the Ground Control Station (GCS).
The security vulnerabilities can prompt an assault on confidentiality, trustworthiness,
validness, and accessibility of UAVs. Generally, cryptographic mechanisms accomplish
message security and control signal assurance. Consequently, security concerns like unau-
thorized access, malicious control, unlawful association, or other malevolent attacks need
to be mitigated effectively with limited or no consequences on the performance [6]. Rec-
ognizable proof of threats and their defense in UAV systems are critical issues to be dealt
with by comprehensive and proficient methodologies.
Recently, a vulnerability has been discovered in the DJI UAVs that an attacker was
able to exploit to gain user account information, which then led to UAV hijacking [6]. The
attack is succeeded by intercepting users’ identification tokens by logging into the DJI
forums and acting as a legitimate user. It is often the case that the administrator of the
UAVs maintains information related to flight history, photographs taken during the flight,
payment information, real-time access rights of UAV cameras, and location information.
Accordingly, attacks on these devices, apart from other damages, may enable adversaries
to leak such crucial information and violate the security and privacy of users. In general,
UAVs lack suitable security mechanisms that protect them from various attacks while
taking a good balance between performance and safety [7].
Such security issues, especially in a military setting, may bring devastating effects that
put classified information in jeopardy. For instance, a session hijacking attack orchestrated
in a military scenario enables an attacker to extract previously exchanged information and
use it for different malicious activities. Additionally, communication among UAVs needs to
be secured since they usually work in collaboration to achieve a specific objective, such as
passing information in an ad-hoc manner. Another critical issue in the military environment,
where sensitive information is transmitted and commands are triggered, is maintaining
tractability. That is, any entity (UAV or GCS) should be accountable for its actions and
should not be able to repudiate it. Consequently, the main aim of this paper is to design a
secure UAV communication that is specially designed for military environments by which
perfect forward secrecy is maintained, UAV-to-UAV (and UAV-to-GCS) communications
are secured, and nonrepudiation is supported. The key contributions of this paper are
listed as follows:
• A new protocol for UAV-to-UAV and UAV-to-GCS is proposed,
• A formal security analysis of the proposed protocol using BAN-logic and Scyther tool
is carried out,
• A detailed comparative analysis based on security property and computational over-
head between the proposed and existing protocols is given,
• The protocol is also implemented on a real UAV (powered by Raspberry Pi) and a
Linux-based ground control station.
• The remainder of the paper is organized as follows: In Section 2, the state-of-the-art
study of existing drone communication protocols is described. In Sections 3 and 4, the
proposed protocol is presented in detail, and a formal security analysis of the protocol
is provided, respectively. In the final three sections, performance analysis, simulation
results, and conclusion of the paper are provided, respectively.
Sensors 2021, 21, 2057 3 of 25

2. Related Works
The development era of drones and communication technologies are tremendously
growing, where the various specialist service providers and equipment sellers are bringing
constant flow of new advancements, such as network accessibility [8], offloading strate-
gies [9], path planning [10], and various applications [11–13]. These enhancements go
hand in hand with industrial advancements, such as in References [14,15]. In particular
to UAVs, the ongoing improvements emphasize the information rate and security, which
includes secrecy, honesty, verification, and non-denial of transmitted information. UAVs
have a risk of information leakage as they are remotely controlled or operated through
predetermined missions in a resource-limited environment. With this regard, the cryp-
tographic mechanisms are well-known solutions against the attacks in most UAV-based
communications, which help to design robust security services. UAV communication, in
general, involves the drones, network providers, ground control stations, and trusted third
parties for authentications. Every entity plays a significant role in the entire communication
process to safeguard the system from security breaches. To this end, various researchers
have studied multiple security issues concerning UAVs, such as eavesdropping, network
jamming, weak authentication, and mobility management issues [16,17].
Seo et al. [18] proposed a security solution for drone-enabled delivery service by
utilizing White-Box Cryptography (WBC) as a product assurance instrument for UAV
landing points and cryptographic resources, alongside Public Key Infrastructure (PKI) as a
verification and non-repudiation technique. The principal goals of the proposed protocol
are assurance of a secret key, information protection during capturing, and secure storage
of information. The authors considered different security properties, such as confidentiality,
integrity, non-repudiation, authentication, and software protection. Kriz and Gabrlik [19]
proposed the UranusLink packet-oriented communication protocol with both non-reliable
and reliable transfer mechanisms that allow secure connection and packet loss detection.
The authors discussed various related issues such as security, low data throughput, ability
to data loss detection, and low latency. Won et al. [20] proposed a secure communication
protocol for drones and smart objects that depend on an efficient Certificateless Signcryp-
tion Tag Key Encapsulation Mechanism (eCLSC-TKEM). Islam et al. [21] presented a group
key distribution protocol for FANETs (Flying Ad hoc NETworks), which relies on a group
leader that discharges the base station for other operations. The authors considered dif-
ferent FANET requirements, such as node mobility and changes in the topology. Maxa
et al. [22] provided a protected UAV ad hoc reactive routing protocol (SUAP; Secure Uav
Ad hoc routing Protocol) that depends on public-key cryptography, hash chains, and geo-
logical lashes. It is utilized to ensure the route discovery component giving trustworthiness,
verification, and non-repudiation services, which is the expansion of the SAODV (Secure
Ad hoc On-demand Distance Vector) routing protocol.
Other related researches such as Blazy et al. [23] proposed UAV-GCS Secure Commu-
nication Protocol by using efficient cryptographic techniques to ensure the confidentiality
of sensed data. The authors highlight various interesting requirements, such as forensic-
resistant property of captured UAVs should not compromise the security of UAS (Un-
manned Aerial System) or the freshness of keys, to name a few. In addition, Wang et al. [24]
proposed a handover key management scheme for the LTE (Long-Term Evolution)-based
UAV control system to stress on the robust and secure connection to direct and control the
UAVs. The paper further discussed security prerequisites such as authentication, access con-
trol, confidentiality, integrity, and user plane traffic. A certificateless group authenticated
key agreement (CL-GAKA) scheme for secure communication among untrusted parties
is also proposed by Semal et al. [25]. The authors considered confidentiality, message
integrity, and authenticity requirements in UAV communication along with UAV-to-UAV
secure channel establishment, whereas UAV-to-Infrastructure communication, as well as
the routing problem, are not discussed.
Another study that examined the security requirements of UAV communications
is presented by He et al. [7]. The authors discussed specific attacks like GPS jamming,
Sensors 2021, 21, 2057 4 of 25

spoofing, and Wi-Fi attacks along with the countermeasures. Likewise, Kim et al. [26]
proposed a mechanism to confirm deletion activities in the wake of eradicating information,
regardless of whether control of a remotely conveyed UAV is lost. The authors utilized
a countdown-based approach and a hash chain to validate the sender of the received
messages to trigger the deletion activity, significantly after UAV communication was lost.
In connection to this, the security and privacy concerns of the Internet of Drones (IoD) is
studied by Wazid et al. [27]. The authors also proposed a centralized authentication and
key agreement scheme. The authors cover various security requirements but lack emphasis
on the forward and backward perfect secrecy and non-repudiation, which are the essential
requirements in critical and sensitive drone-oriented missions.

3. The Proposed Protocol

This section describes a security protocol used for UAVs to communicate with moni-
toring UAVs and GCS. The protocol is mainly designed to serve in a military environment
with two sub-protocols: SP-D2GS (Security Protocol for Drone-to-Ground Control Station)
and SP-D2MD (Security Protocol for Drone-to-Monitoring Drone).

3.1. Preliminary
Apart from their widespread usage in many application areas, UAVs have been
extensively used in military settings, especially for the purpose of surveillance, search and
rescue, national intelligence programs, reconnaissance, etc. [28]. Clearly, such operations
are sensitive by nature, due to the fact that they almost always involve national secrets.
Consequently, if exchanged information between the UAVs and the ground station are
disclosed, it may bring a lot of damages—from risking international relationships to serious
conflicts and wars. Thus, it is important to design a scheme that enables communicating
entities to establish a secure channel before exchanging any sensitive information. In this
section, such a security protocol that is particularly designed to operate in a military
environment is described.
The intended communication between the UAVs and the GCS can be arranged in a
direct or hierarchical fashion. In the former case, each of the participating UAVs exchange
information with the GCS independently. That is, the UAVs establish a secure channel with
the GCS first, and send the collected data through a wireless channel. Such arrangements
can be secured with the SP-D2GCS protocol (shown as the golden colored arrows in
Figure 1). For the hierarchical organization, a dedicated monitoring drone is responsible
to collect and transmit various data from each of the assigned UAVs to the GCS. The
monitoring drone, hence, acts as a middleman that executes the SP-D2MD protocol (shown
as the blue colored arrow in Figure 1) between the UAVs and itself, and then transmits
the collected data to GCS by using the SP-D2GCS security protocol. The details of these
sub-protocols will be described in Sections 3.3 and 3.4.
Prior to the execution of the proposed protocol, however, the UAVs and the GCS need
to be configured with the necessary information. First, the GCS generates the long-term
private and public keys for each UAV. Then, it prepares a certificate request (CSR), based on
their respective public keys and other information, and sends it to the Certificate Authority
(CA). Next, it prepares unique identities (ID) for each of the participants. Once the key
pairs, the certificates, and the IDs are ready, they will be securely delivered to each UAV, as
shown by the green arrows in Figure 1. Furthermore, GCS and UAVs are assumed to be
pre-configured with various cryptographic functions, such as digital signature algorithms
(e.g., ECDSA; Elliptic Curve Digital Signature Algorithm), encryption and decryption
function, cryptographic hash functions (e.g., HMAC; Hash-based Message Authentication
Code), pseudo-random number generators (PRNG), etc. It is also assumed that the GCS
and the UAVs are time-synchronized, and that the elliptic curve domain parameters (p, a,
b, G, n, and h) are decided ahead of the communication, and are known by each of the
communicating entities. Additionally, important information such as pre-shared keys (for
Sensors 2021, 21, 2057 5 of 25

instance PIN), IP address, type of UAV (monitoring or general drone), and operation ID
(IDMISSION ) are configured by the user before the UAVs start their mission.

Figure 1. Execution flow of the proposed protocol.

3.2. Threat Model

In computing, a threat can be understood as any incident that has the potential to
bring loss or harm to a system. Substantially, threats are events that aim at violating the
confidentiality, integrity, and availability properties of a computing system. Such threats
can happen due to different vulnerabilities, which are weaknesses in the system as a
consequence of design flaws, configuration mistakes, security policy inaccuracies, to name
a few. Consequently, anyone with malicious intent and technical capability can exploit these
vulnerabilities to launch an attack, thereby realizing the threats. Attacks can be orchestrated
by two classes of an adversary: insider or external. The former refers to malicious attacks,
such as replay, falsification, and masquerading, repudiation, or obstructions [29]. These
attacks are typically carried out by a foe with legitimate or authorized system access. The
latter represents attacks committed on a system network or computer system mainly either
by exploiting a vulnerability of the system or by social engineering. These are threat
actors that attempt to exploit security exposures, and they are generally located outside
the firewall.
More often than not, cryptographic protocols are intended to work in an open envi-
ronment where adversaries are capable of accessing the ciphered information exchanged
between communicating peers. Such security schemes are often modeled with the Dolev-
Yao (DY) threat model [30]. This model assumes an insecure public channel (which makes
the communicating entities untrustworthy) and powerful adversaries that are capable of
obtaining messages passing through the network, initiate and receive a conversation to
and from other participants, and able of impersonating other entities. Despite all these ca-
pacities of the attacker, there is off-limits information. Some of this information is guessing
random numbers generated from sample space and deciphering a ciphertext, enciphering
a plaintext, or getting the same HMAC value without the proper key. Consequently, the
protocol proposed in this work is modeled using the DY threat model, and only GCS is
assumed to be fully trusted.
The assumptions we took in designing this protocol are described as follows. It is
assumed that the elliptic curve domain parameters (p, a, b, G, n, and h) are decided ahead
of the communication and are known by each of the communicating entities. The GCS and
all affiliated drones can obtain a timestamp value indicating the current time, and have
time synchronization to verify the given timestamp value from the other party. The GCS
and all its drones have public/private key pairs and certificates supporting Elliptic Curve
Digital Signature Algorithm (ECDSA), GCS assigns IDs to the drones and monitoring
Sensors 2021, 21, 2057 6 of 25

drones, and the user plans the operation through the related application and selects the
drones included in the operation by using IDMISSION (the ID of the operation) and P (PIN
number), which are provided before the execution of the protocol.
The proposed protocol is required to satisfy important security requirements to with-
stand various attacks. Some of the most important requirements are:
• Mutual Authentication: for secure communication among a drone, a monitoring drone,
and a GCS, the communicating entities need to authenticate each other mutually.
• Strong Key Exchange: in order to assure the perfect forward secrecy of the protocol, a
strong key exchange should be executed in a way that generated session keys cannot
be recovered.
• Confidentiality: the information exchanged between the drones and between the
drone and the GCS should be protected from being accessed by unauthorized parties.
• Integrity: it is critical to assure the authenticity of the information (that the information
is not changed in between, and the source of information is genuine) exchanged
between the communicating ends.
• Non-repudiation: one of the essential security requirements in such scenarios is to
make sure that the action done by one party cannot be successfully denied without
others knowing about it.
• Perfect Forward Secrecy: this property assures communicating parties that even if an
adversary discloses a master key, old session keys will not be compromised.
• Perfect Backward Secrecy: this property assures the communicating entities that even
if an adversary discloses a master key, future session keys will not be compromised.
• Protection against Denial of Service: legitimate users, such as legitimate drones, should
not be denied service from a service provider, such as a GCS.
• Protection against MITM (Man-In-The-Middle) attack: the protocol prevents an at-
tacker from secretly relaying messages between the communicating ends.

3.3. SP-D2GCS
The drones and GCS should establish a secure channel and mutually authenticate each
other before exchanging any sensitive information. For this, a security protocol, SP-D2GCS
(Security Protocol for Drone-to-Ground Control Station), is needed that operates between
the drones and the GCS. In SP-D2GCS protocol, drones and a GCS securely communicate
to exchange telemetry and status information (from the drone to GCS) and commands
and controls (from GCS to the drones). The D2GCS protocol consists of four message
exchanges and is also compatible with the defacto MAVLink packet structure [31]. The
notations used in both sub protocols (SP-D2GCS and SP-D2MD) are described in Table 1.
The communication and packet structure of the D2GCS protocol is shown in Figure 2, and
the details of the proposed protocol are shown in Figure 3.
(1) The first thing that happens in the SP-D2GCS protocol is for D to get the operation
ID (IDMISSION ) and PIN (P) from the user. While doing so, or even before the actual
protocol session starts, it can generate a random ECDH private key dD ∈ {1 . . . n − 1},
where n is the order of the group generated by G. It then calculates the ECDH public
key QD = dD • G. Now, D is ready to create a message M1, containing IDMISSION ,
its certificate (CERTD ), the computed public key QD , and the current timestamp
ts1 , which is accompanied with the signature S1 computed by the ECDSA private
key PR(D). To allow GCS to prevent the resource exhaustion attacks caused by the
expensive public key operation, an HMAC is computed over the message M1 and
signature S1 using the PIN number, P. Finally, the message M1, with the signature S1
and the message digest, is sent to GCS.
(2) Upon receiving the message, GCS first checks its freshness by checking the included
timestamp ts1. Once ts1 is in the acceptable threshold, it then computes HM(P,
M1||S1), which is then compared with the received HMAC value. Note that doing
two such verifications before the expensive public key operation, i.e., the S1 verifi-
cation, helps to defend against resource exhaustion denial of service attacks. In a
Sensors 2021, 21, 2057 7 of 25

positive case, GCS checks the validity of the received certificate CERTD and verifies the
digital signature S1 by using the public key that belongs to CERTD . If the verification
of S1 holds, GCS successfully authenticates D. Now, GCS uses the same procedure D
followed to prepare the ECDH private key (dGCS ) and public key (QGCS = dGCS • G). It
then computes the master session key MSKD-GCS = dGCS •dD •G to produce the encryp-
tion and authentication keys. While the encryption key EKD-GCS (=HM(MSKD-GCS,
“D-GCS Encryption Key”||ts1)) is used to protect the confidentiality of the command
CMD sent to D, the authentication key AKD-GCS (=HM(MSKD-GCS , “D-GCS Authen-
tication Key”||ts1 )) assures the authenticity and integrity of this command. GCS
then arranges a message M2 (containing IDMISSION , CERTGCS , QGCS , and ts2 ) and
signs that message with its ECDSA private key PR(GCS), followed by encrypting
the command CMD with the encryption key EKD-GCS and computing HM(AKD-GCS ,
M2|| E(EKD-GCS , CMD)). Finally, GCS sends the message M2, the signature S2, the
encrypted command, and the HMAC value to D.
(3) Once D gets the message, it verifies the timestamp ts2 and the digital signature S2 to
authenticate GCS. Next, it generates the master session key MSKD-GCS , from which
the encryption and authentication keys EKD-GCS and AKD-GCS are derived using the
same procedure as shown in step (2). Afterward, D computes the HMAC value
and verifies if it is the same as the one it received. In turn, it extracts the operation
command CMD by decrypting the received cipher using EKD-GCS . To proceed with
the next step, D further composes a message M3 (containing IDMISSION , IDD , IDGCS ,
and ts3 ), concatenates it with the deciphered CMD, and signs the result by computing
S(PR(D), M3||CMD). It also calculates HM(AKD-GCS , M3||S3), which is, in turn,
sent together with the message M3 and the digital signature S3 to GCS.
(4) Upon receipt of the message, GCS verifies the timestamp ts3 and the HMAC value
before confirming the validity of the digital signature S3. If S3 is valid, GCS can be
sure that D has successfully received the operation command CMD. S3 also plays an
important role in fulfilling the non-repudiation property of the protocol by making
sure that D cannot deny that it received the CMD. Similarly, GCS allows D to prove
that it has sent an operation command CMD via the digital signature S4 (=S(PR(GCS),
M4||CMD)). Besides, the HMAC value is calculated based on AKD-GCS to counter
the threat of the resource exhaustion attacks due to the public key operation. Note
that in the SP-D2GCS protocol, GCS computes and transmits optional parameters
that will be used for scenarios where drones communicate with their monitoring
drone. In such scenarios, it prepares for a ticket that contains a session key SK
and its lifetime LT along with the IDs of D and its monitoring drone MD. In more
detail, GCS computes ENC(D) = E(EKD-GCS , IDD ||IDMD ||IDGCS ||SK||LT||ts4 )
and ST(D) = E(EKGCS-MD , IDMISSION ||IDD ||IDMD ||IDGCS ||SK||LT||ts4 ) for D
and MD, respectively. Finally, the GCS sends the message M4 (optionally including
ENC(D) and ST(D)), the digital signature S4, and the HMAC value. The protocol
is concluded after D validates the included ts4 , HMAC value, and S4, respectively.
Similar to S3, S4 supports non-repudiation. If ENC(D) and ST(D) are given, D recovers
the session key SK by decrypting ENC(D) with EKD-GCS .

Figure 2. D2GCS communication and packet structure.

Sensors 2021, 21, 2057 8 of 25

Table 1. Notations and their meaning.

Notation Description
D Drone.
MD Monitoring Drone.
GCS Ground Control Station.
ECDH Elliptic Curve Diffie–Hellman.
ECDSA Elliptic Curve Digital Signature Algorithm.
HMAC Hash-based Message Authentication Code
IDMISSION Operation ID.
P PIN number.
dX X’s ECDH Private key.
QX X’s ECDH Public key: dX • G.
PU(X) X’s ECDSA Public key.
PR(X) X’s ECDSA Private key.
HM(K, M) An HMAC function where K is a secret and M is an input message.
CERTX X’s Digital Certificate.
ts Timestamp.
CMD Operation command.
SK Session key.
MSKX-Y Master session key shared between X and Y.
EKX-Y Encryption key shared between X and Y.
AKX-Y Authentication key shared between X and Y.
ST(X) X’s Authentication Ticket.
LT Key life cycle (Lifetime).
E(K, M) An encrypt function where K is a secret key and M is an input message.
D(K, C) A decrypt function where K is a secret key and C is a cipher message.

3.4. SP-D2MD
For cases where a dedicated monitoring drone is required to collect information
from different general drones and pass this information to the ground station, a separate
security protocol is required. Consequently, the SP-D2MD (Security Protocol for Drone-to-
Monitoring Drone) protocol is used between a general drone D and a monitoring drone MD
to perform mutual authentication and key exchange, thereby protecting their subsequent
communications. Once all the information is collected by the MD, the MD uses the SP-
D2GCS protocol to pass this information to GCS and receive different commands and
controls from it. The communication and packet structure of this sub-protocol is shown in
Figure 4, and the details are depicted in Figure 5.
(1) Note that during the D2GCS protocol session, D received the session key SK and the
corresponding ticket ST(D) that allow itself to execute mutual authentication and key
exchange with MD. To start this protocol, D first generates its ECDH public key pair
dD and QD , before composing a message M1 containing IDMISSION , IDGCS , ST(D), IDD ,
QD , and ts1 . It, in turn, calculates HM(SK, M1), which is sent to MD along with M1.
(2) On receiving the message, MD verifies its freshness and decrypts ST(D) with EKGCS-MD
to extract SK, which is then used to verify the received HM(SK, M1). After that, it
generates the ECDH public key pair dMD and QMD , computes a master session key
MSKD-MD , and computes EKD-MD and AKD-MD . Finally, D generates the two HMAC
values, HM(AKD-MD , M2) and HM(SK, M2|| HM(AKD-MD , M2)), which are then
sent to MD along with M2.
(3) After verifying the received ts2 and HM(SK, M2|| HM(AKD-MD , M2)), D com-
putes MSKD-MD , EKD-MD , and AKD-MD . With AKD-MD , HM(AKD-MD , M2) is ver-
ified, followed by sending MD a message M3 (= IDMISSION , IDD , IDMD , ts3 ) with
HM(AKD-MD , M3). Finally, MD concludes this protocol by verifying the included
ts3 and HM(AKD-MD , M3). The positive result enables MD to confirm the valid
key exchange.
Sensors 2021, 21, 2057 9 of 25

Figure 3. SP-D2GCS protocol.

Sensors 2021, 21, 2057 10 of 25

Figure 4. D2MD communication and packet structure.

Figure 5. SP-D2MD protocol.

4. Formal Security Analysis

This section puts forward the formal analysis of the proposed security protocols
described in Section 3. The formal security analysis verifies whether the security protocol
actually satisfies the targeted security requirements and services or not. In the past few
years, the research on formal security analysis has been continuously conducted. In this
paper, the proposed protocols are formally verified through modal-logic-based analysis,
such as BAN Logic [32], and automation tool, such as Scyther [33].
Sensors 2021, 21, 2057 11 of 25

4.1. Formal Verification with BAN-Logic

Named after its three authors, Burrows, Abadi, and Needham, BAN logic has become
one of the most used verification methods to analyze security protocols formally. BAN-
Logic consists of different notations and rules that are used for formal verification.
In general, formal verification through BAN-Logic is carried out in four steps: (1) ide-
alization, (2) assumption, (3) goals, and (4) derivation. The analysis starts by idealizing
the messages exchanged between the communicating parties by representing them into
suitable format by which only encrypted (non-plaintext) messages are considered. Once the
messages are put in this format, underlying assumptions regarding the original messages
are made and formally expressed. Next, the goals are defined and expressed formally.
Finally, the goals are derived by using the BAN-Logic rules, the assumptions, and the
intermediate results. Here, ‘I’, ‘A’, ‘G’, and ‘D’ are used to denote idealizations, assump-
tions, goals, and derivations. Tables 2 and 3 summarize the BAN-Logic notations and
rules, respectively.

Table 2. BAN-Logic Notations.

Notations Meanings
P believes X P believes that the message X is true
P sees X P receives the message X at any point in time
P said X P previously sent the message X
P controls X P has jurisdiction over X
Fresh ( X ) X is fresh
K
P↔Q K is a secret key shared between P and Q
K
→P K is the P’s public key and L is the P’s private key
K
P⇔Q K is a shared secret between P and Q
{ X }K X is encrypted with a key K
X, Y X is combined with Y

Table 3. BAN-Logic Rules.

Rule Names Rules

Message Meaning Rule K
P believes P↔ Q, P sees { X }K P believes P⇔K K
Q, P sees XK P believes → Q, P sees { X } L−1
(MM) P believes Q said X P believes Q said X P believes Q said X

Nonce Verification Rule P believes #( X ), P believes Q said X

(NV) P believes Q believes X

Jurisdiction Rule P believes Q controls X, P believes Q believesX

(JR) P believesX

Freshness Rule P believes f resh( X )

(FR) P believes f resh( X,Y )

Decomposition Rule P sees ( X, Y )

(DR) P sees X

Belief Conjunction Rule P believes X, P believes Y P believes Q believes ( X,Y ) P believes Q said ( X,Y )
(BC) P believes( X,Y ) P believes Q believes X P believes Q said X

Diffie–Hellman Rule gY gX gY gX
P believes Q said → Q, P believes → P P believes Q said → Q, P believes → P
(DH) g XY g XY
P believes P ↔ Q P believes P ⇔ Q

4.1.1. SP-D2GCS
1. Idealization
The SP-D2GCS protocol is formulated into the following four idealizations.
Sensors 2021, 21, 2057 12 of 25

(I1) D → GCS : h D MISSION , g x , ts1 i p

AK EK
(I2) GCS → D : h ID MISSION , gy , ts2 , CMD, GCS ↔ D, GCS ↔ D i AK , { gy , ts2 } PU (GCS)−1
AK EK
(I3) D → GCS : h ID MISSION , IDD , IDGCS , ts3 , CMD, GCS ↔ D, GCS ↔ D i AK
(I4) GCS → D : h ID MISSION , IDGCS , IDD , ts4 , CMD i AK
2. Assumptions
The assumptions taken in the process of verification are listed below. While the
assumptions A1–A4, A6, and A10 are with respect to GCS, the rest are taken by D.
P
(A1) GCS believes GCS ⇔ D
(A2) GCS believes f resh(ts1 )
gY
(A3) GCS believes → GCS
PU ( GCS)
(A4) D believes → GCS
(A5) D believes f resh(ts2 )
gX
(A6) D believes →D
(A7) D believes f resh(ts1 )
(A8) G believes f resh(ts3 )
(A9) D believes f resh(ts4 )
SK
(A10) D believes GCS control D ↔ MD
3. Goals
The goals that are expected to be met by the SP-D2GCS protocol are listed below. They
primarily illustrate mutual authentication and secure key exchange between D and GCS.
(G1) GCS believes D believes ID MISSION
AK
(G2) GCS believes GCS ↔ D
EK
(G3) GCS believes GCS ↔ D
AK
(G4) D believes GCS ↔ D
EK
(G5) D believes GCS ↔ D
(G6) D believes GCS believes ID MISSION
(G7) D believes GCS believes CMD
AK
(G8) D believes GCS believes GCS ↔ D
EK
(G9) D believes GCS believes GCS ↔ D
(G10) GCS believes D believes IDD
(G11) GCS believes D believes CMD
AK
(G12) GCS believes D believes GCS ↔ D
EK
(G13) GCS believes D believes GCS ↔ D
(G14) D believes GCS believes IDGCS
SK
(G15) D believes GCS believes D ↔ MD
SK
(G16) D believes D ↔ MD
4. Derivations
Based on the idealizations, the assumptions, the BAN-logic rules, and the intermediate
results of the derivations, the goals set are deduced.
From (I1):
(D1) GCS sees h ID MISSION , g x , ts1 i p
(D2) GCS believes D said [ ID MISSION , g x , ts1 ] by ( D1), ( A1), MM
(D3) GCS believes D believes [ ID MISSION , g x , ts1 ] by ( D2), ( A2), FR, NV
(D4) GCS believes D said ID MISSION by ( D3), BC
Sensors 2021, 21, 2057 13 of 25

g XY
(D5) GCS believesGCS ↔ D by ( D2), BC, ( A3), DH
AK
(D6) GCS believesGCS ↔ D by ( D5), ( A2), BC
EK
(D7) GCS believesGCS ↔ D by ( D5), ( A2), BC
From (I2):
AK EK
(D8) D seesh ID MISSION , gy , ts2 , CMD, GCS ↔ D, GCS ↔ D i AK , h gy , ts2 i PU (GCS)−1
(D9) D believes GCS said [ gy , ts2 ] by ( D8), BC, ( A4), MM
(D10) D believes GCS believes [ gy , ts2 ] by ( D9), ( A5), FR, NV
g XY
(D11) D believesGCS ↔ D by ( D9), BC, ( A6), DH
AK
(D12) D believes GCS ↔ D by ( D11), ( A7), BC
EK
(D13) D believes GCS ↔ D by ( D11), ( A7), BC
AK EK
(D14) D sees h ID MISSION , gy , ts2 , CMD, GCS ↔ D, GCS ↔ D i AK by ( D10), DR
h i
AK EK
(D15) D believes GCS said ID MISSION , gy , ts2 , CMD, GCS ↔ D, GCS ↔ D
by ( D14), ( D12), MM h i
AK EK
(D16) D believes GCS believes ID MISSION , gy , ts2 , CMD, GCS ↔ D, GCS ↔ D
by ( D15), ( A5), FR, NV
(D17) D believes GCS believes ID MISSION by ( D16), BC
(D18) D believes GCS believes CMD by ( D16), BC
AK
(D19) D believes GCS believes GCS ↔ D by ( D16), BC
EK
(D20) D believes GCS believes GCS ↔ D by ( D16), BC
From (I3):
AK EK
(D21) GCS sees h ID MISSION , IDD , IDGCS , ts3 , CMD, GCS ↔ D, GCS ↔ D i AK
h i
AK EK
(D22) GCS believes D said ID MISSION , IDD , IDGCS , ts3 , CMD, GCS ↔ D, GCS ↔ D
by ( D21), ( D6), MM h i
AK EK
(D23) GCS believes D believes ID MISSION , IDD , IDGCS , ts3 , CMD, GCS ↔ D, GCS ↔ D
by ( D22), ( A8), NV, FR
(D24) GCS believes D believes IDD by ( D23), BC
(D25) GCS believes D believes CMD by ( D23), BC
AK
(D26) GCS believes D believes GCS ↔ D by ( D23), BC
EK
(D27) GCS believes D believes GCS ↔ D by ( D23), BC
From (I4):
SK
(D28) D sees h ID MISSION , IDGCS , IDD , ts4 , D ↔ MD, CMD i AK
h i
SK
(D29) D believes GCS said ID MISSION , IDGCS , IDD , ts4 , D ↔ MD, CMD
by ( D28), ( D12), MM h i
SK
(D30) D believes GCS believes ID MISSION , IDGCS , IDD , ts4 , D ↔ MD, CMD
by ( D29), ( A9), FR, NV
(D31) D believes GCS believes IDGCS by ( D30), BC
SK
(D32) D believes GCS believes D ↔ MD by ( D30), BC
SK
(D33) D believes D ↔ MD by ( D32), ( A9), JR
From the above analysis, it is shown that the SP-D2GCS protocol fulfills each of the
goals (G1~G16). Moreover, the following lemmas can be derived while showing that the
target security requirements are satisfied.

Lemma 1. The SP-D2GCS protocol provides a mutual authentication between D and GCS.
Sensors 2021, 21, 2057 14 of 25

Proof. Through the beliefs (D4) and (D17), both D and GCS can believe IDMISSION . Also,
they can believe ID of another from derived beliefs (D24) and (D31). Accordingly, this
proves that D and GCS mutually authenticate each other. 

Lemma 2. The SP-D2GCS protocol enables a secure exchange of AK and EK keys between D
and GCS.

Proof. As shown in the derivations (D5) and (D11), both GCS and D believe the session key
(gXY ) is a secret key shared between them and only known to them. There are direct beliefs
that AK and EK are securely exchanged between GCS and D, as shown in (D6) and (D7)
and (D12) and (D13). Also, indirect beliefs of GCS and D are shown in (D19) and (D20) and
(D26) and (D27). Accordingly, it can prove that D and GCS securely exchange AK and EK.


Lemma 3. The SP-D2GCS protocol enables a secure exchange of SK key between D and GCS.

Proof. The session key SK, which is used for communication between D and MD, is
generated by GCS. According to (D32) and (D33), D believes SK as a secret key between
itself and MD. Note that we cannot reason about the MD’s belief on SK because it is not
involved in this protocol. However, the above-obtained belief can be evolved to allow MD
to be sure of SK with the help of ST(D) during the SP-D2MD protocol. Therefore, we can
prove that SK is securely exchanged between D and MD. 

Lemma 4. The SP-D2GCS protocol has resistance against denial-of-service attacks.

Proof. (D3) shows that GCS authenticates message and its freshness prior to the expensive
computations, thus protecting the protocol from resource exhaustion attacks. 

Lemma 5. The SP-D2GCS protocol supports non-repudiation.

Proof. Every message of the SP-D2GCS protocol contains the public key encryption. Thus,
the message can prove who transferred messages with the public key. 

Lemma 6. The SP-D2GCS protocol supports confidentiality of CMD.

Proof. In the case of GCS, (D18) and (D25) can verify that D believes the operation
command CMD. Besides, D can verify that GCS sends the operation command CMD as it is
encrypted by EK (which is generated by the session key gXY that both D and GCS believe).
Thus, D and GCS support confidentiality for operational command CMD. 

Lemma 7. The SP-D2GCS protocol supports the integrity and data authentication of messages.

Proof. Concerning GCS, (D3) and (D23) show that D verifies (I1) and (I3), which illustrates
the integrity and data authentication of the message. In the case of D, (D10) and (D30) show
that the GCS confirms the trust of (I2) and (I4) (respectively) to support the integrity and
data authentication of the message. Accordingly, it can be shown that SP-D2GC supports
integrity and data authentication for messages. 

Lemma 8. The SP-D2GCS protocol prevents the man-in-the-middle attacks.

Proof. The ECDHE public keys exchanged between D and MD are protected by the digital
signatures that are also sent along with the keys. Also, it can be confirmed from (D5)
and (D11) that both parties can trust the ECDHE public key. Accordingly, the SP-D2GCS
protocol is secure against man-in-the-middle attacks. 
Sensors 2021, 21, 2057 15 of 25

Lemma 9. The SP-D2GCS protocol supports PFS and PBS.

Proof. Lemmas 2 and 8, above, show that gXY is securely set up between D and GCS. The
private keys X and Y are immediately removed from both parties so that gXY will not be
recovered in any case. Accordingly, it can be seen that the AK and EK derived from gXY
support PFS and PBS. 

Hence, it can be concluded from the proofs that the SP-D2GCS protocol fulfills the
security requirements outlined in Section 3, which enables it to withstand known attacks.

4.1.2. SP-D2MD
1. Idealization
The idealized forms of the SP-D2MD protocol are shown below:
SK
(I1) D → MD : h ID MISSION , ID MD , g x , ts1 , D ↔ MD iSK
AK EK SK
(I2) MD → D : h IDMISSION , IDMD , gy, ts2, D ↔ MD, D ↔ MDiAK , hgy, ts2, D ↔ MDiSK
AK EK
(I3) D → MD : h ID MISSION , IDD , ID MD , gy , ts3 , D ↔ MD, D ↔ MD i AK
2. Assumptions
The following are the assumptions considered while preparing the derivation process.
The assumptions (A1)~(A6) are related to MD and the rest are related to D.
SK
(A1) MD believes D ↔ MD
(A2) MD believes f resh(ts1 )
gY
(A3) MD believes → MD
SK
(A4) D believes D ↔ MD
(A5) D believes f resh(ts2 )
gX
(A6) D believes → D
(A7) MD believes f resh(ts3 )
3. Goals
The goals that are expected to be achieved by SP-D2MD are shown below:
SK
(G1) MD believes D believes D ↔ MD
AK
(G2) MD believes D ↔ MD
EK
(G3) MD believes D ↔ MD
SK
(G4) D believes MD believes D ↔ MD
AK
(G5) MD believes D ↔ MD
EK
(G6) MD believes D ↔ MD
(G7) D believes MD believes ID MISSION
(G8) D believes MD believes ID MD
AK
(G9) D believes MD believes D ↔ MD
EK
(G10) D believes MD believes D ↔ MD
(G11) MD believes D believes ID MISSION
(G12) MD believes D believes IDD
AK
(G13) MD believes D believes D ↔ MD
EK
(G14) MD believes D believes D ↔ MD
4. Derivations
The following derivations show the steps taken to realize the goals:
From (I1):
Sensors 2021, 21, 2057 16 of 25

h i
SK SK
(D1) MD sees ST ( D ), h M1 , D ↔ MD, D ⇔ MD i SK by ( I1)
(D2) MD sees ST ( D ) by ( D1), DR
h i
SK SK
(D3) MD believes GCS believes ID MISSION , ID MD , IDGCS , D ↔ MD, D ⇔ MD, LT
by ( D2), ( A1), MM, ( A2), FR, NV
SK
(D4) MD believes GCS believes D ↔ MD by ( D3), BC
SK
(D5) MD believes GCS believes D ⇔ MD by ( D3), BC
SK
(D6) MD believes D ↔ MD by ( D4), ( A3), JR
SK
(D7) MD believes D ⇔ MD by ( D5), ( A4), JR
SK SK
(D8) MD seesh M1 , D ↔ MD, D ⇔ MD i SK by ( D1), DR
h i
SK SK
(D9) MD believes D said M1 , D ↔ MD, D ⇔ MD by ( D8), ( D7), MM
h i
SK SK
(D10) MD believes D believes M1 , D ↔ MD, D ⇔ MD by ( D9), ( A5), FR, NV
SK
(D11) MD believes D believes D ↔ MDby ( D10), BC
SK
(D12) MD believes D believes D ⇔ MDby ( D10), BC
g XY
(D13) MD believes D ↔ MD by ( D9), BC, ( A6), DH
g XY
(D14) MD believes D ⇔ MD by ( D9), BC, ( A6), DH
From (I2):
g XY g XY
(D15) D sees h M2 , h M2 , D ↔ MD, D ⇔ MD i gXY iSK by ( I2)
 
g XY i g XY
(D16) D believes MD said h M2 , D ↔ MD, D ⇔ MDgXY by ( D15), ( A7), MM
 
g XY g XY
(D17) D believes MD believes h M2 , D ↔ MD, D ⇔ MD i gXY by ( D16), ( A8), FR, NV
g XY
(D18) D believes D ↔ MD by ( D16), BC, ( A9), DH
g XY
(D19) D believes D ⇔ MD by ( D16), BC, ( A9), DH
g XY g XY
(D20)( D20) D seesh M2 , D ↔ MD, D ⇔ MD i gXY by ( D16), BC
 
g XY g XY
(D21) D believes MD believes M2 , D ↔ MD, D ⇔ MD by ( D20), ( D19), MM,
( A8), FR, NV
g XY
(D22) D believes MD believes D ↔ MD by ( D21), BC
g XY
(D23) D believes MD believes D ⇔ MD by ( D21), BC
From (I3):
g XY g XY
(D24) MD sees h M3 , D ↔ MD, D ⇔ MD h gXY by ( I3)
 
g XY g XY
(D25) MD believes D believes M3 , D ↔ MD, D ⇔ MD by ( D24), ( D14), MM,
( A10), FR, NV
g XY
(D26) MD believes D believes D ↔ MD by ( D25), BC
g XY
(D27) MD believes D believes D ⇔ MD by ( D25), BC
From the above analysis, it is shown that the SP-D2MD protocol satisfied the goals
(G1~G14). Also, the following lemmas can be derived through the satisfied requirements.

Lemma 10. The SP-D2MD protocol provides mutual authentication between D and MD.
Sensors 2021, 21, 2057 17 of 25

Proof. The derivation result (D10) shows that the MD authenticates D. Similarly, D au-
thenticates MD, as shown in (D17). Hence, mutual authentication between D and MD is
realized in the SP-D2GC protocol. 

Lemma 11. The SP-D2MD protocol provides a secure key exchange of AK and EK.

Proof. As shown in the derivations (D13) and (D14) and (D18) and (D19), both MD and D
believe that the session key (gXY ) is a secret key shared between them and also believe that
it is a shared secret that is only known to them. Accordingly, there is a direct belief that
AK and EK are securely exchanged between GCS and D, as these keys are computed from
the session key gXY . Also, the indirect belief was secured by trusting beliefs in AK and EK
through (D22), (D23), (D26), and (D27). Thus, AK and EK are exchanged securely between
D and MD. 

Lemma 12. The SP-D2MD protocol prevents denial-of-service attacks.

Proof. In the case of MD, M1 shows freshness through (D10) and does not issue a message
without knowing SK, thus supporting defense against denial-of-service attacks. In the case
of D, M2 is protected by AK, which is derived from the master session key (gXY ). As a
result, the next message will not be processed by MD since the sender has no knowledge of
the master session key; thus, supporting denial-of-service attacks. 

Lemma 13. The SP-D2MD protocol supports confidentiality of AK and EK.

Proof. In the case of MD, (D13) and (D14) show the secure exchange of AK and EK, which
indicates the confidentiality of AK and EK. Similarly, D can be sure about the confidentiality
of AK and EK, as shown in (D18) and (D19). 

Lemma 14. The SP-D2MD protocol supports confidentiality of SK.

Proof. The proof for Lemma 3 of the SP-D2GCS protocol shows that SK is exchanged
between D (MD) and GCS securely. The proof of Lemma 8 shows the confidentiality of SK
between D and GCS. Similarly, it can be shown that the SP-D2MD protocol supports the
confidentiality of SK, as indicated in the derivations (D6) and (D7). 

Lemma 15. The SP-D2MD protocol supports integrity and data authentication of messages.

Proof. The derivations (D10) and (D25) show that D supports the integrity and data
authentication of the message by verifying the trust of M1 and M3. MD also verifies the
trust of M2, through the derivation (D17), to support the integrity and data authentication
of the message. Hence, we can verify that D and MD support the integrity and data
authentication of the message. 

Lemma 16. The SP-D2MD protocol provides defense against man-in-the-middle attacks.

Proof. The ECDHE public keys exchanged between D and MD are protected by the digital
signatures that are also sent along with the keys. Also, it can be confirmed from (D10)
and (D17) that both parties can trust the ECDHE public key. Accordingly, the SP-D2MD
protocol is secure against man-in-the-middle-attack. 

Lemma 17. The SP-D2MD protocol supports PFS and PBS.

Proof. As per Lemma 11 and Lemma 12 of the SP-D2MD protocol, the master session
key gXY is securely set up through the Diffie–Hellman key exchange between M and MD.
The private keys X and Y are immediately removed from both parties so that gXY is not
Sensors 2021, 21, 2057 18 of 25

recovered under any circumstances. Hence, the authentication and encryption keys derived
from gXY support PFS and PBS. 

From the above proofs, we can conclude that SP-D2MD, like SP-D2GCS, is proven to
satisfy mutual authentication, secure key exchange, integrity and data authentication of
messages, and supports PFS, which makes it secured against known attacks.

4.2. Formal Verification with Scyther

Although the formal verification carried out by BAN-Logic validates the proposed
protocol, highlighting that it meets the security goals and is secure against known attacks,
BAN-Logic has found to have a limitation in pointing out some flaws [34]. Hence, for a
complete formal analysis of security protocols, it is often necessary to combine BAN-Logic
with automated tools such as Scyther and AVISPA (Automated Validation of Internet
Security Protocols and Applications) [35]. In this paper, the automated formal verification
tool Scyther is used to formally verify the SP-D2GC and SP-D2MD protocols.
Scyther, developed by Cremers in 2007, provides a graphical user interface that
integrates the Command Line tool and the python scripting interface as an automated
tool for formal validation. It provides validation, presentation, analysis, specification, and
derivation of protocols. In particular, by providing protocol behavior classes, Scyther points
out security problems through straightforward formalization and verification of protocols.
The Security Protocol Description Language (SPDL) used in Scyther has a similar syntax
to C/JAVA language (although case-insensitive), and defines roles as a series of events,
consisting of events representing transmission and reception of information.
For protocol verification, Scyther can be used in three ways. Verification claim: ver-
ified or falsified security attributes, automatic claims: Scyther automatically generates
and confirms a claim when security attributes are not specified as a claim event, and
characterization: Scyther analyzes protocols and provides a finite representation of all
traces, including the execution of protocol roles, so that each protocol role can be character-
ized. During the protocol verification process, Scyther creates an attack graph for unsafe
protocols, and displays an individual attack graph for each claim. Claim events used for
verification in this paper can be categorized by the functions shown in Table 4, and the
details are described in Reference [26].

Table 4. Claim event description.

Notations Meanings
Event Security Attribute
Alive, Nisynch, Niagree, Weakagree, Commit Authentication
Secret Secrecy

At first, each role is modeled in SPDL scripts. The basic roles include the D’s role,
the GCS’s role, and the MD’s role, as shown in Figure 6a–c, respectively. In addition, we
included the claim events to each modeling, such as Alive, Nisynch, Niagree, Weakagree,
Commit/Running, and Secret. Each roles are communicated with each other through the
channel set through ‘send’ and ‘recv’. These events check whether modeling can provide
authentication and secrecy. If the proposed protocol is secure, the status of the result will
show that every claim is OK. Otherwise, the result will show the process of leading to a
vulnerable modeling state.
Scyther composes a communication environment based on SPDL scripts, as shown
in Figure 6, and executes verification according to claim events. As shown in Figure 7, D,
GCS, and MD of the proposed protocol have not been attacked against claim events such
as Alive, Nisynch, Niagree, Weakagree, Commit/Running, and Secret. Consequently, the
proposed protocol is proven to be secure against known attacks.
Sensors 2021, 21, 2057 19 of 25

Figure 6. SPDL script of proposed protocol; (a) D’s SPDL script; (b) GCS’s SPDL script; (c) MD’s SPDL script.
Sensors 2021, 21, 2057 20 of 25

Figure 7. A Scyther verification result.

Sensors 2021, 21, 2057 21 of 25

5. Performance Analysis
In this section, the proposed protocol is compared with four state-of-the-art security
protocols [18,23,27,36], that can be deployed to protect the communication within the UAV
network. The comparison is made in terms of security and computation overhead, whose
results are provided in Tables 5 and 6, respectively.

Table 5. The state-of-the-art comparison with existing protocols.

Security Requirements [18] [23] [27] [36] Our Protocol

Confidentiality X X X X X
Integrity X X X X X
Mutual Authentication X X X X X
Non-repudiation X X X X X
Perfect Forward Secrecy X X X X X
Perfect Backward Secrecy X X X X X
Response to DoS Attacks X X X X X
Man-in-the-middle response X X X X X
D2D security support X X X X X
X: Supported, X: Unsupported.

Table 6. Computational overhead comparison.

Security Protocols Computational Overhead

SP-D2GCS SP-D2MD
Our Protocol
7CSC + 4CS + 4CSV + 2CDH + 11CHM + 2CC CSC + 2CDH + 8CHM
[18] 5CWBC + 2CS + 2CSV
Initial Step Authentication Step
[23] —– 2CSC + 3CXoR + 3CH
[27] Cbio + 8CXoR + 12CH Cbio + 12CXoR + 32CH
[36] 2CPC + 2CS + 2CSV
Cbio : Biometric Authentication, CSC : Symmetric Key Cryptography, CPC : Public Key Cryptography, CDH : Diffie–
Hellman Key Exchange, CS : Digital Signature, Csv : Digital Signature Verification, CWBC : White Box Encryption,
CXoR : XOR Operation, CHM : HMAC operation, CH : Hash Operation, CCV : Digital Certificate Verification.

Table 5 provides the comparative analysis among protocols based on the security
properties. It can see that the work in References [23,27] does not support non-repudiation
property. Also, References [18,27] do not provide PFS. Therefore, if any long-term key
used to derive past session keys has been exposed, adversaries can use the session keys to
recover the encrypted messages to acquire sensitive data. Likewise, References [18,27] do
not support PBS, thus causing the subsequent sessions to be vulnerable to various attacks,
in case of compromise of any of the current long-term keys. Moreover, proposed protocols
of References [23,36] are susceptible to DoS attacks due to resource exhaustion. Even worse,
they perform high computational operation in order to support PFS and PBS, which puts a
heavy burden on key updates during flight. In addition, protocols in References [18,23,36]
do not support security between UAVs. As a result, it can be concluded that the designed
security protocol offers better security compared to the other state-of-the-art protocols.
On the other hand, Table 6 compares the proposed protocol with the 4 protocols based
on computation overhead. Similar to References [18,27], the proposed protocol cannot
avoid excessive computational overhead in SP-D2GCS to support PFS and PBS. It is worth
to note that such overhead is negligible because SP-D2GCS is executed only once. However,
based on the strong session key, SK, derived from SP-D2GCS, SP-D2MD, which is primary
executed in the proposed protocols, achieves relatively lightweight computation while
meeting the security requirements.

6. Simulation Results
We developed the proposed security protocols using Python and tested it on an ad-
hoc network that composed two real UAVs and a ground control station. The network
Sensors 2021, 21, 2057 22 of 25

architecture in the experimental simulation along with the actual experimental test bed for
the proposed protocol are shown in Figures 8 and 9, respectively. The instruments used
in this experiment are also listed in Table 7. The UAVs are equipped with a companion
board Raspberry-Pi that is serially interfaced with the Pixhawk flight controller. The
companion board enables developers to develop a self-operating UAV according to their
target application. In the experiments, we create a straightforward application where
UAVs and GCS simply exchange operational data or commands with each other at a pre-
defined interval. Meanwhile, before the execution of said application, the proposed security
protocols were first accomplished. During the execution of the protocols, essential metrics,
such as size and transmission latency of the messages, were collected. The transmission
latency refers to the amount of time for a message to travel across the network.

Figure 8. An illustration of UAV ad-hoc network architecture implemented in the experimental simulation.

Figure 9. The actual experimental testbed for the proposed security protocol.

Table 7. Implementation environment.

Environment Description
UAV Two UAVs each with Raspberry Pi model B+
GCS Ubuntu 18.04.3 LTS, 11GB RAM, and i5-2400 CPU @3.10 GHz
Language Python 3.8
Sensors 2021, 21, 2057 23 of 25

Table 8 shows the collected values of the target metrics. Based on this, the proposed
D2GCS and D2MD security protocols have a total message size of 2411 and 781 bytes,
respectively. Furthermore, the average transmission latency of each message corresponds
to the number of bytes it carries. Based on our experiment, it takes approximately 213 mil-
liseconds to establish a secure channel between UAV and GCS. Meanwhile, the execution
of the D2MD security protocol takes an average of 29 milliseconds. The performance of
UAVs can be significantly influenced by its power consumption and transmission latency,
which can be associated to the message size of a particular key exchange protocol. With
regards to the former, the size of the transmitted or received messages play an important
role in extending energy lifetime of UAVs, especially when the key exchange protocol is
executed during its flight. On the other hand, the latter, which is still dependent on the size
of the messages, has an impact on the amount of time it takes for two parties to establish
the secure channel. In relation to these factors, the relatively low message size and latency
obtained from our experiment indicate that the proposed protocol has a great potential in
terms of the practical aspects related to UAV network security.

Table 8. Notations and their meaning.

SP-D2GCS SP-D2MD
Messages
Message Size Message Size
Latency (ms*) Latency (ms*)
(bytes) (bytes)
M1 939 71.11001 393 18.74995
M2 1036 93.67990 257 10.45012
M3 218 23.38982 131 9.96995
M4 218 25.03991 - -
Total 2411 213.2196 781 29.20008
* ms: millisecond.

7. Conclusions
Although UAVs play an essential role in a wide range of application areas, there
are still security issues that limit their full potential in delivering the required solution.
Especially in the case of military scenarios, the security and privacy of UAVs should be
among the highest priority. In order to resolve the security concerns, we proposed a
security protocol (with two sub-protocols, SP-D2GCS and SP-D2MD) that enables secure
communication among UAVs and between the UAV and the GCS.
Our protocol can be applied in four different deployment scenarios. Scenario one
consists of multiple military UAVs with inbuilt sensors that transmit traffic to each other,
in which only the monitoring drone is able to communicate with GCS directly. In this
case, the SP-D2GCS protocol assists the communication between the drone and GCS, while
SP-D2MD is used between the drone and monitoring drone. In case 2, apart from the com-
munication between the drones and monitoring drones, the ordinary drones themselves
communicate with each other. However, similar to case 1, it is only the monitoring drone
that communicates with the GCS. The third case involves direct communication between
the drones and the GCS without a monitoring node sitting between them. In such case, the
SP-D2GCS protocol can be used to secure the channel. The final arrangement is similar to
case two, except all intercommunicating drones also communicate with the GCS directly,
which uses both of the proposed sub-protocols.
Our protocol is also evaluated to prove that it meets all the security requirements
described in the proposed protocol section. The proof is conducted by using two formal
verification methods, BAN-Logic and Scyther. Furthermore, both sub-protocols are imple-
mented on a real UAV (powered by Raspberry Pi) and a Linux-based ground control station
and compared to other similar protocols against security and performance. The authors
would like to further consider the privacy issues in UAV communication and design an
adaptive security solution as their future work.
Sensors 2021, 21, 2057 24 of 25

Author Contributions: Conceptualization, Y.K., J.K., and I.Y.; methodology, Y.K., J.K., G.P., and
I.Y.; validation, Y.K., J.K., and D.G.D.; formal analysis, Y.K., J.K., and D.G.D.; investigation, P.V.A.
and J.K.; data curation, P.V.A. and J.K.; writing—original draft preparation, Y.K., J.K., and D.G.D.;
writing—review and editing, I.Y., and G.P.; visualization, D.G.D.; supervision, I.Y.; project adminis-
tration, I.Y.; funding acquisition, I.Y. All authors have read and agreed to the published version of
the manuscript.
Funding: This research was supported by Basic Science Research Program through the National
Research Foundation of Korea (NRF), funded by the Ministry of Education (NRF-2020R1I1A2073603),
as well as the Soonchunhyang University Research Fund.
Institutional Review Board Statement: Not applicable.
Informed Consent Statement: Not applicable.
Data Availability Statement: Not applicable.
Conflicts of Interest: The authors declare no conflict of interest.

References
1. Vergouw, B.; Nagel, H.; Bondt, G.; Custers, B. Drone technology: Types, payloads, applications, frequency spectrum issues and
future developments. In The Future of Drone Use; TMC Asser Press: The Hague, The Netherlands, 2016; pp. 21–45.
2. Naqvi, S.A.; Hassan, S.A.; Pervaiz, H.; Ni, Q. Drone-aided communication as a key enabler for 5G and resilient public safety
networks. IEEE Commun. Mag. 2018, 56, 36–42. [CrossRef]
3. Livingston, S.J.; Chandan, P.H.; Simeon, R.S.; Vikas, B. D-ARCH: A Detailed Analysis of Drone Challenges Policy Enforcements
and Security Solutions. J. Comput. Theor. Nanosci. 2018, 15, 2842–2847. [CrossRef]
4. Ismail, M.A.; Bierig, A. Identifying drone-related security risks by a laser vibrometer-based payload identification system.
In Proceedings of the Laser Radar Technology and Applications XXIII, Orlando, FL, USA, 10 May 2018; Volume 10636, p. 1063603,
International Society for Optics and Photonics.
5. Bunse, C.; Plotz, S. Security analysis of drone communication protocols. In Proceedings of the International Symposium on
Engineering Secure Software and Systems, Paris, France, 26–27 June 2018; Springer: Cham, Switzerland, 2018; pp. 96–107.
6. Choudhary, G.; Sharma, V.; You, I. Sustainable and secure trajectories for the military Internet of Drones (IoD) through an efficient
Medium Access Control (MAC) protocol. Comput. Electr. Eng. 2019, 74, 59–73. [CrossRef]
7. He, D.; Chan, S.; Guizani, M. Communication security of unmanned aerial vehicles. IEEE Wirel. Commun. 2016, 24, 134–139.
[CrossRef]
8. Wang, J.; Jin, C.; Tang, Q.; Xiong, N.; Srivastava, G. Intelligent Ubiquitous Network Accessibility for Wireless-Powered MEC in
UAV-Assisted B5G. IEEE Trans. Netw. Sci. Eng. 2020. [CrossRef]
9. Tang, Q.; Chang, L.; Yang, K.; Wang, K.; Wang, J.; Sharma, P.K. Task number maximization offloading strategy seamlessly adapted
to UAV scenario. Comput. Commun. 2020, 151, 19–30. [CrossRef]
10. Lin, N.; Tang, J.; Li, X.; Zhao, L. A novel improved bat algorithm in UAV path planning. Comput. Mater. Contin. 2019, 61, 323–344.
[CrossRef]
11. Chen, P.Y.; Chen, G.Y. The Design of a TLD and Fuzzy-PID Controller based on the Autonomous Tracking System for Quadrotor
Drones. Intell. Autom. Soft Comput. 2020, 26, 489–500. [CrossRef]
12. Qayyum, A.; Ahmad, I.; Iftikhar, M.; Mazher, M. Object Detection and Fuzzy-Based Classification Using UAV Data. Intell. Autom.
Soft Comput. 2020, 26, 693–702. [CrossRef]
13. Zhang, L.; Bai, L.; Zhang, X.; Zhang, Y.; Yang, L.; Yan, X. Cultivated land monitoring system based on dynamic wake-up UAV
and wireless of distributed storage. Comput. Mater. Contin. 2019, 61, 817–828. [CrossRef]
14. Villalonga, A.; Beruvides, G.; Castaño, F.; Haber, R.E. Cloud-based industrial cyber–physical system for data-driven reasoning:
A review and use case on an industry 4.0 pilot line. IEEE Trans. Ind. Inform. 2020, 16, 5975–5984. [CrossRef]
15. Beruvides, G.; Juanes, C.; Castaño, F.; Haber, R.E. A self-learning strategy for artificial cognitive control systems. In Proceedings
of the 2015 IEEE 13th International Conference on Industrial Informatics (INDIN), Cambridge, UK, 22–24 July 2015; IEEE:
Piscataway, NJ, USA, 2015; pp. 1180–1185.
16. Choudhary, G.; Sharma, V.; You, I.; Yim, K.; Chen, I.R.; Cho, J.H. Intrusion Detection Systems for Networked Unmanned Aerial
Vehicles: A Survey. In Proceedings of the 2018 14th International Wireless Communications & Mobile Computing Conference
(IWCMC), Limassol, Cyprus, 25–29 June 2018; IEEE: Piscataway, NJ, USA, 2018; pp. 560–565.
17. Sharma, V.; Choudhary, G.; Ko, Y.; You, I. Behavior and vulnerability assessment of drones-enabled industrial internet of things
(iiot). IEEE Access. 2018, 6, 43368–43383. [CrossRef]
18. Seo, S.H.; Won, J.; Bertino, E.; Kang, Y.; Choi, D. A security framework for a drone delivery service. In Proceedings of the
2nd Workshop on Micro Aerial Vehicle Networks, Systems, and Applications for Civilian Use, Singapore, 26 June 2016; ACM:
New York, NY, USA, 2016; pp. 29–34.
Sensors 2021, 21, 2057 25 of 25

19. Kriz, V.; Gabrlik, P. Uranuslink-communication protocol for UAV with small overhead and encryption ability. IFAC-Pap. OnLine
2015, 48, 474–479. [CrossRef]
20. Won, J.; Seo, S.H.; Bertino, E. A secure communication protocol for drones and smart objects. In Proceedings of the 10th ACM
Symposium on Information, Computer and Communications Security, Singapore, 14–17 April 2015; ACM: New York, NY, USA,
2015; pp. 249–260.
21. Islam, N.; Hossain, M.K.; Ali, G.M.; Chong, P.H. An expedite group key establishment protocol for Flying Ad-Hoc Network
(FANET). In Proceedings of the 2016 5th International Conference on Informatics, Electronics and Vision (ICIEV), Dhaka,
Bangladesh, 13–14 May 2016; IEEE: Piscataway, NJ, USA, 2016; pp. 312–315.
22. Maxa, J.A.; Mahmoud, M.S.; Larrieu, N. Extended verification of secure UAANET routing protocol. In Proceedings of the 2016
IEEE/AIAA 35th Digital Avionics Systems Conference (DASC), Sacramento, CA, USA, 25–29 September 2016; IEEE: Piscatvey,
NJ, USA, 2016; pp. 1–16.
23. Blazy, O.; bonnefoi, P.-F.; Conchon, E.; Sauveron, D.; Akram, R.N.; Markantonakis, K.; Mayes, K.; Chaumette, S. An Efficient
Protocol for UAS Security. 2017 Integrated Communications, Navigation and Surveillance Conference (ICNS), Herndon, VA, USA, 18–20
April 2017; IEEE: Piscataway, NJ, USA, 2017; pp. 1–21.
24. Wang, G.; Lim, K.; Lee, B.S.; Ahn, J.Y. Handover Key Management in an LTE-based Unmanned Aerial Vehicle Control Network.
In Proceedings of the 2017 5th International Conference on Future Internet of Things and Cloud Workshops (FiCloudW), Prague,
Czech Republic, 21–23 August 2017; IEEE: Piscataway, NJ, USA, 2017; pp. 200–205.
25. Semal, B.; Markantonakis, K.; Akram, R.N. A Certificateless Group Authenticated Key Agreement Protocol for Secure Communi-
cation in Untrusted UAV Networks. In Proceedings of the 2018 IEEE/AIAA 37th Digital Avionics Systems Conference (DASC),
London, UK, 23–27 September 2018; IEEE: Piscataway, NJ, USA, 2018; pp. 1–8.
26. Kim, S.; Youn, T.; Choi, D.; Park, K. UAV-Undertaker: Securely Verifiable Remote Erasure Scheme with a Countdown-Concept for
UAV via Randomized Data Synchronization. Wirel. Commun. Mob. Comput. 2019, 2019, 1–11. [CrossRef]
27. Wazid, M.; Das, A.K.; Kumar, N.; Vasilakos, A.V.; Rodrigues, J.J. Design and analysis of secure lightweight remote user
authentication and key agreement scheme in Internet of drones deployment. IEEE Int. Things J. 2018, 6, 3572–3584. [CrossRef]
28. Hartmann, K.; Giles, K. UAV exploitation: A new domain for cyber power. In Proceedings of the 2016 8th International Conference
on Cyber Conflict (CyCon), Tallinn, Estonia, 31 May–3 June 2016; IEEE: Piscataway, NJ, USA, 2016; pp. 205–221.
29. Medhi, D.; Huang, D. Secure and resilient routing: Building blocks for resilient network architectures. In Information Assurance;
Elsevier Inc.: Amsterdam, The Netherlands, 2008; pp. 417–448.
30. Dolev, D.; Yao, A. On the security of public key protocols. IEEE Trans. Inf. Theory 1983, 29, 198–208. [CrossRef]
31. Koubaa, A.; Allouch, A.; Alajlan, M.; Javed, Y.; Belghith, A.; Khalgui, M. Micro air vehicle link (mavlink) in a nutshell: A survey.
IEEE Access. 2019, 7, 87658–87680. [CrossRef]
32. Burrows, M.; Abadi, M.; Needham, R.M. A logic of authentication. Proceedings of the Royal Society A—Mathematical, Physical
and Engineering Sciences. 1989. Available online: https://royalsocietypublishing.org/doi/abs/10.1098/rspa.1989.0125 (accessed
on 11 May 2020).
33. Cremers, C.J. The Scyther Tool: Verification, falsification, and analysis of security protocols. In Proceedings of the International
Conference on Computer Aided Verification, Princeton, NJ, USA, 7–14 July 2008; Springer: Berlin/Heidelberg, Germany, 2008;
pp. 414–418.
34. Boyd, C.; Mao, W. On a limitation of BAN logic. In Proceedings of the Workshop on the Theory and Application of of
Cryptographic Techniques, Lofthus, Norway, 23–27 May 1993; Springer: Berlin/Heidelberg, Germany, 1993; pp. 240–247.
35. Armando, A.; Basin, D.; Boichut, Y.; Chevalier, Y.; Compagna, L.; Cuéllar, J.; Mödersheim, S. The AVISPA tool for the automated
validation of internet security protocols and applications. In Proceedings of the International conference on computer aided
verification, Scotland, UK, 6–10 July 2005; Springer: Berlin/Heidelberg, Germany, 2005; pp. 281–285.
36. Galois, Inc. Galois Embedded Crypto: Light Weight Cryptography. Available online: https://github.com/GaloisInc/gec/blob/
master/README.md (accessed on 20 April 2015).