{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T02:59:26Z","timestamp":1763348366579,"version":"3.37.3"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2021,8,6]],"date-time":"2021-08-06T00:00:00Z","timestamp":1628208000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,8,6]],"date-time":"2021-08-06T00:00:00Z","timestamp":1628208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100007514","name":"Universit\u00e0 di Pisa","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100007514","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Comput Virol Hack Tech"],"published-print":{"date-parts":[[2021,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>When designing Wireless Sensor Networks it is important to analyze their security risks and provide adequate solutions for protecting them from malicious attacks. Unfortunately, perfect security cannot be achieved, for performance reasons. Therefore, designers have to devise security priorities, and select security mechanisms accordingly. However, in the early stages of the design process, the concrete effects of security attacks on the system may not be clearly identified. In this paper, we propose a framework that integrates formal verification and network simulation for enabling designers to evaluate the effects of attacks, identify possible security mechanisms, and evaluate their effectiveness, since design time. Formal methods are used to build the abstract model of the application, together with a set of attacks, and to state properties of general validity. The simulator measures the impact of the attacks in terms of common network parameters, like energy consumption or computational effort. Such information can be used to select adequate security mechanisms, then the initial abstract model can be refined to adopt them, and finally prove that former system properties are still verified. The framework relies on UPPAAL for formal modeling and verification and uses the Attack Simulation Framework on top of Castalia as a network simulator. As proof of concept, a case study is shown.\n<\/jats:p>","DOI":"10.1007\/s11416-021-00392-0","type":"journal-article","created":{"date-parts":[[2021,8,6]],"date-time":"2021-08-06T07:03:15Z","timestamp":1628233395000},"page":"249-263","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A framework for formal analysis and simulative evaluation of security attacks in wireless sensor networks"],"prefix":"10.1007","volume":"17","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1604-4465","authenticated-orcid":false,"given":"Cinzia","family":"Bernardeschi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6029-5467","authenticated-orcid":false,"given":"Gianluca","family":"Dini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6177-0928","authenticated-orcid":false,"given":"Maurizio","family":"Palmieri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0452-5010","authenticated-orcid":false,"given":"Francesco","family":"Racciatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,8,6]]},"reference":[{"issue":"2","key":"392_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"392_CR2","unstructured":"Boulis, A., Pediaditakis, D.: Castalia - A simulator for Wireless Sensor Networks and Body Area Networks, version 3.3, User\u2019s Manual (2013). https:\/\/github.com\/boulis\/Castalia\/blob\/master\/ Castalia"},{"key":"392_CR3","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A Tutorial on UPPAAL 4.0 (2006). http:\/\/www.it.uu.se\/research\/group\/darts\/papers\/texts\/new-tutorial.pdf"},{"key":"392_CR4","doi-asserted-by":"crossref","unstructured":"Bernardeschi, C., Masci, P., Pfeifer, H.: Early prototyping of wireless sensor network algorithms in PVS. In: Computer Safety, Reliability, and Security, 27th International Conference, pp. 346\u2013359 (2008)","DOI":"10.1007\/978-3-540-87698-4_29"},{"key":"392_CR5","doi-asserted-by":"crossref","unstructured":"Bernardeschi, C., Masci, P., Pfeifer, H.: Analysis of wireless sensor network protocols in dynamic scenarios. In: Stabilization, Safety, and Security of Distributed Systems, 11th International Symposium, pp. 105\u2013119 (2009)","DOI":"10.1007\/978-3-642-05118-0_8"},{"issue":"2","key":"392_CR6","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1109\/32.988495","volume":"28","author":"K Bhargavan","year":"2002","unstructured":"Bhargavan, K., Gunter, C., Lee, I., Sokolsky, O., Kim, M., Obradovic, D., Viswanathan, M.: Verisim: formal analysis of network simulations. IEEE Trans. Softw. Eng. 28(2), 129\u2013145 (2002)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"392_CR7","doi-asserted-by":"publisher","first-page":"2037","DOI":"10.1007\/s11277-017-4962-0","volume":"98","author":"B Bhushan","year":"2018","unstructured":"Bhushan, B., Sahoo, G.: Recent advances in attacks, technical challenges, vulnerabilities and their countermeasures in wireless sensor networks. Wireless Personal Commun. 98(2), 2037\u20132077 (2018)","journal-title":"Wireless Personal Commun."},{"key":"392_CR8","doi-asserted-by":"crossref","unstructured":"Bolton, C., Lowe, G.: Analyses of the reverse path forwarding routing algorithm. In: Intl. Conf. on Dependable Systems and Networks Proceedings, pp. 485\u2013494. IEEE Computer Society (2004)","DOI":"10.1109\/DSN.2004.1311918"},{"key":"392_CR9","first-page":"155","volume":"4","author":"J Buck","year":"1994","unstructured":"Buck, J., Ha, S., Lee, E.A., Messerschmitt, D.G.: Ptolemy: a framework for simulating and prototyping heterogeneous systems. Int. J. Comput. Simulat. 4, 155\u2013182 (1994)","journal-title":"Int. J. Comput. Simulat."},{"issue":"8","key":"392_CR10","doi-asserted-by":"publisher","first-page":"1434","DOI":"10.1016\/j.adhoc.2009.04.012","volume":"7","author":"AA Cardenas","year":"2009","unstructured":"Cardenas, A.A., Roosta, T., Sastry, S.: Rethinking security properties, threat models, and the design space in sensor networks: a case study in scada systems. Ad Hoc Netw. 7(8), 1434\u20131447 (2009)","journal-title":"Ad Hoc Netw."},{"key":"392_CR11","doi-asserted-by":"crossref","unstructured":"Dini, G., Tiloca, M.: Asf: An attack simulation framework for wireless sensor networks. 2012 IEEE 8th International Conference on Wireless and Mobile Computing, Networking and Communications (WiMob) pp. 203\u2013210 (2012)","DOI":"10.1109\/WiMOB.2012.6379077"},{"key":"392_CR12","doi-asserted-by":"crossref","unstructured":"Dini, G., Tiloca, M.: On simulative analysis of attack impact in wireless sensor networks. In: 2013 IEEE 18th Conference on Emerging Technologies Factory Automation (ETFA), pp. 1\u20138 (2013)","DOI":"10.1109\/ETFA.2013.6648059"},{"key":"392_CR13","doi-asserted-by":"crossref","unstructured":"Fatima, T., Saghar, K., Ihsan, A.: Evaluation of model checkers SPIN and UPPAAL for testing wireless sensor network routing protocols. In: 2015 12th International Bhurban Conference on Applied Sciences and Technology (IBCAST), pp. 263\u2013267 (2015)","DOI":"10.1109\/IBCAST.2015.7058514"},{"key":"392_CR14","doi-asserted-by":"crossref","unstructured":"Fonseca, J., Vieira, M.: A survey on secure software development lifecycles. In: Software Development Techniques for Constructive Information Systems Design, pp. 57\u201373. IGI Global (2013)","DOI":"10.4018\/978-1-4666-3679-8.ch003"},{"key":"392_CR15","doi-asserted-by":"crossref","unstructured":"Healy, M., Newe, T., Lewis, E.: Security for wireless sensor networks: A review. In: 2009 IEEE Sensors Applications Symposium, pp. 80\u201385 (2009)","DOI":"10.1109\/SAS.2009.4801782"},{"key":"392_CR16","doi-asserted-by":"crossref","unstructured":"Heinzelman, W., Kulik, J., Balakrishnan, H.: Adaptive protocols for information dissemination in wireless sensor networks. In: Proceedings of International Conference on Mobile Computing and Networking, pp. 174\u2013185. ACM (1999)","DOI":"10.1145\/313451.313529"},{"key":"392_CR17","unstructured":"Henderson, T., Riley, G., Floyd, S., Roy, S., et\u00a0al.: The NS Manual (2019)"},{"key":"392_CR18","doi-asserted-by":"publisher","first-page":"7047","DOI":"10.24297\/ijct.v16i7.6467","volume":"16","author":"A Hudaib","year":"2017","unstructured":"Hudaib, A., Alshraideh, M., Surakhi, O., Alkhanafseh, M.: A survey on design methods for secure software development. Int. J. Comput. Technol. 16, 7047\u20137064 (2017)","journal-title":"Int. J. Comput. Technol."},{"key":"392_CR19","doi-asserted-by":"crossref","unstructured":"Lazarescu, M.T., Lavagno, L.: Wireless Sensor Networks, pp. 1\u201342. Springer, Netherlands, Dordrecht (2017)","DOI":"10.1007\/978-94-017-7358-4_38-1"},{"key":"392_CR20","doi-asserted-by":"crossref","unstructured":"Mohammad, A., Alqatawna, J., Abushariah, M.: Secure software engineering: Evaluation of emerging trends. In: 2017 8th International Conference on Information Technology (ICIT), pp. 814\u2013818 (2017)","DOI":"10.1109\/ICITECH.2017.8079952"},{"key":"392_CR21","doi-asserted-by":"crossref","unstructured":"Nair, S., Cardell-Oliver, R.: Formal specification and analysis of performance variation in sensor network diffusion protocols. In: Symposium on Modeling, Analysis and Simulation of Wireless and Mobile Systems Proceedings, pp. 170\u2013173. ACM (2004)","DOI":"10.1145\/1023663.1023694"},{"key":"392_CR22","doi-asserted-by":"crossref","unstructured":"Rashid, A., Hasan, O., Saghar, K.: Formal analysis of a ZigBee-based routing protocol for smart grids using UPPAAL. In: 2015 12th International Conference on High-capacity Optical Networks and Enabling\/Emerging Technologies (HONET), pp. 1\u20135 (2015)","DOI":"10.1109\/HONET.2015.7395420"},{"key":"392_CR23","volume-title":"Threat Modeling: Designing for Security","author":"A Shostack","year":"2014","unstructured":"Shostack, A.: Threat Modeling: Designing for Security. Wiley, Hoboken (2014)"},{"key":"392_CR24","unstructured":"Varga, A.: OMNeT++ (2014). https:\/\/doc.omnetpp.org\/omnetpp4\/manual"}],"container-title":["Journal of Computer Virology and Hacking Techniques"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11416-021-00392-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11416-021-00392-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11416-021-00392-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,30]],"date-time":"2022-07-30T08:22:40Z","timestamp":1659169360000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11416-021-00392-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,6]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,9]]}},"alternative-id":["392"],"URL":"https:\/\/doi.org\/10.1007\/s11416-021-00392-0","relation":{},"ISSN":["2263-8733"],"issn-type":[{"type":"electronic","value":"2263-8733"}],"subject":[],"published":{"date-parts":[[2021,8,6]]},"assertion":[{"value":"2 August 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 July 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 August 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}