Abstract
Internet of Things (IoT) aids in tracking of moving objects attached with Radio Frequency Identification tag. Earlier researchers assume that the owner of the object needs to either be online and actively participating for an update of travel status of a moving object, or rely on a third party to perform this task. If no such third party exists and owner is offline for a certain period, this leads to an inconsistent travel status. On the contrary, involvement of the third party in the update process requires it to be fully trusted, which can lead to privacy threats to the owner. Therefore, the existing works depend either on the unreliable owner device or on the vulnerable third party. This paper performs cryptanalysis on the object tracking protocol proposed by Ray et al. and discovers that this protocol does not allow the owner device to be offline, and it has various security issues. Along with this cryptanalysis, this paper proposes an IoT based object tracking system that depends only on the third party and allows the owner device to be offline. However, the vulnerabilities of this third party have been taken care in such a way that there is no privacy risk for the owner. Unlike the existing systems, this system provides unlinkability, untraceability, resistance against impersonation, information leakage through the communication link, replay, man-in-the-middle attack, desynchronization problem. In our experiment, we modeled the system using High-Level Protocol Specification Language (HLPSL) and simulated HLPSL model using automated security verification tool AVISPA.
Similar content being viewed by others
References
Musaddiq, A., Zikria, Y. B., Hahm, O., Yu, H., Bashir, A. K., & Kim, S. W. (2018). A survey on resource management in IoT operating systems. IEEE Access, 6, 8459–8482.
Nie, X., & Zhong, X. (2013). Security in the internet of things based on RFID: issues and current countermeasures. In Proceedings of the 2nd international conference on computer science and electronics engineering (pp. 1181–1184).
Baruah, B., & Dhal, S. (2018). A two-factor authentication scheme against FDM attack in IFTTT based Smart Home System. Journal of Computers & Security, 77, 21–35.
Zhang, D., He, Z., Qian, Y., Wan, J., Li, D., & Zhao, S. (2016). Revisiting unknown RFID tag identification in large-scale internet of things. Journal of Wireless Communications, 23(5), 24–29.
Karuppuswami, S., Matta, L. L., Alocilja, E. C., & Chahal, P. (2018). A wireless RFID compatible sensor tag using gold nanoparticle markers for pathogen detection in the liquid food supply chain. IEEE Sensors Letters, 2(2), 1–4.
Bi, H. H., & Lin, D. K. J. (2009). RFID-enabled discovery of supply networks. IEEE Transactions on Engineering Management, 56(1), 129–141.
Shen, Z., Zeng, P., Qian, Y., & Choo, K. R. (2018). A secure and practical RFID ownership transfer protocol based on Chebyshev polynomials. IEEE Access, 6, 14560–14566.
Jia, X., Feng, Q., Fan, T., & Lei, Q. (2012). RFID technology and its applications in Internet of Things (IoT). In Proceedings of the 2nd international conference on consumer electronics, communications and networks (pp. 1282–1285).
Park, S. S. (2018). An IoT application service using mobile RFID technology. In Proceedings of the international conference on electronics, information, and communication.
Li, R., Song, T., Capurso, N., Yu, J., Couture, J., & Cheng, X. (2017). IoT applications on secure smart shopping system. Journal of IEEE Internet of Things, 4(6), 1945–1954.
Xie, D., Qin, Y., Sheng, Q. Z., & Xu, Y. (2014). Managing uncertainties in RFID applications: A survey. In Proceedings of the 11th international conference on e-business engineering (pp. 220–225).
Ray, Biplob R., Chowdhury, Morshed U., & Abawajy, Jemal H. (2016). Secure object tracking protocol for the Internet of Things. Journal of Internet of Things, 3(4), 544–553.
Ray, B., Howdhury, M., Abawajy, J., & Jesmin, M. (2015). Secure object tracking protocol for Networked RFID Systems. In Proceedings of the 16th international conference on software engineering, artificial intelligence, networking and parallel/distributed computing.
Ray, B. R., Chowdhury, M. U., & Abawajy, J. H. (2014). PUF-based secure checker protocol for Networked RFID Systems. In Proceedings of the international conference on open systems (pp. 78–83).
Blass, E.-O., Elkhiyaoui, K., Molva, R. (2011). Tracker: Security and privacy for RFID-based supply chains. In Proceedings of the 18th annual network and distributed system security symposium (pp. 29–36).
Chen, X., Zhu, Y., Li, J., Wen, Y., & Gong, Z. (2015). Efficiency and privacy enhancement for a track and trace system of RFID-based supply chains. Journal of Information, 6(2), 258–274.
Shafagh, H., Hithnawi, A., Droescher, A., Duquennoy, S., & Hu, W. (2015). Talos: Encrypted query processing for the Internet of Things. In Proceedings of the 13th ACM conference on embedded networked sensor systems.
Elkhiyaoui, K., Blass, E.-O., & Molva, R. (2012). CHECKER: On-site checking in RFID-based supply chains. In Proceedings of the 5th ACM conference on security and privacy in wireless and mobile networks (pp. 173–184).
Ouafi, K., & Vaudenay, S. (2009). Pathchecker: An RFID application for tracing products in supply-chains. In Proceedings of the 5th workshop on RFID security (pp. 1–14).
Xin, W., Sun, H., Yang, T., Guan, Z., & Chen, Z. (2012). A privacy-preserving path-checking solution for RFID-based supply chains. In Proceedings of the international conference on information and communications security (pp. 400–407).
Xin, W., Sun, H., Wang, Z., Guan, Z., & Chen, Z. (2012). A RFID path-checking protocol based on ordered multisignatures. Radio Frequency Identification System Security, 8, 33–44.
Paillier, P. (1999). Public-key cryptosystems based on composite degree residuosity classes. In Proceedings of the 28th annual international conference on the theory and applications of cryptographic techniques, Eurocrypt (pp. 223–238), LNCS, vol. 1592. Springer
Gong, L., Needham, R., & Yahalom, R. (1990). Reasoning about belief in cryptographic protocols. In Proceedings of the IEEE Computer society symposium on research in security and privacy (pp. 234–248).
Burrows, M., & Abadi, M. (1990). A logic of authentication. ACM Transactions on Computer Systems, 8(1), 18–36.
Takkinen, L. (2006). Analysing security protocols with AVISPA. In TKK T-110.7290 research seminar on network security.
Sadeghi, A.-R., Visconti, I., & Wachsmann, C. (2010). Enhancing RFID security and privacy by physically unclonable functions. In Towards hardware-intrinsic security (pp. 281–305).
Viganò, L. (2006). Automated security protocol analysis with the AVISPA tool. Electronic Notes in Theoretical Computer Science, 155, 61–86.
SPAN. A security protocol animator for AVISPA. http://people.irisa.fr/Thomas.Genet/span/.
AVISPA. Automated validation of internet security protocols and applications. http://www.avispa-project.org/.
Kitsos, P. (Ed.). (2016). Enhancing RFID security and privacy by physically unclonable functions. In Security in RFID and sensor networks. Boston, MA: Auerbach Publications.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Appendices
Appendix 1: Verification Using BAN Logic
Notations BAN Logic Notations used to verify the proposed framework are as follows:
-
A \(\arrowvert \equiv\) B: A believes B
-
A \(\ni\) M: A possesses M
-
A \(\triangleleft\) M: A sees M/ A is told M
-
\(\phi\)(M): M is recognizable, if there are certain expectations about the contents of M before actually receiving it, i.e., a particular value, a particular structure or a particular form of redundancy can be recognized
-
A \(\arrowvert \sim\) M: A once conveyed M, where M can be a message itself or some content computable from such a message, i.e. M can be conveyed implicitly
-
#(M): M is fresh and has not been used for the same purpose at any time before the current run of the protocol
-
A \({\mathop {\rightleftharpoons }\limits ^{X}}\) B: X is a secret known only to A and B
-
\(\langle X \rangle\): A secret X used for identification purposes
-
\({\mathop {\mapsto }\limits ^{k}} A\): A has k as a public key
-
\(\langle M \rangle _N\): M combined with (secret) formula N
-
\(\{M\}_k\): M encrypted under the key k
-
A \(\triangleleft\)\(\star\)M: A is told M which A did not convey previously
-
A \(\arrowvert \equiv\)\(\otimes\)(A): A believes it can identify the messages that were not originated by itself in current or previous sessions
-
\(\frac{X}{Y}\): If X is true, then Y is true
Rules Rules used to verify the proposed system are as follows:
-
R1:
Fresh rule: \(\frac{A \arrowvert \equiv \#(M)}{A \arrowvert \equiv \#(M, N), A \arrowvert \equiv \#F(M)}\)
-
R2:
Possession rule: \(\frac{A \triangleleft M}{A \ni M}\)
-
R3:
Possession rule: \(\frac{A \ni M, A \ni N}{A \ni (M,N), A \ni F(M,N)}\)
-
R4:
Being told rule: \(\frac{A \triangleleft (M, N)}{A \triangleleft (M)}\)
-
R5:
Message interpretation rule:
$$\begin{aligned} \frac{A \triangleleft \star H(X, \langle S \rangle ), A \ni (X,S), A \arrowvert \equiv A {\mathop {\rightleftharpoons }\limits ^{S}} B, A \arrowvert \equiv \phi (X,S), A \arrowvert \equiv \otimes (A)}{A \arrowvert \equiv B \arrowvert \sim (X, \langle S \rangle ), A \arrowvert \equiv B \arrowvert \sim H(X, \langle S \rangle )} \end{aligned}$$ -
R6:
Fresh rule: \(\frac{A \arrowvert \equiv \#(M), A \ni M}{A \arrowvert \equiv \#(H(M))}\)
-
R7:
Message-meaning rule: \(\frac{A \arrowvert \equiv A {\mathop {\rightleftharpoons }\limits ^{N}} B, A \triangleleft \langle M \rangle _{N}}{A \arrowvert \equiv B \arrowvert \sim M}\)
Message Exchange In this scheme, the active participants are \(T_j\), \(P_i\) and CS. The messages exchanged among the entities used to verify the proposed system are as follows:
M1: \(T_j\)\(\triangleleft\) (\(cc_i\), \(rs_ic\), \(N_c\)), M2: CS \(\triangleleft\) (\(EE_T\), NN),
M3: \(T_j\)\(\triangleleft\)\(V_{CS}\),
M4: CS \(\triangleleft\) (\(Q_{CO}\), \(R_2\)),
M5: owner \(\triangleleft\) (\(sst_j\), \(R_{CS}\)),
Assumption 1
The assumptions of the scheme are:
-
A1:
CS \(\arrowvert \equiv\) #(\(N_c\))
-
A2:
\(T_j\)\(\ni\) (\(c_i\)\(\oplus\) PRF(n))
-
A3:
\(T_j\) \(\arrowvert \equiv\) \(P_i\) \({\mathop {\rightleftharpoons }\limits ^{c_i \oplus PRF(n)}}\) \(T_j\)
-
A4:
\(T_j\)\(\arrowvert \equiv\)\(\phi\)(\(N_c\), \(c_i\)\(\oplus\) PRF(n))
-
A5:
\(T_j\)\(\arrowvert \equiv\)\(\otimes\)(\(T_j\))
-
A6:
CS \(\ni\) (\(E_{T_{ic}}\)\(\oplus\)\({\mathcal {E}}\)(\(st_j\)))
-
A7:
CS \(\arrowvert \equiv\)\(T_j\)\({\mathop {\rightleftharpoons }\limits ^{E_{T_{ic}} \oplus {\mathcal {E}}(st_j)}}\) CS
-
A8:
CS \(\arrowvert \equiv\)\(\phi\)(\(N_c\)\(\oplus\) NN, \(E_{T_{ic}}\)\(\oplus\)\({\mathcal {E}}\)(\(st_j\)))
-
A9:
CS \(\arrowvert \equiv\)\(\otimes\)(CS)
-
A10:
\(T_j\)\(\arrowvert \equiv\) #(NN)
-
A13:
\(T_j\)\(\arrowvert \equiv\) CS \({\mathop {\rightleftharpoons }\limits ^{E(TC_{jc})}}\)\(T_j\)
-
A14:
\(T_j\)\(\arrowvert \equiv\)\(\phi\)(\(N_c\)\(\oplus\) NN, E(\(TC_{jc}\)))
-
A15:
CS \(\arrowvert \equiv\) #(\(R_1\))
-
A16:
owner \(\arrowvert \equiv\) #(\(R_2\))
-
A17:
CS \(\arrowvert \equiv\) owner \({\mathop {\rightleftharpoons }\limits ^{E(TC_{jc})}}\) CS
Possessions
Some of the possessions of the entities used to verify the proposed system are as follows:
P1: CS \(\ni\) (E(\(TC_{jc}\))), P2: CS \(\ni\)\(N_c\), P3: \(T_j\)\(\ni\) NN, P4: CS \(\ni\) (\(E_{T_{ic}}\)\(\oplus\)\({\mathcal {E}}\)(\(st_j\))), P5: \(T_j\)\(\ni\) (E(\(TC_{jc}\))), P6: CS \(\ni\)\(R_1\),
Goal
Goals refer to belief and freshness of the messages exchanged among the entities. Goals of the system are:
G1: \(T_j\)\(\arrowvert \equiv\)\(P_i\)\(\arrowvert \sim\)\(cc_i\), G2: CS \(\arrowvert \equiv\)\(T_j\)\(\arrowvert \sim\)\(EE_T\), G3: CS \(\arrowvert \equiv\)\(\#(EE_T)\), G4: \(T_j\)\(\arrowvert \equiv\)\(\#(V_{CS})\), G5: \(T_j\)\(\arrowvert \equiv\) CS \(\arrowvert \sim\)\((V_{CS})\), G6: CS \(\arrowvert \equiv\)\(\#(Q_{CO})\), G7: CS \(\arrowvert \equiv\) owner \(\arrowvert \sim\)\((Q_{CO})\), G8: owner \(\arrowvert \equiv\)\(\#(sst_j)\), G9: owner \(\arrowvert \equiv\) CS \(\arrowvert \sim\)\((sst_j)\)
Logic Verification Logic verification has been performed based on the messages exchanged, assumptions and BAN logic rules.
Goal 1: \(T_j\) \(\arrowvert \equiv\) \(P_i\) \(\arrowvert \sim\) \(cc_i\)
Proof
According to Message M1 and Rule R4, we obtain that, \(T_j\)\(\triangleleft\)\(\star\) H(\(N_c\),\(\langle c_i\)\(\oplus\) PRF(n)\(\rangle\)). According to Message M1, Rule R2 and Rule R4, we obtain that, \(T_j\)\(\ni\)\(N_c\). Next using Assumption A2, \(T_j\)\(\ni\)\(N_c\) and Rule R3, it turns out that, \(T_j\)\(\ni\) (\(N_c\), \(c_i\)\(\oplus\) PRF(n)). Using \(T_j\)\(\triangleleft\)\(\star\) H(\(N_c\),\(\langle c_i\)\(\oplus\) PRF(n)\(\rangle\)), \(T_j\)\(\ni\) (\(N_c\), \(c_i\)\(\oplus\) PRF(n)) and applying Assumption A3, Assumption A4, Assumption A5 and Rule R5, we obtain that, \(T_j\)\(\arrowvert \equiv\)\(P_i\)\(\arrowvert \sim\) H(\(N_c\),\(\langle c_i\)\(\oplus\) PRF(n)\(\rangle\)). Hence the goal G1 has been achieved, i.e., \(T_j\)\(\arrowvert \equiv\)\(P_i\)\(\arrowvert \sim\)\(cc_i\)\(\square\)
Goal 2: CS \(\arrowvert \equiv\)\(T_j\)\(\arrowvert \sim\)\(EE_T\)
Proof
Using Message M2 and Rule R4, we obtain that, CS \(\triangleleft\)\(\star\) H(\(N_c\)\(\oplus\) NN,\(\langle E_{T_{ic}}\)\(\oplus\)\({\mathcal {E}}\)(\(st_j\))\(\rangle\)). According to Message M2, Rule R2 and Rule R4, we obtain that, CS \(\ni\) NN. Now applying Rule R3, Possession P2, CS \(\ni\) NN, it turns out that, CS \(\ni\)\(N_c\)\(\oplus\) NN. Next using Assumption A6, CS \(\ni\)\(N_c\)\(\oplus\) NN and Rule R3, it turns out that, CS \(\ni\) (\(N_c\)\(\oplus\) NN, \(E_{T_{ic}}\)\(\oplus\)\({\mathcal {E}}\)(\(st_j\))). Using CS \(\triangleleft\)\(\star\) H(\(N_c\)\(\oplus\) NN,\(\langle E_{T_{ic}}\)\(\oplus\)\({\mathcal {E}}\)(\(st_j\))\(\rangle\)), CS \(\ni\) (\(N_c\)\(\oplus\) NN, \(E_{T_{ic}}\)\(\oplus\)\({\mathcal {E}}\)(\(st_j\))) and applying Assumption A7, Assumption A8, Assumption A9 and Rule R5, we obtain that CS \(\arrowvert \equiv\)\(T_j\)\(\arrowvert \sim\) H(\(N_c\)\(\oplus\) NN,\(\langle E_{T_{ic}}\)\(\oplus\)\({\mathcal {E}}\)(\(st_j\))\(\rangle\)). Hence the goal G2 has been achieved. \(\square\)
Goal 3: CS \(\arrowvert \equiv\)\(\#(EE_T)\)
Proof
Using Assumption A1 and Rule R1, it turns out that, CS \(\arrowvert \equiv\)\(\#(E_{T_{ic}}\)\(\oplus\)\({\mathcal {E}}\)(\(st_j\)) \(\oplus\)\(N_c\)\(\oplus\) NN). Using Message M2, Rule R2 and Rule R4, it turns out that, CS \(\ni\) NN. Using Possession P2, Possession P4, CS \(\ni\) NN and Rule R3, we obtain that, CS \(\ni\) (\(E_{T_{ic}}\)\(\oplus\)\({\mathcal {E}}\)(\(st_j\)) \(\oplus\)\(N_c\)\(\oplus\) NN). Using CS \(\arrowvert \equiv\)\(\#(E_{T_{ic}} \oplus {\mathcal {E}}\)(\(st_j\)) \(\oplus\)\(N_c\)\(\oplus\) NN), CS \(\ni\) (\(E_{T_{ic}}\)\(\oplus\)\({\mathcal {E}}\)(\(st_j\)) \(\oplus\)\(N_c\)\(\oplus\) NN) and Rule R6, we obtain that, CS \(\arrowvert \equiv\)\(\#H(E_{T_{ic}} \oplus {\mathcal {E}}\)(\(st_j\)) \(\oplus\)\(N_c\)\(\oplus\) NN). Hence the goal G3 has been achieved, i.e., CS \(\arrowvert \equiv\)\(\#(EE_T)\). CS believes that the message is not a replay. \(\square\)
Goal 4: \(T_j\) \(\arrowvert \equiv\) \(\#(V_{CS})\)
Proof
Using Assumption A10 and Rule R1, it turns out that, \(T_j\)\(\arrowvert \equiv\)\(\#(E\)(\(TC_{jc}\)) \(\oplus\)\(N_c\)\(\oplus\) NN). According to Message M1, Rule R2 and Rule R4, we obtain that, \(T_j\)\(\ni\)\(N_c\). Using Possession P3, Possession P5, \(T_j\)\(\ni\)\(N_c\) and Rule R3, we obtain that, \(T_j\)\(\ni\) (E(\(TC_{jc}\)) \(\oplus\)\(N_c\)\(\oplus\) NN). Using \(T_j\)\(\arrowvert \equiv\)\(\#(E\)(\(TC_{jc}\)) \(\oplus\)\(N_c\)\(\oplus\) NN), \(T_j\)\(\ni\) (E(\(TC_{jc}\)) \(\oplus\)\(N_c\)\(\oplus\) NN) and Rule R6, we obtain that, \(T_j\)\(\arrowvert \equiv\)\(\#H(E\)(\(TC_{jc}\)) \(\oplus\)\(N_c\)\(\oplus\) NN), i.e., \(T_j\)\(\arrowvert \equiv\)\(\#(V_{CS})\). \(T_j\) believes that the message is not a replay. Hence the goal G4 has been achieved. \(\square\)
Goal 5:\(T_j\)\(\arrowvert \equiv\) CS \(\arrowvert \sim\)\((V_{CS})\)
Proof
Using Message M3, we obtain that, \(T_j\)\(\triangleleft\)\(\star\) H(\(N_c\)\(\oplus\) NN,\(\langle E\)(\(TC_{jc}\))\(\rangle\)). According to Message M1, Rule R2 and Rule R4, we obtain that, \(T_j\)\(\ni\)\(N_c\). Now applying Rule R3, Possession P3, \(T_j\)\(\ni\)\(N_c\), it turns out that, \(T_j\)\(\ni\)\(N_c\)\(\oplus\) NN. Next using Possession P5, \(T_j\)\(\ni\)\(N_c\)\(\oplus\) NN and Rule R3, it turns out that, \(T_j\)\(\ni\) (\(N_c\)\(\oplus\) NN, E(\(TC_{jc}\))). Next using \(T_j\)\(\triangleleft\)\(\star\) H(\(N_c\)\(\oplus\) NN,\(\langle E\)(\(TC_{jc}\))\(\rangle\)), \(T_j\)\(\ni\) (\(N_c\)\(\oplus\) NN, E(\(TC_{jc}\))) and applying Assumption A11, Assumption A12, Assumption A5 and Rule R5, we obtain that \(T_j\)\(\arrowvert \equiv\) CS \(\arrowvert \sim\) H(\(N_c\)\(\oplus\) NN,\(\langle E\)(\(TC_{jc}\))\(\rangle\)). Hence the goal G5 has been achieved, i.e., \(T_j\)\(\arrowvert \equiv\) CS \(\arrowvert \sim\)\((V_{CS})\). \(\square\)
Goal 6: CS \(\arrowvert \equiv\)\(\#(Q_{CO})\)
Proof
Using Assumption A13 and Rule R1, it turns out that, CS \(\arrowvert \equiv\)\(\#(E\)(\(TC_{jc}\)) \(\oplus\)\(R_1\)\(\oplus\)\(R_2\)). According to Message M4, Rule R2 and Rule R4, we obtain that, CS \(\ni\)\(R_2\). Using Possession P6, Possession P1, CS \(\ni\)\(R_2\) and Rule R3, we obtain that, CS \(\ni\) (E(\(TC_{jc}\)) \(\oplus\)\(R_1\)\(\oplus\)\(R_2\)). Using CS \(\arrowvert \equiv\)\(\#(E\)(\(TC_{jc}\)) \(\oplus\)\(R_1\)\(\oplus\)\(R_2\)), CS \(\ni\) (E(\(TC_{jc}\)) \(\oplus\)\(R_1\)\(\oplus\)\(R_2\)) and Rule R6, we obtain that, CS \(\arrowvert \equiv\)\(\#H(E\)(\(TC_{jc}\)) \(\oplus\)\(R_1\)\(\oplus\)\(R_2\)). Hence the goal G6 has been achieved, i.e., CS \(\arrowvert \equiv\)\(\#(Q_{CO})\). \(\square\)
Goal 7: CS \(\arrowvert \equiv\) owner \(\arrowvert \sim\)\((Q_{CO})\)
Proof
Using Message M4 and Rule R4, we obtain that, CS \(\triangleleft\)\(\star\) H(\(R_1\)\(\oplus\)\(R_2\),\(\langle E\)(\(TC_{jc}\))\(\rangle\)). According to Message M4, Rule R2 and Rule R4, we obtain that, CS \(\ni\)\(R_2\). Using Possession P6, CS \(\ni\)\(R_2\) and Rule R3, it turns out that, CS \(\ni\)\(R_1\)\(\oplus\)\(R_2\). Next using Possession P1, CS \(\ni\)\(R_1\)\(\oplus\)\(R_2\) and Rule R3, it turns out that, CS \(\ni\) (\(R_1\)\(\oplus\)\(R_2\), E(\(TC_{jc}\))). Next using CS \(\triangleleft\)\(\star\) H(\(R_1\)\(\oplus\)\(R_2\),\(\langle E\)(\(TC_{jc}\))\(\rangle\)), CS \(\ni\) (\(R_1\)\(\oplus\)\(R_2\), E(\(TC_{jc}\))) and applying Assumption A14, Assumption A15, Assumption A9 and Rule R5, we obtain that, CS \(\arrowvert \equiv\) owner \(\arrowvert \sim\) H(\(R_1\)\(\oplus\)\(R_2\),\(\langle E\)(\(TC_{jc}\))\(\rangle\)). Hence the goal G7 has been achieved. \(\square\)
Goal 8: owner \(\arrowvert \equiv\)\(\#(sst_j)\)
Proof
Using Assumption A16 and Rule R1, we obtain that, owner \(\arrowvert \equiv\)\(\#(sst_j)\). Hence the goal G8 has been achieved. \(\square\)
Goal 9: owner \(\arrowvert \equiv\) CS \(\arrowvert \sim\)\({\mathcal {E}}\)(\(st_j^{new}\))
Proof
Using Message M5 and Rule R4, it turns out that, owner \(\triangleleft\)\(sst_j\), i.e., owner \(\triangleleft\)\(\langle {\mathcal {E}}\)(\(st_j^{new}\))\(\rangle _{E(TC_{jc})}\). Using Assumption A17, owner \(\triangleleft\)\(\langle\)\(st_j^{new}\rangle _{E(TC_{jc})}\) and Rule R7, we obtain that, owner \(\arrowvert \equiv\) CS \(\arrowvert \sim\)\({\mathcal {E}}\)(\(st_j^{new}\)). Hence the goal G9 has been achieved. \(\square\)
Appendix 2: Specifications of the Roles, Environment and Goal for Update Protocol and Retrieval Protocol
Rights and permissions
About this article
Cite this article
Baruah, B., Dhal, S. An IoT Based Secure Object Tracking System. Wireless Pers Commun 106, 1209–1242 (2019). https://doi.org/10.1007/s11277-019-06210-7
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11277-019-06210-7