{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,8]],"date-time":"2026-02-08T08:36:54Z","timestamp":1770539814951,"version":"3.49.0"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2025,2,1]],"date-time":"2025-02-01T00:00:00Z","timestamp":1738368000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,2,1]],"date-time":"2025-02-01T00:00:00Z","timestamp":1738368000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2025,2]]},"DOI":"10.1007\/s10009-025-00793-2","type":"journal-article","created":{"date-parts":[[2025,4,22]],"date-time":"2025-04-22T15:11:45Z","timestamp":1745334705000},"page":"5-19","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formal verification and security analysis of MQTT-SN"],"prefix":"10.1007","volume":"27","author":[{"given":"Wei","family":"Lin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sini","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,4,22]]},"reference":[{"key":"793_CR1","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/j.matpr.2021.05.067","volume":"51","author":"K. Gulati","year":"2022","unstructured":"Gulati, K., Boddu, R.S.K., Kapila, D., Bangare, S.L., Chandnani, N., Saravanan, G.: A review paper on wireless sensor network techniques in Internet of Things (IoT). Mater. Today Proc. 51, 161\u2013165 (2022)","journal-title":"Mater. Today Proc."},{"key":"793_CR2","doi-asserted-by":"publisher","first-page":"161103","DOI":"10.1109\/ACCESS.2021.3131367","volume":"9","author":"S. Lata","year":"2021","unstructured":"Lata, S., Mehfuz, S., Urooj, S.: Secure and reliable WSN for Internet of Things: challenges and enabling technologies. IEEE Access 9, 161103\u2013161128 (2021)","journal-title":"IEEE Access"},{"key":"793_CR3","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-030-38516-3_5","volume-title":"Integration of WSN and IoT for Smart Cities","author":"K. Bajaj","year":"2020","unstructured":"Bajaj, K., Sharma, B., Singh, R.: Integration of WSN with IoT applications: a vision, architecture, and future challenges. In: Integration of WSN and IoT for Smart Cities, pp.\u00a079\u2013102 (2020)"},{"issue":"1","key":"793_CR4","doi-asserted-by":"publisher","DOI":"10.3390\/asi3010014","volume":"3","author":"D. Kandris","year":"2020","unstructured":"Kandris, D., Nakas, C., Vomvas, D., Koulouras, G.: Applications of wireless sensor networks: an up-to-date survey. Appl. Syst. Innov. 3(1), 14 (2020)","journal-title":"Appl. Syst. Innov."},{"key":"793_CR5","doi-asserted-by":"publisher","DOI":"10.1088\/1742-6596\/1969\/1\/012042","volume":"1969","author":"S. Sharma","year":"2021","unstructured":"Sharma, S., Kaur, A.: Survey on wireless sensor network, its applications and issues. J. Phys. Conf. Ser. 1969, 012042 (2021)","journal-title":"J. Phys. Conf. Ser."},{"issue":"3","key":"793_CR6","first-page":"45","volume":"12","author":"O.I. Khalaf","year":"2020","unstructured":"Khalaf, O.I., Abdulsahib, G.M.: Energy efficient routing and reliable data transmission protocol in WSN. Int. J. Adv. Soft Comput. Appl. 12(3), 45\u201353 (2020)","journal-title":"Int. J. Adv. Soft Comput. Appl."},{"key":"793_CR7","doi-asserted-by":"publisher","DOI":"10.1016\/j.adhoc.2022.102982","volume":"136","author":"E. Av\u015far","year":"2022","unstructured":"Av\u015far, E., Mowla, M.N.: Wireless communication protocols in smart agriculture: a review on applications, challenges and future trends. Ad Hoc Netw. 136, 102982 (2022)","journal-title":"Ad Hoc Netw."},{"issue":"2","key":"793_CR8","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1016\/j.jksuci.2023.01.008","volume":"35","author":"B.A. Begum","year":"2023","unstructured":"Begum, B.A., Nandury, S.V.: Data aggregation protocols for WSN and IoT applications\u2013a comprehensive survey. J. King Saud Univ, Comput. Inf. Sci. 35(2), 651\u2013681 (2023)","journal-title":"J. King Saud Univ, Comput. Inf. Sci."},{"key":"793_CR9","unstructured":"Stanford-Clark, A., Truong, H.L.: MQTT for sensor networks (MQTT-SN) protocol specification. International business machines (IBM) Corporation version 1.2, 1\u201328 (2013)"},{"key":"793_CR10","unstructured":"OASIS: MQTT Version 5.0 (2019). https:\/\/docs.oasis-open.org\/mqtt\/mqtt\/v5.0\/mqtt-v5.0.html"},{"key":"793_CR11","doi-asserted-by":"crossref","unstructured":"Faris, M., Mahmud, M.N., Salleh, M.F.M., Alnoor, A.: Wireless sensor network security: a recent review based on state-of-the-art works. Int. J. Eng. Bus. Manag. 15 (2023)","DOI":"10.1177\/18479790231157220"},{"key":"793_CR12","first-page":"1","volume-title":"Wireless Mesh Networks-Security, Architectures and Protocols","author":"O.O. Olakanmi","year":"2020","unstructured":"Olakanmi, O.O., Dada, A.: Wireless sensor networks (WSNs): security and privacy issues and solutions. In: Wireless Mesh Networks-Security, Architectures and Protocols vol.\u00a013, pp.\u00a01\u201316 (2020)"},{"issue":"3","key":"793_CR13","doi-asserted-by":"publisher","first-page":"761","DOI":"10.32604\/iasc.2021.012806","volume":"27","author":"A.K. Singh","year":"2021","unstructured":"Singh, A.K., Alshehri, M., Bhushan, S., Kumar, M., Alfarraj, O., Pardarshani, K.R.: Secure and energy efficient data transmission model for WSN. Intell. Autom. Soft Comput. 27(3), 761\u2013769 (2021)","journal-title":"Intell. Autom. Soft Comput."},{"issue":"12","key":"793_CR14","doi-asserted-by":"publisher","first-page":"2022","DOI":"10.1016\/j.comnet.2009.02.023","volume":"53","author":"S. Ozdemir","year":"2009","unstructured":"Ozdemir, S., Xiao, Y.: Secure data aggregation in wireless sensor networks: a comprehensive overview. Comput. Netw. 53(12), 2022\u20132037 (2009)","journal-title":"Comput. Netw."},{"key":"793_CR15","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.aej.2023.03.061","volume":"72","author":"S. Urooj","year":"2023","unstructured":"Urooj, S., Lata, S., Ahmad, S., Mehfuz, S., Kalathil, S.: Cryptographic data security for reliable wireless sensor network. Alex. Eng. J. 72, 37\u201350 (2023)","journal-title":"Alex. Eng. J."},{"key":"793_CR16","first-page":"119","volume-title":"2019 Sixth International Conference on Internet of Things: Systems, Management and Security (IOTSMS)","author":"O. Sadio","year":"2019","unstructured":"Sadio, O., Ngom, I., Lishou, C.: Lightweight security scheme for MQTT\/MQTT-SN protocol. In: 2019 Sixth International Conference on Internet of Things: Systems, Management and Security (IOTSMS), pp.\u00a0119\u2013123. IEEE (2019)"},{"key":"793_CR17","doi-asserted-by":"publisher","DOI":"10.1088\/1742-6596\/2020\/1\/012044","volume":"2020","author":"T. Kao","year":"2021","unstructured":"Kao, T., Wang, H., Li, J.: Safe MQTT-SN: a lightweight secure encrypted communication in IoT. J. Phys. Conf. Ser. 2020, 012044 (2021)","journal-title":"J. Phys. Conf. Ser."},{"key":"793_CR18","first-page":"692","volume-title":"Design, Automation & Test in Europe Conference & Exhibition (DATE), 2017","author":"F. De Santis","year":"2017","unstructured":"De Santis, F., Schauer, A., Sigl, G.: ChaCha20-Poly1305 authenticated encryption for high-speed embedded IoT applications. In: Design, Automation & Test in Europe Conference & Exhibition (DATE), 2017, pp.\u00a0692\u2013697. IEEE (2017)"},{"key":"793_CR19","first-page":"115","volume-title":"International Conference on Engineering of Computer-Based Systems","author":"W. Lin","year":"2023","unstructured":"Lin, W., Chen, S., Zhu, H.: Formalization and verification of MQTT-SN communication using CSP. In: International Conference on Engineering of Computer-Based Systems, pp.\u00a0115\u2013132. Springer, Berlin (2023)"},{"key":"793_CR20","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall International, Englewood Cliffs (1985)"},{"key":"793_CR21","volume-title":"Model Checking CSP Revisited: Introducing a Process Analysis Toolkit","author":"J. Sun","year":"2008","unstructured":"Sun, J., Liu, Y., Dong, J.S.: Model Checking CSP Revisited: Introducing a Process Analysis Toolkit. Springer, Berlin (2008)"},{"key":"793_CR22","unstructured":"National University of Singapore: PAT: Process Analysis Toolkit (2007). https:\/\/pat.comp.nus.edu.sg\/"},{"key":"793_CR23","doi-asserted-by":"publisher","first-page":"1248","DOI":"10.1145\/3377811.3380419","volume-title":"Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering","author":"H. Yu","year":"2020","unstructured":"Yu, H., Chen, Z., Fu, X., Wang, J., Su, Z., Sun, J., Huang, C., Dong, W.: Symbolic verification of message passing interface programs. In: Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering, pp.\u00a01248\u20131260 (2020)"},{"key":"793_CR24","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2020.110559","volume":"165","author":"A. Liu","year":"2020","unstructured":"Liu, A., Zhu, H., Popovic, M., Xiang, S., Zhang, L.: Formal analysis and verification of the PSTM architecture using CSP. J. Syst. Softw. 165, 110559 (2020)","journal-title":"J. Syst. Softw."},{"issue":"10","key":"793_CR25","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/32.637148","volume":"23","author":"G. Lowe","year":"1997","unstructured":"Lowe, G., Roscoe, B.: Using CSP to detect errors in the TMN protocol. IEEE Trans. Softw. Eng. 23(10), 659\u2013669 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"793_CR26","first-page":"616","volume-title":"International Conference on Parallel and Distributed Computing: Applications and Technologies","author":"S. Chen","year":"2021","unstructured":"Chen, S., Li, R., Zhu, H.: Formalization and verification of group communication CoAP using CSP. In: International Conference on Parallel and Distributed Computing: Applications and Technologies, pp.\u00a0616\u2013628. Springer, Berlin (2021)"},{"key":"793_CR27","doi-asserted-by":"publisher","first-page":"226422","DOI":"10.1109\/ACCESS.2020.3045441","volume":"8","author":"C.-S. Park","year":"2020","unstructured":"Park, C.-S., Nam, H.-M.: Security architecture and protocols for secure MQTT-SN. IEEE Access 8, 226422\u2013226436 (2020)","journal-title":"IEEE Access"},{"issue":"21","key":"793_CR28","doi-asserted-by":"publisher","DOI":"10.3390\/app122110991","volume":"12","author":"J. Rold\u00e1n-G\u00f3mez","year":"2022","unstructured":"Rold\u00e1n-G\u00f3mez, J., Carrillo-Mond\u00e9jar, J., Castelo G\u00f3mez, J.M., Ruiz-Villafranca, S.: Security analysis of the MQTT-SN protocol for the Internet of Things. Appl. Sci. 12(21), 10991 (2022)","journal-title":"Appl. Sci."},{"key":"793_CR29","first-page":"291","volume-title":"International Conference on Innovative Computing and Communications: Proceedings of ICICC 2020","author":"N. Verma","year":"2020","unstructured":"Verma, N., Kaushik, A., Nayak, P.: A lightweight secure authentication protocol for wireless sensor networks. In: International Conference on Innovative Computing and Communications: Proceedings of ICICC 2020, vol.\u00a01, pp.\u00a0291\u2013299. Springer, Berlin (2020)"},{"key":"793_CR30","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1109\/SmartCloud49737.2020.00032","volume-title":"2020 IEEE International Conference on Smart Cloud (SmartCloud)","author":"F. Chen","year":"2020","unstructured":"Chen, F., Huo, Y., Zhu, J., Fan, D.: A review on the study on MQTT security challenge. In: 2020 IEEE International Conference on Smart Cloud (SmartCloud), pp.\u00a0128\u2013133. IEEE (2020)"},{"key":"793_CR31","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1109\/ISCTURKEY53027.2021.9654337","volume-title":"2021 International Conference on Information Security and Cryptology (ISCTURKEY)","author":"E. Atilgan","year":"2021","unstructured":"Atilgan, E., Ozcelik, I., Yolacan, E.N.: MQTT security at a glance. In: 2021 International Conference on Information Security and Cryptology (ISCTURKEY), pp.\u00a0138\u2013142. IEEE (2021)"},{"issue":"6","key":"793_CR32","doi-asserted-by":"publisher","first-page":"3368","DOI":"10.1080\/03772063.2021.1912651","volume":"69","author":"A.J. Hintaw","year":"2023","unstructured":"Hintaw, A.J., Manickam, S., Aboalmaaly, M.F., Karuppayah, S.: MQTT vulnerabilities, attack vectors and solutions in the Internet of Things (IoT). IETE J. Res. 69(6), 3368\u20133397 (2023)","journal-title":"IETE J. Res."},{"key":"793_CR33","doi-asserted-by":"publisher","first-page":"629","DOI":"10.23919\/DATE.2018.8342086","volume-title":"2018 Design, Automation & Test in Europe Conference & Exhibition (DATE)","author":"Y. Shen","year":"2018","unstructured":"Shen, Y., Rezaei, A., Zhou, H.: Sat-based bit-flipping attack on logic encryptions. In: 2018 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp.\u00a0629\u2013632. IEEE (2018)"},{"issue":"1","key":"793_CR34","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1007\/s11277-020-08044-0","volume":"118","author":"S. Singh","year":"2021","unstructured":"Singh, S., Saini, H.S.: Learning-based security technique for selective forwarding attack in clustered WSN. Wirel. Pers. Commun. 118(1), 789\u2013814 (2021)","journal-title":"Wirel. Pers. Commun."},{"issue":"2","key":"793_CR35","doi-asserted-by":"publisher","first-page":"16","DOI":"10.53608\/estudambilisim.1297052","volume":"4","author":"M.M. \u015eim\u015fek","year":"2023","unstructured":"\u015eim\u015fek, M.M., At\u0131lgan, E.: Attacks on availability of IoT middleware protocols: a case study on MQTT. J. ESTUDAM Inf. 4(2), 16\u201327 (2023)","journal-title":"J. ESTUDAM Inf."},{"key":"793_CR36","unstructured":"Li, W., Manickam, S., Nanda, P., Al-Ani, A.K., Karuppayah, S., et\u00a0al.: Securing MQTT ecosystem: Exploring vulnerabilities, mitigations, and future trajectories. IEEE Access (2024)"},{"key":"793_CR37","first-page":"350","volume-title":"Proceedings of the 8th International Conference on Sciences of Electronics, Technologies of Information and Telecommunications (SETIT\u201918)","author":"J. Hcine","year":"2020","unstructured":"Hcine, J., Ben Hafaiedh, I.: Formal-based modeling and analysis of a network communication protocol for IoT: MQTT protocol. In: Proceedings of the 8th International Conference on Sciences of Electronics, Technologies of Information and Telecommunications (SETIT\u201918), vol.\u00a02, pp.\u00a0350\u2013360. Springer, Berlin (2020)"},{"key":"793_CR38","series-title":"Proceedings","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-319-69483-2_16","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium","author":"M. Diwan","year":"2017","unstructured":"Diwan, M., D\u2019Souza, M.: A framework for modeling and verifying IoT communication protocols. In: Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017. Proceedings, vol.\u00a03, pp.\u00a0266\u2013280. Springer (2017)"},{"key":"793_CR39","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-030-59028-4_7","volume-title":"International Conference on Database and Expert Systems Applications","author":"H. Sochor","year":"2020","unstructured":"Sochor, H., Ferrarotti, F., Ramler, R.: Exploiting MQTT-SN for distributed reflection denial-of-service attacks. In: International Conference on Database and Expert Systems Applications, pp.\u00a074\u201381. Springer, Berlin (2020)"},{"issue":"14","key":"793_CR40","doi-asserted-by":"publisher","DOI":"10.3390\/app13148122","volume":"13","author":"M. Krichen","year":"2023","unstructured":"Krichen, M.: A survey on formal verification and validation techniques for Internet of Things. Appl. Sci. 13(14), 8122 (2023)","journal-title":"Appl. Sci."},{"key":"793_CR41","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2020.107233","volume":"174","author":"K. Hofer-Schmitz","year":"2020","unstructured":"Hofer-Schmitz, K., Stojanovi\u0107, B.: Towards formal verification of IoT protocols: a review. Comput. Netw. 174, 107233 (2020)","journal-title":"Comput. Netw."},{"key":"793_CR42","doi-asserted-by":"publisher","first-page":"736","DOI":"10.1016\/j.procs.2011.07.097","volume":"5","author":"A. Gawanmeh","year":"2011","unstructured":"Gawanmeh, A.: Embedding and verification of ZigBee protocol stack in Event-B. Proc. Comput. Sci. 5, 736\u2013741 (2011)","journal-title":"Proc. Comput. Sci."},{"key":"793_CR43","doi-asserted-by":"publisher","first-page":"621","DOI":"10.1007\/s10009-006-0014-x","volume":"8","author":"M. Duflot","year":"2006","unstructured":"Duflot, M., Kwiatkowska, M., Norman, G., Parker, D.: A formal analysis of Bluetooth device discovery. Int. J. Softw. Tools Technol. Transf. 8, 621\u2013632 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"6","key":"793_CR44","doi-asserted-by":"publisher","DOI":"10.3390\/s18061888","volume":"18","author":"I. You","year":"2018","unstructured":"You, I., Kwon, S., Choudhary, G., Sharma, V., Seo, J.T.: An enhanced LoRaWAN security protocol for privacy preservation in IoT with a case study on a smart factory-enabled parking system. Sensors 18(6), 1888 (2018)","journal-title":"Sensors"},{"issue":"2","key":"793_CR45","doi-asserted-by":"publisher","first-page":"1131","DOI":"10.1109\/JIOT.2018.2805696","volume":"5","author":"Y. Qiu","year":"2018","unstructured":"Qiu, Y., Ma, M.: Secure group mobility support for 6LoWPAN networks. IEEE Internet Things J. 5(2), 1131\u20131141 (2018)","journal-title":"IEEE Internet Things J."},{"issue":"7","key":"793_CR46","doi-asserted-by":"publisher","DOI":"10.1002\/smr.2384","volume":"35","author":"Y. Fei","year":"2023","unstructured":"Fei, Y., Zhu, H., Yin, J.: Modeling and verifying NLSR protocol of NDN for CPS using UPPAAL. J. Softw. Evol. Process 35(7), 2384 (2023)","journal-title":"J. Softw. Evol. Process"},{"issue":"2","key":"793_CR47","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/0304-3975(94)00171-E","volume":"138","author":"G. Lowe","year":"1995","unstructured":"Lowe, G.: Probabilistic and prioritized models of timed CSP. Theor. Comput. Sci. 138(2), 315\u2013352 (1995)","journal-title":"Theor. Comput. Sci."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-025-00793-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-025-00793-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-025-00793-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,26]],"date-time":"2025-05-26T08:04:22Z","timestamp":1748246662000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-025-00793-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2]]},"references-count":47,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,2]]}},"alternative-id":["793"],"URL":"https:\/\/doi.org\/10.1007\/s10009-025-00793-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,2]]},"assertion":[{"value":"4 April 2025","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 April 2025","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}