5.1. Formal Verification with AVISPA
A formal security verification was performed on LAKD protocol using the SPAN+AVISPA tool. The AVISPA tool is an automated verification tool for cryptographic protocols. It supports four back-ends that search for attacks on the security properties of the protocol under verification. They are On-the-fly Model-Checker (OFMC), Constraint-Logic-based Attack Searcher (CL-AtSe), SAT-based Model-Checker (SATMC), and Tree Automata based on Automatic Approximations for the Analysis of Security Protocols (TA4SP) [
46]. For the verification, the protocol has to be described using the High-Level Protocol Specification Language (HLPSL). It is a role-based language, where each role describes the information a principal can use initially, such as preshared keys and cryptographic algorithms, the initial state, requirements for state transitions, and specifications concerning how the roles interact with one another [
47]. The SPAN tool is a protocol animator for HLPSL specifications which allows interactively building message sequence charts of the protocol and attacks that are found [
48].
The AVISPA tool implements a communication channel controlled by a Dolev–Yao intruder, which means that the adversary can intercept, decompose, reassemble or modify the transmitted messages; however, because perfect cryptography is assumed, the adversary can analyze intercepted messages only if he/she possesses the decryption keys [
49,
50]. Three verifications are performed by the AVISPA tool. The first verification is the executability of a non-trivial HLPSL specification, which ensures that the protocol executes to completion; thus, it can reach a state where possible attacks can be found. The second is the verification of replay attacks, where the back-ends give the intruder the knowledge of regular sessions between legitimate agents, verify if legitimate participants can execute the protocol by searching for a passive intruder, and determine whether a replay attack exists. The third verification is Dolev–Yao checking, where back-ends verify if a MITM attack is possible. After the verifications, the AVISPA tool outputs whether the protocol is concluded safely or unsafely against MITM and replay attacks, or if the analysis is inconclusive [
51].
The security goals specified in the HLPSL modeling of LAKD protocol were mutual authentication and secrecy of the session key . The first involves that an agent is correct in believing the aimed principal is in the current session, has reached a particular state, and agrees on some value that cannot be used twice with the same participants. If the mutual authentication goal is violated or the intruder learns a secret value, the tool concludes the protocol as unsafe, indicates which goal was unsatisfied, and provides an attack trace which shows the sequence of messages resulting in an attack.
In the verification of LAKD, CL-AtSe and OFMC back-ends were used because of their support of the xor operation [
52]. In
Figure 3 the verification results are shown; as can be seen, both back-ends concluded that LAKD protocol is safe against replay and MITM attacks, and the secrecy and mutual authentication goals were achieved.
5.2. Formal Verification with BAN Logic
BAN logic is a formal logic for analyzing the security properties of a protocol. It consists of a set of rules and postulates to reason about what principals believe about whom. BAN logic allows verifying whether the exchanged information on an authentication protocol is trustworthy [
27]. Its notations and inference rules are introduced in
Table 2 and
Table 3, respectively.
The security goals LAKD protocol has to satisfy to achieve mutual authentication are the following. represents the gateway, and the sensor node.
Goal 1: .
Goal 2: .
Goal 3: .
Goal 4: .
The idealized form of LAKD protocol is as follows:
Message 1: .
Message 2: .
Message 3: .
Message 4: .
The assumptions about the LAKD protocol initial state are the following:
Assumption 1. .
Assumption 2. .
Assumption 3. .
Assumption 4. .
Assumption 5. .
Assumption 6. .
Assumption 7. .
Assumption 8. .
Assumption 9. .
Assumption 10. .
The BAN logic proof demonstrating that LAKD protocol achieves the mutual authentication goals is presented in
Appendix A. It consists of applying the BAN logic rules to the idealized form of the protocol and initial assumptions.
5.3. Informal Security Analysis
In this section, we provide an analysis of the security properties achieved by LAKD protocol and its resistance against known attacks.
5.3.1. Confidentiality
All information which has to be kept confidential between a gateway and sensor node is sent ciphered through an xor, or masked using random numbers and a one-way hash function. To send with confidentiality, it is ciphered through an xor with . The value is a secret between sensor node and gateway; therefore, the adversary cannot compute to obtain ; additionally, it cannot invert the hash function to obtain . The use of and causes the hash value to be different in each protocol execution, preventing the adversary to reuse old values of seized by him/her. In a similar manner, is sent ciphered with , and with . The values and become session secrets. They are used to mask long-term secrets, such as , , and , make messages dependent to the current session, make messages different and unpredictable between sessions, and construct the session key . Together with the hash function, they prevent the adversary from discerning secrets from the transmitted messages.
5.3.2. Data Integrity
The following scenarios describe what would happen if a message were to be modified during transmission. In all of them, the receptor can detect a data integrity violation. Consequently, it aborts the communication.
If , , or is modified, the verification of digest value will not be true due to it is created with , , which the gateway derive from , and which is selected according to the value of . Even if only one of , , or is altered, it will cause to be different from that originally sent, resulting in verification being false. Also, it is infeasible the adversary be able to fabricate a valid to hide its modifications, because its construction uses , which is a secret between sensor node and the gateway.
If , , or is modified, the verification of digest value will not be true because it is created with and , which the gateway tries to derive from and , respectively. Concerning , it is used in ; thus, its alteration also affects . Even if only one of , , or is modified, it will result in different values of and from the sent by the gateway, causing the verification of to be false. Also, it is infeasible the adversary be able to fabricate a valid , because it uses .
If or is modified, the verification of digest value will be false, because it is constructed with . It also uses , which is the key from selected by gateway through in . It is infeasible the adversary be able to fabricate a valid , because he/she does not know the secret keys.
If or is modified, a similar situation to that previously described will happen, due to depends on and .
5.3.3. Mutual Authentication
In the registration phase of LAKD protocol, the gateway and sensor node construct and exchange in a secure manner, the values , , and . The knowledge of , , and demonstrates to the gateway that an agent is the sensor node, and vice versa. Gateway authenticates the sensor node by verifying that was constructed using and , and with and . The sensor node authenticates the gateway by confirming was created with and , and with and . Therefore, both principals authenticate each other.
5.3.4. Sensor Node Anonymity
After each authentication session, the sensor node pseudonym is updated, and because random numbers are used in its modification, its new value is unpredictable. Therefore, an adversary can neither know the specific node behind some action nor keep a record of the activities performed by the same node.
5.3.5. Perfect Forward and Backward Secrecy
If the adversary obtains the current session key , he/she cannot derive older or futures from it, because there is no relationship between them, since each key is constructed with values specific to the session it belongs. is constructed using ephemeral random values sent during the current session, the current of the sensor node, and the key selected in the current session. Even if the adversary obtains long-term keys, he/she will not be able to generate older because of the ephemeral random numbers. Therefore, a sensor node can only access information which was transmitted when it was part of the network, neither the previous nor the future one.
5.3.6. Known Session Key Security
Each execution of a key agreement protocol should provide a unique session key. As a result, if the adversary learns some, he/she is not able to generate others [
53]. In the proposed protocol,
is constructed using two random numbers (
and
), which are ephemeral and different per session. The
of the sensor node is also used, which changes after each authentication session, and for its modification uses the secret
unknown to the adversary. Therefore, the adversary is not able to create
even if he/she learned some old ones due to the unpredictable changes.
5.3.7. Resistance to the Tracking Attack
In this attack, an adversary intercepts messages of different sessions and tries to find a relationship between them to determine if they belong to the same sensor node [
54,
55]. In LAKD protocol, the principals never use their identities. To authenticate, they use the secrets
and
, which are the hash outputs of their identities, keys, and random numbers. Thus, the adversary cannot invert them to know the specific node behind a message. Also, every message is constructed using random numbers. Because they are different per session, messages between sessions are different and unpredictable. Finally, in each session, a different
is selected, which contributes to the unpredictability among sessions. Consequently, an adversary cannot track a node from captured messages.
5.3.8. Resistance to the Offline Identity Guessing Attack
In this attack, the adversary tries to guess the sensor node or the gateway identity off-line. In the proposed protocol, only the values and contain the identities of the sensor node and the gateway, respectively. The values are not invertible because they are the result of a hash function. Also, they are never sent in cleartext, when used they are masked with timestamps and unknown random numbers to the adversary, and then input to a hash function. As a result, it is infeasible to obtain the identities or even or from the messages.
5.3.9. Resistance to Impersonation Attack
Every message sent in LAKD protocol uses at least one secret: , , or . They belong to sensor node . It is not feasible that an adversary fabricates valid messages to impersonate sensor node , or to impersonate the gateway, due to the secrecy of , , and , and because of the value changes unpredictably in each authentication session. Additionally, in every protocol execution, a different is selected from the key pool. This makes the impersonation even less possible, because the adversary is also required to know all the keys of .
5.3.10. Resistance to the Injection Attack
In this attack, an adversary fabricates and sends counterfeit messages to legitimate nodes. The proposal resists this attack like how it does to impersonation attack. Every transmitted message uses at least one shared secret between sensor node and gateway. It is infeasible than an adversary fabricates valid messages without knowing them. Additionally, every message contains a digest of the data in it. Therefore, the sensor node and gateway can easily detect counterfeit, replayed, or modified messages. The digest consists of the timestamp, random numbers, and shared secrets input to a hash function. The adversary cannot invert the function to fabricate a valid digest, also cannot modify the hash output in a deterministic manner to make it valid to his/her counterfeit data.
5.3.11. Resistance to the MITM Attack
In this attack, an adversary deceives agents into thinking their communication is secure, while he/she is in the middle of maliciously modifying and relaying messages. In the LAKD protocol, it is not feasible that the adversary modifies or fabricates messages without the sensor node and gateway detecting it, as described in subsections Data Integrity and Resistance to the Injection Attack. Also, it is not feasible he/she obtains secret values, such as identities, keys, , , or from the messages sent, because they are masked with random numbers, timestamps, and hash functions. Finally, the adversary is not able to obtain , because it is constructed using secret random numbers and the selected in the current protocol execution.
5.3.12. Resistance to the Privileged Insider Attack
In this attack, a privileged insider (e.g., a system manager with access to the gateway) tries to impersonate a node when accessing other servers where that node is registered, using the node’s credentials of its system [
56]. In the proposal, the gateway does not know the
and
of the sensor node, and the sensor node does not know the
and
of the gateway. During the registration phase, the principals share those values masked with random numbers and hash functions. Therefore, none of them can invert the operations and obtain the original values to use them to impersonate the node in other systems.
5.3.13. Resistance to the Replay Attack
To perform this attack, the adversary intercepts valid messages and maliciously delays or repeats them, faking ownership over them. LAKD protocol resists this attack in two ways. The first one is using timestamps for the verification of the transmission delay. Messages from an old session will have a transmission delay longer than the allowed. This will be detected by the gateway in , and by the sensor node in . Therefore, the receptor will not accept the messages, and it will abort the communication. The second form of resistance against this attack is using the ephemeral random numbers and , and a different key per session. If the adversary replays old messages from the gateway, sensor node will detect in that is not the one it sent in . Similarly, if the replayed messages are from the sensor node, the gateway will detect in that is not the one it sent in , and is not the one it selected. Therefore, LAKD protocol is resistant to replay attacks.
5.3.14. Resistance to the Known Session-Specific Temporary Information Attack
In this attack, the session key secrecy is compromised of the exposition of session-temporal secrets, such as random numbers. The adversary can perform the attack because random numbers are not usually stored in protected memory, as is done with keys and other long-term secrets. If after the session execution, the random numbers are not correctly deleted from memory, or the adversary controls the random number generator, he/she can obtain them and use them to generate the session key [
53,
57]. LAKD protocol is resistant to this attack, due to
being constructed using the secret key
. Even if the adversary obtains the random numbers
and
, he/she will not be able to generate
because he/she does not have access to the key pool.
5.3.15. Resistance to the DoS Attack
LAKD protocol can detect intent to perform a DoS attack from the first transmitted message. If is a replay message, the gateway will detect that the cleartext is not within the allowed transmission-delay. If was modified to make it look as valid, then the verification of the digest will be false. The adversary cannot construct a valid because he/she does not know . If is not a replay but a fresh and valid message originated by the adversary, the gateway will detect the malicious behavior when receiving many messages with the same . If the adversary modifies the cleartext to pretend that the message is from a different source, then the verification of will be false, because the adversary does not know the of that node.
5.3.16. Resistance to the Desynchronization Attack
In this attack, the adversary tries to impede the communication between two legitimate nodes through de-synchronize them in the values required for the authentication [
58]. In LAKD protocol, the only value that is updated after an authentication session is the pseudonym
. In its modification
,
,
, and the current
are used. Before updating, the principals verify the identities of each other, and the correctness of the random numbers. The gateway confirms in
that the sensor node is the real
, because that message proves that the sensor node knows
,
, and
. It also confirms that the sensor node has the correct
and
. Similarly, the sensor node confirms in
the identity of the gateway and the accuracy of the random numbers. As can be seen, the principals prove their identities and validate the data trustworthiness before using it to update
, preventing this type of attack.
5.3.17. Resistance to Key Disclosure Attack
Resistance to long-term key disclosure attack: The long-term key of the sensor node , of the gateway , and the shared key between them , are never sent in cleartext, ciphered with an xor, or transformed in another invertible way. Keys and are only used to construct and , after hashing them with random numbers. Similarly, , , and are sent in the public channel only after hashing them with the secret random numbers and . Therefore, because it is infeasible to invert the hash output, the adversary cannot obtain or construct , , and .
Resistance to the Session-Key Disclosure Attack: The session key is never sent in a message. It is constructed by the principals using , , and , which are unknown to the adversary. The random numbers and are sent in the public channel using the hashed and to cipher them. Thus, the adversary cannot obtain them. Additionally, the key is sent only after hashing it with , , timestamps, , and . Therefore, the adversary can neither obtain nor construct the session key.