{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T10:10:08Z","timestamp":1767262208427},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T00:00:00Z","timestamp":1683331200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T00:00:00Z","timestamp":1683331200000},"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":["J Reliable Intell Environ"],"published-print":{"date-parts":[[2024,3]]},"DOI":"10.1007\/s40860-023-00202-y","type":"journal-article","created":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T13:01:40Z","timestamp":1683378100000},"page":"73-91","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Formal verification for security and attacks in IoT physical layer"],"prefix":"10.1007","volume":"10","author":[{"given":"Zinah Hussein","family":"Toman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lazhar","family":"Hamel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sarah Hussein","family":"Toman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Graiet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dalton C\u00e9zane Gomes","family":"Valadares","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,5,6]]},"reference":[{"issue":"4","key":"202_CR1","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1109\/LCOMM.2011.022411.110120","volume":"15","author":"H Ning","year":"2011","unstructured":"Ning H, Wang Z (2011) Future internet of things architecture: like mankind neural system or social organization framework? IEEE Commun Lett 15(4):461\u2013463","journal-title":"IEEE Commun Lett"},{"issue":"2","key":"202_CR2","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/s10796-009-9218-4","volume":"13","author":"TS L\u00f3pez","year":"2011","unstructured":"L\u00f3pez TS, Ranasinghe DC, Patkai B, McFarlane D (2011) Taxonomy, technology and applications of smart objects. Inf Syst Front 13(2):281\u2013300","journal-title":"Inf Syst Front"},{"issue":"4","key":"202_CR3","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1049\/trit.2018.1008","volume":"3","author":"A Ghosh","year":"2018","unstructured":"Ghosh A, Chakraborty D, Law A (2018) Artificial intelligence in Internet of things. CAAI Trans Intell Technol 3(4):208\u2013218","journal-title":"CAAI Trans Intell Technol"},{"key":"202_CR4","doi-asserted-by":"publisher","DOI":"10.1016\/j.iot.2020.100240","volume":"11","author":"S Rizvi","year":"2020","unstructured":"Rizvi S, Pipetti R, McIntyre N, Todd J, Williams I (2020) Threat model for securing internet of things (IoT) network at device-level. Internet Things 11:100240","journal-title":"Internet Things"},{"issue":"2","key":"202_CR5","doi-asserted-by":"publisher","first-page":"1773","DOI":"10.1109\/COMST.2018.2878035","volume":"21","author":"JM Hamamreh","year":"2018","unstructured":"Hamamreh JM, Furqan HM, Arslan H (2018) Classifications and applications of physical layer security techniques for confidentiality: a comprehensive survey. IEEE Commun Surv Tutor 21(2):1773\u20131828","journal-title":"IEEE Commun Surv Tutor"},{"key":"202_CR6","doi-asserted-by":"crossref","unstructured":"Shakiba-Herfeh M, Chorti A, Poor HV (2021) Physical layer security: authentication, integrity, and confidentiality. In: Physical layer security. Springer, Cham, pp 129\u2013150","DOI":"10.1007\/978-3-030-55366-1_6"},{"key":"202_CR7","doi-asserted-by":"publisher","first-page":"54508","DOI":"10.1109\/ACCESS.2019.2913438","volume":"7","author":"D Wang","year":"2019","unstructured":"Wang D, Bai B, Lei K, Zhao W, Yang Y, Han Z (2019) Enhancing information security via physical layer approaches in heterogeneous IoT with multiple access mobile edge computing in smart city. IEEE Access 7:54508\u201354521","journal-title":"IEEE Access"},{"issue":"2","key":"202_CR8","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1109\/MCE.2019.2953740","volume":"9","author":"T Alladi","year":"2020","unstructured":"Alladi T, Chamola V, Sikdar B, Choo KKR (2020) Consumer IoT: security vulnerability case studies and solutions. IEEE Consumer Electron Mag 9(2):17\u201325","journal-title":"IEEE Consumer Electron Mag"},{"issue":"5","key":"202_CR9","doi-asserted-by":"publisher","first-page":"8169","DOI":"10.1109\/JIOT.2019.2927379","volume":"6","author":"N Wang","year":"2019","unstructured":"Wang N, Wang P, Alipour-Fanid A, Jiao L, Zeng K (2019) Physical-layer security of 5G wireless networks for IoT: challenges and opportunities. IEEE Internet Things J 6(5):8169\u20138181","journal-title":"IEEE Internet Things J"},{"key":"202_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/j.eti.2020.101091","volume":"20","author":"F Ullah","year":"2020","unstructured":"Ullah F, Al-Turjman F, Nayyar A (2020) IoT-based green city architecture using secured and sustainable android services. Environ Technol Innov 20:101091","journal-title":"Environ Technol Innov"},{"key":"202_CR11","doi-asserted-by":"crossref","unstructured":"Keerthi K, Roy I, Hazra A, Rebeiro C (2019) Formal verification for security in IoT devices. Security and Fault Tolerance in Internet of Things, pp 179\u2013200","DOI":"10.1007\/978-3-030-02807-7_9"},{"issue":"1","key":"202_CR12","doi-asserted-by":"publisher","first-page":"1985","DOI":"10.1007\/s10586-017-1107-x","volume":"22","author":"WS Bae","year":"2019","unstructured":"Bae WS (2019) Verifying a secure authentication protocol for IoT medical devices. Clust Comput 22(1):1985\u20131990","journal-title":"Clust Comput"},{"issue":"5","key":"202_CR13","doi-asserted-by":"publisher","first-page":"705","DOI":"10.1007\/s12652-016-0371-6","volume":"7","author":"V Desnitsky","year":"2016","unstructured":"Desnitsky V, Kotenko I (2016) Automated design, verification and testing of secure systems with embedded devices based on elicitation of expert knowledge. J Ambient Intell Humaniz Comput 7(5):705\u2013719","journal-title":"J Ambient Intell Humaniz Comput"},{"key":"202_CR14","doi-asserted-by":"crossref","unstructured":"Kamm\u00fcller F (2017) Formal modeling and analysis with humans in infrastructures for iot health care systems. In: International conference on human aspects of information security, privacy, and trust. Springer, Cham, pp 339\u2013352","DOI":"10.1007\/978-3-319-58460-7_24"},{"key":"202_CR15","doi-asserted-by":"crossref","unstructured":"Kamm\u00fcller F (2017) Human centric security and privacy for the iot using formal techniques. In: International conference on applied human factors and ergonomics. Springer, Cham, pp 106\u2013116","DOI":"10.1007\/978-3-319-60585-2_12"},{"issue":"16","key":"202_CR16","doi-asserted-by":"publisher","DOI":"10.1002\/dac.3323","volume":"30","author":"PK Dhillon","year":"2017","unstructured":"Dhillon PK, Kalra S (2017) Secure multi-factor remote user authentication scheme for Internet of Things environments. Int J Commun Syst 30(16):e3323","journal-title":"Int J Commun Syst"},{"key":"202_CR17","doi-asserted-by":"crossref","unstructured":"Drozdov D, Patil S, Dubinin V, Vyatkin V (2017) Towards formal verification for cyber-physically agnostic software: a case study. In: IECON 2017\u201343rd annual conference of the IEEE industrial electronics society. IEEE, pp 5509\u20135514","DOI":"10.1109\/IECON.2017.8216953"},{"key":"202_CR18","doi-asserted-by":"crossref","unstructured":"Kim H, Kang E, Lee EA, Broman D (2017) A toolkit for construction of authorization service infrastructure for the internet of things. In: Proceedings of the second international conference on Internet-of-Things design and implementation, pp 147\u2013158","DOI":"10.1145\/3054977.3054980"},{"key":"202_CR19","doi-asserted-by":"publisher","first-page":"5494","DOI":"10.1109\/ACCESS.2017.2696031","volume":"5","author":"M Mohsin","year":"2017","unstructured":"Mohsin M, Sardar MU, Hasan O, Anwar Z (2017) IoTRiskAnalyzer: a probabilistic model checking based framework for formal risk analytics of the Internet of Things. IEEE Access 5:5494\u20135505","journal-title":"IEEE Access"},{"key":"202_CR20","doi-asserted-by":"crossref","unstructured":"Kars P (1998) Formal methods in the design of a storm surge barrier control system. In: Lectures on embedded systems, European educational forum, school on embedded systems. Springer, London, pp 353\u2013367","DOI":"10.1007\/3-540-65193-4_28"},{"key":"202_CR21","doi-asserted-by":"publisher","first-page":"27132","DOI":"10.1109\/ACCESS.2017.2766180","volume":"5","author":"S Zahra","year":"2017","unstructured":"Zahra S, Alam M, Javaid Q, Wahid A, Javaid N, Malik SUR, Khan MK (2017) Fog computing over IoT: a secure deployment and formal verification. IEEE Access 5:27132\u201327144","journal-title":"IEEE Access"},{"issue":"7","key":"202_CR22","doi-asserted-by":"publisher","first-page":"1645","DOI":"10.1016\/j.future.2013.01.010","volume":"29","author":"J Gubbi","year":"2013","unstructured":"Gubbi J, Buyya R, Marusic S, Palaniswami M (2013) Internet of Things(IoT): a vision, architectural elements, and future directions. Futur Gener Comput Syst 29(7):1645\u20131660","journal-title":"Futur Gener Comput Syst"},{"issue":"1","key":"202_CR23","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1109\/MS.2016.20","volume":"33","author":"M Weyrich","year":"2015","unstructured":"Weyrich M, Ebert C (2015) Reference architectures for the internet of things. IEEE Softw 33(1):112\u2013116","journal-title":"IEEE Softw"},{"key":"202_CR24","doi-asserted-by":"crossref","unstructured":"Zhang AL (2016) Research on the architecture of internet of things applied in coal mine. In: 2016 International conference on information system and Artificial Intelligence (ISAI). IEEE, pp 21\u201323","DOI":"10.1109\/ISAI.2016.0014"},{"issue":"9","key":"202_CR25","doi-asserted-by":"publisher","first-page":"9001","DOI":"10.1109\/JIOT.2020.3001597","volume":"7","author":"N Zhang","year":"2020","unstructured":"Zhang N, Fang X, Wang Y, Wu S, Wu H, Kar D, Zhang H (2020) Physical-layer authentication for internet of things via wfrft-based gaussian tag embedding. IEEE Internet Things J 7(9):9001\u20139010","journal-title":"IEEE Internet Things J"},{"issue":"1","key":"202_CR26","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1109\/JIOT.2018.2864168","volume":"6","author":"C Li","year":"2018","unstructured":"Li C, Palanisamy B (2018) Privacy in internet of things: from principles to technologies. IEEE Internet Things J 6(1):488\u2013505","journal-title":"IEEE Internet Things J"},{"issue":"3","key":"202_CR27","doi-asserted-by":"publisher","first-page":"817","DOI":"10.3390\/s18030817","volume":"18","author":"B Ali","year":"2018","unstructured":"Ali B, Awad AI (2018) Cyber and physical security vulnerability assessment for IoT-based smart homes. Sensors 18(3):817","journal-title":"Sensors"},{"issue":"1","key":"202_CR28","doi-asserted-by":"publisher","DOI":"10.1002\/dac.4174","volume":"33","author":"X Li","year":"2020","unstructured":"Li X, Luo C, Ji H, Zhuang Y, Zhang H, Leung VC (2020) Energy consumption optimization for self-powered IoT networks with non-orthogonal multiple access. Int J Commun Syst 33(1):e4174","journal-title":"Int J Commun Syst"},{"issue":"833\u2013848","key":"202_CR29","first-page":"4","volume":"93","author":"S Debroy","year":"2019","unstructured":"Debroy S, Samanta P, Bashir A, Chatterjee M (2019) SpEED-IoT: spectrum aware energy efficient routing for device-to-device IoT communication. Futur Gener Comput Syst 93(833\u2013848):4","journal-title":"Futur Gener Comput Syst"},{"issue":"3","key":"202_CR30","doi-asserted-by":"publisher","first-page":"2120","DOI":"10.1109\/JIOT.2018.2825098","volume":"5","author":"T Xu","year":"2018","unstructured":"Xu T, Darwazeh I (2018) Non-orthogonal narrowband Internet of Things: a design for saving bandwidth and doubling the number of connected devices. IEEE Internet Things J 5(3):2120\u20132129","journal-title":"IEEE Internet Things J"},{"issue":"9","key":"202_CR31","first-page":"1227","volume":"9","author":"SOM Kamel","year":"2018","unstructured":"Kamel SOM, Hegazi NH (2018) A proposed model of IoT security management system based on a study of internet of things (IoT) security. Int J Sci Eng Res 9(9):1227\u20131244","journal-title":"Int J Sci Eng Res"},{"key":"202_CR32","doi-asserted-by":"publisher","DOI":"10.1016\/j.asoc.2021.107806","volume":"111","author":"C Greco","year":"2021","unstructured":"Greco C, Pace P, Basagni S, Fortino G (2021) Jamming detection at the edge of drone networks using Multi-layer Perceptrons and Decision Trees. Appl Soft Comput 111:107806","journal-title":"Appl Soft Comput"},{"key":"202_CR33","doi-asserted-by":"crossref","unstructured":"Chi Z, Li Y, Liu X, Wang W, Yao Y, Zhu T, Zhang Y (2020) Countering cross-technology jamming attack. In: Proceedings of the 13th ACM conference on security and privacy in wireless and mobile networks, pp 99\u2013110","DOI":"10.1145\/3395351.3399367"},{"key":"202_CR34","doi-asserted-by":"crossref","unstructured":"Yousefnezhad N, Madhikermi M, Fr\u00e4mling K (2018) Medi: measurement-based device identification framework for internet of things. In: 2018 IEEE 16th international conference on industrial informatics (INDIN). IEEE, pp 95\u2013100","DOI":"10.1109\/INDIN.2018.8472080"},{"key":"202_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.imavis.2018.04.007","volume":"77","author":"Z Boulkenafet","year":"2018","unstructured":"Boulkenafet Z, Komulainen J, Hadid A (2018) On the generalization of color texture-based face anti-spoofing. Image Vis Comput 77:1\u20139","journal-title":"Image Vis Comput"},{"key":"202_CR36","doi-asserted-by":"crossref","unstructured":"Farhin F, Sultana I, Islam N, Kaiser MS, Rahman MS, Mahmud M (2020) Attack detection in internet of things using software defined network and fuzzy neural network. In: 2020 joint 9th international conference on informatics, electronics & vision (ICIEV) and 2020 4th international conference on imaging, vision & pattern recognition (icIVPR). IEEE, pp 1\u20136","DOI":"10.1109\/ICIEVicIVPR48672.2020.9306666"},{"key":"202_CR37","unstructured":"Hoang TS (2013) An introduction to the Event-B modelling method. Ind Deploy Syst Eng Methods 211\u2013236"},{"key":"202_CR38","doi-asserted-by":"crossref","unstructured":"Craigen D (1999) Formal methods adoption: what\u2019s working, what\u2019s not! In: Proceedings of the 5th and 6th international SPIN workshops on theoretical and practical aspects of SPIN model checking. Springer, London, pp 77\u201391","DOI":"10.1007\/3-540-48234-2_6"},{"issue":"1","key":"202_CR39","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s100090100063","volume":"4","author":"C Eisner","year":"2002","unstructured":"Eisner C (2002) Using symbolic CTL model checking to verify the railway stations of Hoorn- Kersenboogerd and Heerhugowaard. Int J Softw Tools Technol Transf 4(1):107\u2013124","journal-title":"Int J Softw Tools Technol Transf"},{"key":"202_CR40","doi-asserted-by":"crossref","unstructured":"Damchoom K, Butler M, Abrial JR (2008) Modelling and proof of a tree-structured file system in Event-B and Rodin. In: International conference on formal engineering methods. Springer, Berlin, Heidelberg, pp 25\u201344","DOI":"10.1007\/978-3-540-88194-0_5"},{"issue":"8","key":"202_CR41","doi-asserted-by":"publisher","first-page":"8229","DOI":"10.1007\/s12652-020-02557-z","volume":"12","author":"G Orsini","year":"2021","unstructured":"Orsini G, Posdorfer W, Lamersdorf W (2021) Saving bandwidth and energy of mobile and IoT devices with link predictions. J Ambient Intell Humaniz Comput 12(8):8229\u20138240","journal-title":"J Ambient Intell Humaniz Comput"},{"key":"202_CR42","unstructured":"Prieto MD, Mart\u00ednez B, Monton M, Guillen IV, Guillen XV, Moreno JA (2014) Balancing power consumption in IoT devices by using variable packet size. In: 2014 eighth international conference on complex, intelligent and software intensive systems. IEEE, pp 170\u2013176"},{"key":"202_CR43","unstructured":"Aravindh G, Kowshik A. Speed detection using IOT. Int J Comput Appl 975:8887"},{"key":"202_CR44","doi-asserted-by":"crossref","unstructured":"Muankid A, Ketcham M (2019) The real-time electrocardiogram signal monitoring system in wireless sensor network. Int J Online Biomed Eng 15(2)","DOI":"10.3991\/ijoe.v15i02.9422"},{"key":"202_CR45","doi-asserted-by":"crossref","unstructured":"Gusev M, Poposka L, Spasevski G, Kostoska M, Koteska B, Simjanoska M, Trontelj J (2020) Noninvasive glucose measurement using machine learning and neural network methods and correlation with heart rate variability. J Sensors 2020","DOI":"10.1155\/2020\/9628281"},{"key":"202_CR46","doi-asserted-by":"crossref","unstructured":"Georgiades G, Papageorgiou XS, Loizou SG (2019) Integrated forest monitoring system for early fire detection and assessment. In: 2019 6th international conference on control, decision and information technologies (CoDIT). IEEE, pp 1817\u20131822","DOI":"10.1109\/CoDIT.2019.8820548"},{"key":"202_CR47","doi-asserted-by":"crossref","unstructured":"Leuschel M, Butler M (2013) ProB: A model checker for B. In: International symposium of formal methods Europe. Springer, Berlin, Heidelberg, pp 855\u2013874","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"202_CR48","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10009-009-0109-2","volume":"11","author":"Y Ait-Ameur","year":"2009","unstructured":"Ait-Ameur Y, Baron M, Kamel N, Mota JM (2009) Encoding a process algebra using the Event B method: application to the validation of human\u2013computer interactions. Int J Softw Tools Technol Transfer 11:239\u2013253","journal-title":"Int J Softw Tools Technol Transfer"},{"issue":"6","key":"202_CR49","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial JR, Butler M, Hallerstede S, Hoang TS, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in Event-B. Int J Softw Tools Technol Transfer 12(6):447\u2013466","journal-title":"Int J Softw Tools Technol Transfer"}],"container-title":["Journal of Reliable Intelligent Environments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s40860-023-00202-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s40860-023-00202-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s40860-023-00202-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,10]],"date-time":"2024-03-10T18:17:10Z","timestamp":1710094630000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s40860-023-00202-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,6]]},"references-count":49,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3]]}},"alternative-id":["202"],"URL":"https:\/\/doi.org\/10.1007\/s40860-023-00202-y","relation":{},"ISSN":["2199-4668","2199-4676"],"issn-type":[{"value":"2199-4668","type":"print"},{"value":"2199-4676","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,5,6]]},"assertion":[{"value":"23 June 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 March 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 May 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"On behalf of all authors, the corresponding author states that there is no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}