{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T15:52:04Z","timestamp":1778255524715,"version":"3.51.4"},"reference-count":47,"publisher":"MDPI AG","issue":"9","license":[{"start":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T00:00:00Z","timestamp":1619481600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sensors"],"abstract":"<jats:p>For many years various types of devices equipped with sensors have guaranteed proper work in a huge amount of machines and systems. For the proper operation of sensors, devices, and complex systems, we need secure communication. Security protocols (SP) in this case, guarantee the achievement of security goals. However, the design of SP is not an easy process. Sometimes SP cannot realise their security goals because of errors in their constructions and need to be investigated and verified in the case of their correctness. Now SP uses often time primitives due to the necessity of security dependence on the passing of time. In this work, we propose and investigate the SAT-and SMT-based formal verification methods of SP used in communication between devices equipped with sensors. For this, we use a formal model based on networks of communicating timed automata. Using this, we show how the security property of SP dedicated to the sensors world can be verified. In our work, we investigate such timed properties as delays in the network and lifetimes. The delay in the network is the lower time constraint related to sending the message. Lifetime is an upper constraint related to the validity of the timestamps generated for the transmitted messages.<\/jats:p>","DOI":"10.3390\/s21093055","type":"journal-article","created":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:18:20Z","timestamp":1619558300000},"page":"3055","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["SAT and SMT-Based Verification of Security Protocols Including Time Aspects"],"prefix":"10.3390","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1148-5691","authenticated-orcid":false,"given":"Sabina","family":"Szymoniak","sequence":"first","affiliation":[{"name":"Department of Computer Science, Czestochowa University of Technology, Dabrowskiego 73, 42-200 Czestochowa, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9820-6629","authenticated-orcid":false,"given":"Olga","family":"Siedlecka-Lamch","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Czestochowa University of Technology, Dabrowskiego 73, 42-200 Czestochowa, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9897-3561","authenticated-orcid":false,"given":"Agnieszka M.","family":"Zbrzezny","sequence":"additional","affiliation":[{"name":"Faculty of Mathematics and Computer Science, University of Warmia and Mazury, Sloneczna 54, 10-710 Olsztyn, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2771-9683","authenticated-orcid":false,"given":"Andrzej","family":"Zbrzezny","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, Jan Dlugosz University in Czestochowa, Armii Krajowej 13\/15, 42-200 Czestochowa, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0900-3243","authenticated-orcid":false,"given":"Miroslaw","family":"Kurkowski","sequence":"additional","affiliation":[{"name":"Institute of Computer Science, Cardinal St. Wyszynski University, Woycickiego 1\/3, 01-938 Warsaw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2021,4,27]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","unstructured":"Zeng, Y., Lin, M., Guo, S., Shen, Y., Cui, T., Wu, T., Zheng, Q., and Wang, Q. (2020). MultiFuzz: A Coverage-Based Multiparty-Protocol Fuzzer for IoT Publish\/Subscribe Protocols. Sensors, 20.","DOI":"10.3390\/s20185194"},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Mastilak, L., Galinski, M., Helebrandt, P., Kotuliak, I., and Ries, M. (2020). Enhancing Border Gateway Protocol Security Using Public Blockchain. Sensors, 20.","DOI":"10.3390\/s20164482"},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Moreno-Cruz, F., Toral-L\u00f3pez, V., Escobar-Molero, A., Ru\u00edz, V.U., Rivadeneyra, A., and Morales, D.P. (2020). treNch: Ultra-Low Power Wireless Communication Protocol for IoT and Energy Harvesting. Sensors, 20.","DOI":"10.3390\/s20216156"},{"key":"ref_4","doi-asserted-by":"crossref","unstructured":"Yu, D., Li, P., Chen, Y., Ma, Y., and Chen, J. (2020). A Time-efficient Multi-Protocol Probe Scheme for Fine-grain IoT Device Identification. Sensors, 20.","DOI":"10.3390\/s20071863"},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"Steingartner, W., Galinec, D., and Kozina, A. (2021). Threat Defense: Cyber Deception Approach and Education for Resilience in Hybrid Threats Model. Symmetry, 13.","DOI":"10.3390\/sym13040597"},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","article-title":"An Attack on the Needham-Schroeder Public-Key Authentication Protocol","volume":"56","author":"Lowe","year":"1995","journal-title":"Inf. Process. Lett."},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"Lowe, G. (1996). Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Springer.","DOI":"10.1007\/3-540-61042-1_43"},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1145\/77648.77649","article-title":"A Logic of Authentication","volume":"8","author":"Burrows","year":"1990","journal-title":"ACM Trans. Comput. Syst."},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., He\u00e1m, P.C., Kouchnarenko, O., and Mantovani, J. (2005). The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. Lecture Notes in Computer Science, Proceedings of the International Conference on Computer Aided Verification, Scotland, UK, 6\u201310 July 2005, Springer.","DOI":"10.1007\/11513988_27"},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Cremers, C., and Mauw, S. (2012). Operational Semantics and Verification of Security Protocols, Springer. Information Security and Cryptography.","DOI":"10.1007\/978-3-540-78636-8"},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1561\/3300000004","article-title":"Modeling and verifying security protocols with the applied Pi-Calculus and ProVerif","volume":"1","author":"Blanchet","year":"2016","journal-title":"Found. Trends Priv. Secur."},{"key":"ref_12","unstructured":"Kurkowski, M., and Penczek, W. (2016). Applying Timed Automata to Model Checking of Security Protocols. Handbook of Finite State Based Models and Applications, CRC Press."},{"key":"ref_13","unstructured":"M\u00f6dersheim, S., and Bruni, A. (2016, January 2\u20138). AIF-\u03c9: Set-Based Protocol Abstraction with Countable Families. Proceedings of the Principles of Security and Trust\u20145th International Conference, POST 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands."},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Basin, D.A., Cremers, C., and Meadows, C.A. (2018). Model Checking Security Protocols. Handbook of Model Checking, Springer.","DOI":"10.1007\/978-3-319-10575-8_22"},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"Hess, A.V., and M\u00f6dersheim, S. (2017, January 21\u201325). Formalizing and Proving a Typing Result for Security Protocols in Isabelle\/HOL. Proceedings of the 2017 IEEE 30th Computer Security Foundations Symposium (CSF), Santa Barbara, CA, USA.","DOI":"10.1109\/CSF.2017.27"},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Hess, A., and M\u00f6dersheim, S. (2018, January 9\u201312). A Typing Result for Stateful Protocols. Proceedings of the 2018 IEEE 31st Computer Security Foundations Symposium (CSF), Oxford, UK.","DOI":"10.1109\/CSF.2018.00034"},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"157185","DOI":"10.1109\/ACCESS.2019.2948922","article-title":"Multifactor Authentication Protocol in a Mobile Environment","volume":"7","author":"ElFray","year":"2019","journal-title":"IEEE Access"},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"203","DOI":"10.3233\/JCS-181139","article-title":"Secure authentication in the grid: A formal analysis of DNP3 SAv5","volume":"27","author":"Cremers","year":"2019","journal-title":"J. Comput. Secur."},{"key":"ref_19","unstructured":"Alur, R., and Dill, D.L. (1991, January 3\u20137). The Theory of Timed Automata. Proceedings of the Real-Time: Theory in Practice, REX Workshop, Mook, The Netherlands."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","article-title":"Specifying Real-Time Properties with Metric Temporal Logic","volume":"2","author":"Koymans","year":"1990","journal-title":"Real-Time Syst."},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Penczek, W., and P\u00f3lrola, A. (2006). Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach, Springer.","DOI":"10.1007\/978-3-540-32870-4"},{"key":"ref_22","first-page":"363","article-title":"Modelling and Checking Timed Authentication of Security Protocols","volume":"79","author":"Jakubowska","year":"2007","journal-title":"Fundam. Inform."},{"key":"ref_23","unstructured":"Kurkowski, M. (2013). Formalne Metody Weryfikacji W\u0142asno\u015bci Protoko\u0142\u00f3w Zabezpieczaj\u0105cych w Sieciach Komputerowych, Akademicka Oficyna Wydawnicza Exit. Informatyka-Akademicka Oficyna Wydawnicza EXIT."},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"127","DOI":"10.17512\/jamcm.2015.3.14","article-title":"Timed models of security protocols including delays in the network","volume":"14","author":"Szymoniak","year":"2015","journal-title":"J. Appl. Math. Comput. Mech."},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Szymoniak, S., Siedlecka-Lamch, O., and Kurkowski, M. (2017). Timed Analysis of Security Protocols. Information Systems Architecture and Technology: Proceedings of 37th International Conference on Information Systems Architecture and Technology\u2014ISAT 2016\u2014Part II, Springer International Publishing.","DOI":"10.1007\/978-3-319-46586-9_5"},{"key":"ref_26","unstructured":"Zbrzezny, A.M., Szymoniak, S., and Kurkowski, M. (2019, January 13\u201315). Efficient Verification of Security Protocols Time Properties Using SMT Solvers. Proceedings of the International Joint Conference: 12th International Conference on Computational Intelligence in Security for Information Systems (CISIS 2019) and 10th International Conference on EUropean Transnational Education (ICEUTE 2019), Seville, Spain."},{"key":"ref_27","unstructured":"Zbrzezny, A.M., Zbrzezny, A., Szymoniak, S., Siedlecka-Lamch, O., and Kurkowski, M. (2020, January 9\u201313). VerSecTis\u2014An Agent based Model Checker for Security Protocols. Proceedings of the 19th International Conference on Autonomous Agents and Multiagent Systems, AAMAS \u201920, Auckland, New Zealand."},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"366","DOI":"10.4304\/jcp.4.5.366-377","article-title":"TPMC: A Model Checker For Time-Sensitive Security Protocols","volume":"4","author":"Benerecetti","year":"2009","journal-title":"J. Comput."},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Szymoniak, S., Siedlecka-Lamch, O., and Kurkowski, M. (2018). On Some Time Aspects in Security Protocols Analysis. International Conference on Computer Networks, Springer.","DOI":"10.1007\/978-3-319-92459-5_28"},{"key":"ref_30","unstructured":"Szymoniak, S. (2018, January 19\u201322). The Impact of Time Parameters on the Security Protocols Correctness. Proceedings of the Computer Networks\u201425th International Conference, CN 2018, Gliwice, Poland."},{"key":"ref_31","unstructured":"Szymoniak, S. (2017). Modeling and Verification of Security Protocols Including Delays in the Network. [Ph.D. Thesis, Czestochowa University of Technology]."},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1109\/TSE.2017.2712621","article-title":"A Formal Specification and Verification Framework for Timed Security Protocols","volume":"44","author":"Li","year":"2018","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Tobarra, L., Cazorla, D., and Cuartero, F. (2007, January 8\u201311). Formal Analysis of Sensor Network Encryption Protocol (SNEP). Proceedings of the 2007 IEEE International Conference on Mobile Adhoc and Sensor Systems, Pisa, Italy.","DOI":"10.1109\/MOBHOC.2007.4428763"},{"key":"ref_34","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1145\/182110.182113","article-title":"A Lesson on Authentication Protocol Design","volume":"28","author":"Woo","year":"1994","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1023\/A:1016598314198","article-title":"SPINS: Security Protocols for Sensor Networks","volume":"8","author":"Perrig","year":"2002","journal-title":"Wirel. Netw."},{"key":"ref_36","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/978-3-540-68351-3_8","article-title":"The Salsa20 Family of Stream Ciphers","volume":"Volume 4986","author":"Robshaw","year":"2008","journal-title":"New Stream Cipher Designs\u2014The eSTREAM Finalists"},{"key":"ref_37","doi-asserted-by":"crossref","unstructured":"Lara, E., Aguilar, L., Garcia, J.A., and Sanchez, M.A. (2018). A Lightweight Cipher Based on Salsa20 for Resource-Constrained IoT Devices. Sensors, 18.","DOI":"10.3390\/s18103326"},{"key":"ref_38","doi-asserted-by":"crossref","unstructured":"Fukushima, K., Xu, R., Kiyomoto, S., and Homma, N. (2017, January 1\u20134). Fault Injection Attack on Salsa20 and ChaCha and a Lightweight Countermeasure. Proceedings of the 2017 IEEE Trustcom\/BigDataSE\/ICESS, Sydney, Australia.","DOI":"10.1109\/Trustcom\/BigDataSE\/ICESS.2017.348"},{"key":"ref_39","unstructured":"Baier, C., and Katoen, J.P. (2008). Principles of Model Checking, MIT Press."},{"key":"ref_40","first-page":"303","article-title":"SAT-Based Reachability Checking for Timed Automata with Diagonal Constraints","volume":"67","author":"Zbrzezny","year":"2005","journal-title":"Fundam. Inf."},{"key":"ref_41","doi-asserted-by":"crossref","unstructured":"Szymoniak, S. (2018). KaoChow Protocol Timed Analysis. International Multi-Conference on Advanced Computer Systems, Springer.","DOI":"10.1007\/978-3-030-03314-9_30"},{"key":"ref_42","doi-asserted-by":"crossref","first-page":"1136","DOI":"10.3934\/mbe.2021061","article-title":"Security protocols analysis including various time parameters","volume":"18","author":"Szymoniak","year":"2021","journal-title":"Math. Biosci. Eng."},{"key":"ref_43","first-page":"737","article-title":"Yices 2.2","volume":"Volume 8559","author":"Dutertre","year":"2014","journal-title":"Lecture Notes in Computer Science, Proceedings of the International Conference on Computer Aided Verification, Vienna, Austria, 18\u201322 July 2014"},{"key":"ref_44","doi-asserted-by":"crossref","first-page":"101965","DOI":"10.1016\/j.adhoc.2019.101965","article-title":"A secure and efficient three-factor multi-gateway authentication protocol for wireless sensor networks","volume":"95","author":"Guo","year":"2019","journal-title":"Ad Hoc Netw."},{"key":"ref_45","first-page":"102502","article-title":"A robust authentication and access control protocol for securing wireless healthcare sensor networks","volume":"52","author":"Ali","year":"2020","journal-title":"J. Inf. Secur. Appl."},{"key":"ref_46","unstructured":"Saeed, K., and Homenda, W. (2015). Verification of Mutual Authentication Protocol for MobInfoSec System. Lecture Notes in Computer Science, Proceedings of the Computer Information Systems and Industrial Management, Warsaw, Poland, 24\u201326 September 2015, Springer International Publishing."},{"key":"ref_47","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1109\/TMC.2006.16","article-title":"A study of the energy consumption characteristics of cryptographic algorithms and security protocols","volume":"5","author":"Potlapally","year":"2006","journal-title":"IEEE Trans. Mob. Comput."}],"container-title":["Sensors"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1424-8220\/21\/9\/3055\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T05:53:27Z","timestamp":1760162007000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1424-8220\/21\/9\/3055"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,27]]},"references-count":47,"journal-issue":{"issue":"9","published-online":{"date-parts":[[2021,5]]}},"alternative-id":["s21093055"],"URL":"https:\/\/doi.org\/10.3390\/s21093055","relation":{},"ISSN":["1424-8220"],"issn-type":[{"value":"1424-8220","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,4,27]]}}}