3.1. BAN Logic-Based Formal Security Analysis
BAN logic consists of a set of rules that can be used to analyzed information exchange protocols. It specifically determines if the information exchanged in a protocol is resistant against eavesdropping and is trustworthy and secured. The mutual authentication of the proposed protocol has been checked using the BAN logic [
44]. Different rules of BAN logic, including idealized form, assumptions, and proofs, are shown in
Table 3.
To analyze the security of a protocol using BAN logic, different goals have to be determined. In the case of the proposed protocol, eight different goals have been determined based on BAN logic. These goals are shown in the following list. 2
• Goal 1: Ri | • Goal 5: Ri |
• Goal 2: Ri | • Goal 6: Ri |
• Goal 3: Sj | • Goal 7: tag |
• Goal 4: Sj | • Goal 8: tag. |
To achieve the goals listed above, the security analysis using BAN logic has been divided into three parts. Part1 shows the idealized form of the protocol and is proved in Part3, whereas Part2 uses assumptions to analyzed the proposed protocol.
Part1: The idealized form for the proposed protocol has been discussed as follows:
M1: Ri: ,
M2: Sj: M1,
M3: Ri: V3,V4,
M4: .
Part2: The assumptions used for analyzing the proposed protocol using BAN logic are shown below: 2
• A1: | • A6: |
• A2: | • A7: |
• A3: | • A8: |
• A4: | • A9: . |
• A5: | |
Part 3: Analysis of Idealized form of the proposed protocol that has been derived on the basis of BAN logic assumptions and rules is described as follows:
M1: Ri: ,, is time-stamp of . Using the seeing rule, the following can be achieved:
According to the message-meaning rule and S1, the following can be obtained:
Using the freshness-conjuncatenation rule and S2 will achieve the following:
Using the jurisdiction rule and S3, the following can be achieved:
Using S4 and the session key rule, the following can be achieved:
Using the nonce-verification rule, the following is obtained:
M2: , whereas is time-stamp of .
By using the seeing rule, we achieve:
By the message-meaning rule and S7, the following can be achieved:
By the freshness-conjuncatenation rule and S8, the following can be computed:
By applying the jurisdiction rule and S9, the following can be obtained:
Using the S10 and the SK rule, the following can achieved:
Using the nonce-verification rule and S11, the following can be achieved:
M3: Ri: , is time-stamp of .
By the seeing-rule, the following can be achieved:
By the message-meaning rule and S13, the following can be obtained:
By S14 and the freshness-conjuncatenation rule, the following can achieved:
By the assumption S15 and jurisdiction rule, the following can be achieved:
Using S16 and the session-key rule, the following can be achieved:
Applying nonce-verification rule, the following can be computed:
M4: , is timestamp of .
Using the seeing rule, the following can be computed:
Using the message-meaning rule and S19, the following is achieved:
Using S20 and the freshness-conjuncatenation rule, the following can be obtained:
Using the jurisdiction rule and S21, the following can be achieved:
Using the session-key rule, the following can be obtained:
Finally, using the nonce-verification rule, the following can be achieved, which is also the final goal of the proposed protocol:
Consequently, using the BAN logic, it has been shown that , , and achieve mutual authentication successfully and securely attain the session key agreement.
3.2. Security Analysis with ProVerif
Based on applied
calculus, ProVerif uses automated reasoning to test the security features of authentication protocols. Specifically, ProVerif can verify the reachability, correspondence, and observational equivalence, as well as secrecy properties. ProVerif supports primitive cryptographic operations [
45], including MAC, digital signatures, encryption/decryption, elliptic curve operations, hash, and other functions [
46]. The steps of the proposed scheme, as illustrated in
Section 2 and shown in
Figure 4 and
Figure 5, are simulated in ProVerif. The formal security validation model of ProVerif consists of three phases: (1) Declaration, as coded in
Figure 6A, declares the constants, names, variablesm, and cryptographic function, (2) Process part, as shown in
Figure 6B, defines the three processes, each for tag, Reader, and Server, and (3) Main, as implemented in
Figure 6C, simulates the actual protocol.
Simulation of three processes executed in parallel is performed, along with six events to validate the reachability properties of three processes. Finally, four queries are implemented. The results are shown in
Figure 6D. Based on the above description of results 1, 2, and 3, all three original processes of the proposed protocol successfully started and terminated. Result 4 shows that the session tag identity
is safe from any adversary attack. Therefore, the proposed protocol possesses correctness and provides tag secrecy.
3.3. Informal Security Analysis
The proposed protocol for RFID System is analyzed for security loopholes against the known attacks in the following subsections.
3.3.1. Mutual Authentication Between Tag And Server
The RFID Server authenticates RFID tag by verifying a one time alias and in the message . Only a legitimate RFID tag can form a valid request message , including both these parameters, as valid is only known to legal tag; moreover, , are known to the legal tag only. On other side, the RFID tag can authenticate the legitimacy of the Server using parameters and message in . This way, the proposed protocol achieves mutual authentication property.
3.3.2. Anonymity
One of the basic principles of security is that an authentication protocol must not reveal the identity information of any participant (user or device) to an adversary. Anonymity is an essential factor of a secure protocol. A secure scheme guards the personal information of a user so that an adversary or intruder cannot access any information that may lead to a security breach of the system. In the proposed protocol, strong anonymity has been achieved. In the registration phase, the RFID tag registered itself with the Server S through RFID-Reader using a secure channel, .
In the login and authentication phase of the proposed protocol, message has been sent to the Server S using public channel. Here, if an adversary gets the message , the adversary still cannot know the identity of the RFID tag because is a one-time alias identity of the tag. The original identity is kept encrypted in and can only be decrypted by the Server using a shared secret Key . Thus, an adversary cannot reveal the RFID tag’s actual identity, hence achieving anonymity for the proposed protocol.
3.3.3. Traceability
A genuinely secure protocol must not reveal any identifying information of the participants to an illegitimate user. The identifying information may lead to the traceability of the RFID tag. The proposed protocol does not reveal any login information of the current of or any previous sessions that lead to a security attack on the RFID system. It is achieved through the use of different random numbers at different levels, like . Furthermore, a new one-time-alias identity for the RFID tag has been use, making it impossible for an adversary to guess any random number and launch an attack on the RFID system. Consequently, it can be been claimed that the proposed protocol makes the RFID tag untraceable.
3.3.4. Backward/Forward Secrecy
It is essential for security protocols that the information transmitted in a session is not compromised, as well as traced or used by an adversary to create vulnerabilities in the current, previous, or future authentication session between the RFID tag and RFID Server S. In the proposed protocol, even if the identity or alias identity are lost, it does not affect previous or next sessions. It is ensured through the use of encrypted , which is updated in every new session. In this way, the proposed protocol for the RFID System guarantees backward and forward secrecy.
3.3.5. Scalability
In the proposed protocol for the RFID System, the RFID Server S does not perform an exhaustive process to authenticate any RFID-tag. Instead, the RFID-Server S processes to validate the RFID tag and responds quickly to the RFID tag. This makes the proposed protocol more scalable.
3.3.6. Collision Attack
If RFID-tags share the same credentials for authentication to access the RFID Server, the protocol may be left vulnerable to a collision attack. In the proposed protocol, every RFID tag uses different parameters, i.e., , for authentication that makes it impossible for collision attack to take place.
3.3.7. DoS Attack
The protocol is not based on any random key that is responsible for authentication or verification of the RFID tag; rather, it is based on that is well encrypted and updated for every transaction. Therefore, the proposed scheme resists any DoS attack.
3.3.8. Replay Attacks
In a replay attack, the attacker may delay or repeat the transmitted information for authentication with the Server S. The proposed protocol for RFID systems has three participants: tag, Reader, and Server. For authentication, four messages are exchanged, i.e, , using a public channel. Having access to the messages, an adversary A may attempt to launch a replay attack. However, this attempt will fail as every message is sent with a fresh time-stamp T. In case the time-stamp is invalid, the adversary A request will be rejected each time. Furthermore, if an adversary A cannot compute other parameters of the message, the adversary still cannot launch the attack as all message parameters are updated for every new session by the participants of RFID System. Therefore, the proposed protocol for RFID systems is resistant to replay attack.
3.3.9. Location Tracking Attack
As the real identity of the RFID tag is not sent directly in the message for authentication between the RFID-tag and Server S, it has been sent in an encrypted form that only the Server can decrypt using its secret key. Moreover, the messages exchanged among the participants are constantly updated in every new session that provides unpredictability. Hence, an adversary cannot find the location and any attempt of finding the location will ultimately fail.
3.3.10. Impersonation Attacks (Forgery Attacks)
An adversary A may intercept the messages of the previous legitimate RFID tag and modify that for authentication with the RFID Server S. In this case, the adversary A needs to make a valid message request that includes different parameters, like . To do so, the adversary A must compute that is well encrypted and impossible to be computed or forged. Moreover, the adversary A also needs different other parameters and timestamps to put a valid request for authentication as a legitimate RFID tag. It is impossible for the adversary A without knowing the actual parameters of the Message used for authentication, hence leaving the adversary A unable to prove its legitimacy as an RFID tag to the RFID Server S. Reluctantly, the proposed protocol for RFID System resists any forgery attack.
3.3.11. Stolen-Verifier Attacks
The proposed protocol resists stolen-verifier-attack. All the verification and validation keys are stored encrypted in the RFID Database Server S. If the data and keys are stolen from the RFID Database Server S, still the adversary A cannot decrypt and extract them. Also, the adversary A cannot alter or modify the original data saved in the RFID Database Server S. Hence, the proposed protocol resists any stolen-verifier attack.