{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T02:38:41Z","timestamp":1760236721221,"version":"build-2065373602"},"reference-count":49,"publisher":"MDPI AG","issue":"24","license":[{"start":{"date-parts":[[2021,12,15]],"date-time":"2021-12-15T00:00:00Z","timestamp":1639526400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003725","name":"National Research Foundation of Korea","doi-asserted-by":"publisher","award":["NRF-2020R1I1A2073603"],"award-info":[{"award-number":["NRF-2020R1I1A2073603"]}],"id":[{"id":"10.13039\/501100003725","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sensors"],"abstract":"<jats:p>The need for continuous monitoring of physiological information of critical organs of the human body, combined with the ever-growing field of electronics and sensor technologies and the vast opportunities brought by 5G connectivity, have made implantable medical devices (IMDs) the most necessitated devices in the health arena. IMDs are very sensitive since they are implanted in the human body, and the patients depend on them for the proper functioning of their vital organs. Simultaneously, they are intrinsically vulnerable to several attacks mainly due to their resource limitations and the wireless channel utilized for data transmission. Hence, failing to secure them would put the patient\u2019s life in jeopardy and damage the reputations of the manufacturers. To date, various researchers have proposed different countermeasures to keep the confidentiality, integrity, and availability of IMD systems with privacy and safety specifications. Despite the appreciated efforts made by the research community, there are issues with these proposed solutions. Principally, there are at least three critical problems. (1) Inadequate essential capabilities (such as emergency authentication, key update mechanism, anonymity, and adaptability); (2) heavy computational and communication overheads; and (3) lack of rigorous formal security verification. Motivated by this, we have thoroughly analyzed the current IMD authentication protocols by utilizing two formal approaches: the Burrows\u2013Abadi\u2013Needham logic (BAN logic) and the Automated Validation of Internet Security Protocols and Applications (AVISPA). In addition, we compared these schemes against their security strengths, computational overheads, latency, and other vital features, such as emergency authentications, key update mechanisms, and adaptabilities.<\/jats:p>","DOI":"10.3390\/s21248383","type":"journal-article","created":{"date-parts":[[2021,12,15]],"date-time":"2021-12-15T21:47:36Z","timestamp":1639604856000},"page":"8383","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Can Formal Security Verification Really Be Optional? Scrutinizing the Security of IMD Authentication Protocols"],"prefix":"10.3390","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7121-4204","authenticated-orcid":false,"given":"Daniel Gerbi","family":"Duguma","sequence":"first","affiliation":[{"name":"Department of Information Security Engineering, Soonchunhyang University, Asan-si 31538, Choongchungnam-do, Korea"}]},{"given":"Ilsun","family":"You","sequence":"additional","affiliation":[{"name":"Department of ICT Environmental Health System, Soonchunhyang University, Asan-si 31538, Choongchungnam-do, Korea"}]},{"given":"Yonas Engida","family":"Gebremariam","sequence":"additional","affiliation":[{"name":"Department of ICT Environmental Health System, Soonchunhyang University, Asan-si 31538, Choongchungnam-do, Korea"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2710-0864","authenticated-orcid":false,"given":"Jiyoon","family":"Kim","sequence":"additional","affiliation":[{"name":"Department of Information Security Engineering, Soonchunhyang University, Asan-si 31538, Choongchungnam-do, Korea"}]}],"member":"1968","published-online":{"date-parts":[[2021,12,15]]},"reference":[{"key":"ref_1","unstructured":"Coherent Market Insights (2021, November 20). U.S. Implantable Medical Devices Market Analysis. Available online: https:\/\/www.coherentmarketinsights.com\/market-insight\/us-implantable-medical-devices-market-3853."},{"key":"ref_2","unstructured":"(2021, November 20). IMARC Implantable Medical Devices Market: Global Industry Trends, Share, Size, Growth, Opportunity and Forecast 2020\u20132025. Available online: https:\/\/www.imarcgroup.com\/implantable-medical-devices-market."},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Maddock, N.A., James, N.L., McKenzie, D.R., and Patrick, J.F. (2012). Technological advances for polymers in active implantable medical devices. The Design and Manufacture of Medical Devices, Elsevier.","DOI":"10.1533\/9781908818188.239"},{"key":"ref_4","first-page":"38","article-title":"Towards an Epidemic SMS-based Cellular Botnet","volume":"10","author":"Kitana","year":"2020","journal-title":"J. Internet Serv. Inf. Secur."},{"key":"ref_5","first-page":"55","article-title":"The use of mobile phones to monitor the status of patients with Parkinson\u2019s disease","volume":"11","author":"Shichkina","year":"2020","journal-title":"J. Wirel. Mob. Netw. Ubiquitous Comput. Dependable Appl."},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1016\/j.jbi.2015.04.007","article-title":"Security and privacy issues in implantable medical devices: A comprehensive survey","volume":"55","author":"Camara","year":"2015","journal-title":"J. Biomed. Inform."},{"key":"ref_7","first-page":"1","article-title":"Cost and Effectiveness of TrustZone Defense and Side-Channel Attack on ARM Platform","volume":"11","author":"Liu","year":"2020","journal-title":"J. Wirel. Mob. Netw. Ubiquitous Comput. Dependable Appl."},{"key":"ref_8","first-page":"49","article-title":"Detection and Classification of Radio Frequency Jamming Attacks using Machine learning","volume":"11","author":"Kasturi","year":"2020","journal-title":"J. Wirel. Mob. Netw. Ubiquitous Comput. Dependable Appl."},{"key":"ref_9","first-page":"16","article-title":"Location spoofing attack detection with pre-installed sensors in mobile devices","volume":"11","author":"Wong","year":"2020","journal-title":"J. Wirel. Mob. Netw. Ubiquitous Comput. Dependable Appl."},{"key":"ref_10","first-page":"47","article-title":"A Survey of Secure Internet of Things in Relation to Blockchain","volume":"10","author":"Alizadeh","year":"2020","journal-title":"J. Internet Serv. Inf. Secur."},{"key":"ref_11","first-page":"59","article-title":"Identification of device motion status via Bluetooth discovery","volume":"10","author":"Wong","year":"2020","journal-title":"J. Internet Serv. Inf. Secur."},{"key":"ref_12","doi-asserted-by":"crossref","unstructured":"Rushanan, M., Rubin, A.D., Kune, D.F., and Swanson, C.M. (2014, January 18\u201321). Sok: Security and privacy in implantable medical devices and body area networks. Proceedings of the 2014 IEEE Symposium on Security and Privacy, Berkeley, CA, USA.","DOI":"10.1109\/SP.2014.40"},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"147948","DOI":"10.1109\/ACCESS.2020.3015686","article-title":"Imdfence: Architecting a secure protocol for implantable medical devices","volume":"8","author":"Siddiqi","year":"2020","journal-title":"IEEE Access"},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Belkhouja, T., Sorour, S., and Hefeida, M.S. (2019, January 9\u201313). Role-Based Hierarchical Medical Data Encryption for Implantable Medical Devices. In Proceeding of the 2019 IEEE Global Communications Conference (GLOBECOM), Waikoloa, HI, USA.","DOI":"10.1109\/GLOBECOM38437.2019.9014192"},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"Tutari, V.H., Das, B., and Chowdhury, D.R. (2019, January 25\u201328). A Continuous Role-Based Authentication Scheme and Data Transmission Protocol for Implantable Medical Devices. Proceedings of the 2019 Second International Conference on Advanced Computational and Communication Paradigms (ICACCP), Gangtok, India.","DOI":"10.1109\/ICACCP.2019.8883012"},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"1126","DOI":"10.1109\/TETC.2020.2982461","article-title":"Access control for implantable medical devices","volume":"9","author":"Camara","year":"2020","journal-title":"IEEE Trans. Emerg. Top. Comput."},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Zhang, Z., Xu, X., Han, S., Liang, Y., and Liu, C. (2020, January 25\u201328). Wearable Proxy Device-Assisted Authentication Request Filtering for Implantable Medical Devices. Proceedings of the 2020 IEEE Wireless Communications and Networking Conference (WCNC), Seoul, Korea.","DOI":"10.1109\/WCNC45663.2020.9120856"},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"3763","DOI":"10.1109\/JBHI.2021.3063173","article-title":"TrMAps: Trust Management in Specification-based Misbehavior Detection System for IMD-Enabled Artificial Pancreas System","volume":"25","author":"Astillo","year":"2021","journal-title":"IEEE J. Biomed. Health Inform."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1016\/j.future.2021.10.023","article-title":"Federated intelligence of anomaly detection agent in IoTMD-enabled Diabetes Management Control System","volume":"128","author":"Astillo","year":"2021","journal-title":"Futur. Gener. Comput. Syst."},{"key":"ref_20","first-page":"3","article-title":"Why would we get attacked? An analysis of attacker\u2019s aims behind DDoS attacks","volume":"11","author":"Abhishta","year":"2020","journal-title":"J. Wirel. Mob. Netw. Ubiquitous Comput. Dependable Appl."},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1098\/rspa.1989.0125","article-title":"A logic of authentication","volume":"426","author":"Burrows","year":"1989","journal-title":"Proc. R. Soc. Lond. A. Math. Phys. Sci."},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cu\u00e9llar, J., Drielsma, P.H., H\u00e9am, P.-C., Kouchnarenko, O., and Mantovani, J. (2005). The AVISPA tool for the automated validation of internet security protocols and applications. International Conference on Computer Aided Verification, Springer.","DOI":"10.1007\/11513988_27"},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Khan, H., Dowling, B., and Martin, K.M. (2018, January 1\u20133). Highly efficient privacy-preserving key agreement for wireless body area Networks. Proceedings of the 2018 17th IEEE International Conference On Trust, Security And Privacy in Computing and Communications\/12th IEEE International Conference On Big Data Science And Engineering (TrustCom\/BigDataSE), New York, NY, USA.","DOI":"10.1109\/TrustCom\/BigDataSE.2018.00149"},{"key":"ref_24","unstructured":"Wu, L., Chi, H., and Du, X. (2018). A Secure Proxy-based Access Control Scheme for Implantable Medical Devices. arXiv, arXiv1803.07751."},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Chi, H., Wu, L., Du, X., Zeng, Q., and Ratazzi, P. (June, January 30). e-SAFE: Secure, efficient and forensics-enabled access to implantable medical devices. Proceedings of the 2018 IEEE Conference on Communications and Network Security (CNS), Beijing, China.","DOI":"10.1109\/CNS.2018.8433213"},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Parvez, K., Zohra, F.T., and Jahan, M. (2019, January 17\u201319). A secure and lightweight user authentication mechanism for wireless body area network. Proceedings of the 6th International Conference on Networking, Systems and Security, Dhaka, Bangladesh.","DOI":"10.1145\/3362966.3362981"},{"key":"ref_27","first-page":"180","article-title":"Efficient Key Agreement and Nodes Authentication Scheme for Body Sensor Networks","volume":"8","author":"Iqbal","year":"2017","journal-title":"Int. J. Adv. Comput. Sci. Appl."},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1109\/MCOM.2015.7010518","article-title":"Authentication protocol for an ambient assisted living system","volume":"53","author":"He","year":"2015","journal-title":"IEEE Commun. Mag."},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Ellouze, N., Allouche, M., Ben Ahmed, H., Rekhis, S., and Boudriga, N. (2013, January 4). Securing implantable cardiac medical devices: Use of radio frequency energy harvesting. Proceedings of the 3rd International Workshop on Trustworthy Embedded Devices, Berlin, Germany.","DOI":"10.1145\/2517300.2517307"},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Fu, C., Du, X., Wu, L., Zeng, Q., Mohamed, A., and Guizani, M. (2019). Poks based secure and energy-efficient access control for implantable medical devices. International Conference on Security and Privacy in Communication Systems, Springer.","DOI":"10.1007\/978-3-030-37228-6_6"},{"key":"ref_31","unstructured":"Antonescu, B., and Basagni, S. (October, January 30). Wireless body area networks: Challenges, trends and emerging technologies. Proceedings of the 8th International Conference on Body Area Networks, Boston, MA, USA."},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"2475","DOI":"10.1002\/sec.939","article-title":"Security of implantable medical devices: Limits, requirements, and proposals","volume":"7","author":"Ellouze","year":"2014","journal-title":"Secur. Commun. Netw."},{"key":"ref_33","doi-asserted-by":"crossref","first-page":"28889","DOI":"10.3390\/s151128889","article-title":"Power approaches for implantable medical devices","volume":"15","author":"Amar","year":"2015","journal-title":"Sensors"},{"key":"ref_34","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1016\/j.icte.2016.08.010","article-title":"Review of medical implant communication system (MICS) band and network","volume":"2","author":"Islam","year":"2016","journal-title":"ICT Express"},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1145\/2541228.2555313","article-title":"A system architecture, processor, and communication protocol for secure implants","volume":"10","author":"Strydis","year":"2013","journal-title":"ACM Trans. Archit. Code Optim."},{"key":"ref_36","doi-asserted-by":"crossref","first-page":"2590","DOI":"10.1109\/JSYST.2016.2544805","article-title":"Anonymous authentication for wireless body area networks with provable security","volume":"11","author":"He","year":"2016","journal-title":"IEEE Syst. J."},{"key":"ref_37","doi-asserted-by":"crossref","unstructured":"Halperin, D., Heydt-Benjamin, T.S., Ransford, B., Clark, S.S., Defend, B., Morgan, W., Fu, K., Kohno, T., and Maisel, W.H. (2008, January 18\u201322). Pacemakers and Implantable Cardiac Defibrillators: Software Radio Attacks and Zero-Power Defenses. Proceedings of the 2008 IEEE Symposium on Security and Privacy (SP 2008), Oakland, CA, USA.","DOI":"10.1109\/SP.2008.31"},{"key":"ref_38","doi-asserted-by":"crossref","unstructured":"Burleson, W., Clark, S.S., Ransford, B., and Fu, K. (2012, January 3\u20137). Design challenges for secure implantable medical devices. Proceedings of the DAC Design Automation Conference 2012, San Francisco, CA, USA.","DOI":"10.1145\/2228360.2228364"},{"key":"ref_39","doi-asserted-by":"crossref","first-page":"562","DOI":"10.1109\/JSEN.2016.2633973","article-title":"Ideas and challenges for securing wireless implantable medical devices: A review","volume":"17","author":"Zheng","year":"2016","journal-title":"IEEE Sens. J."},{"key":"ref_40","doi-asserted-by":"crossref","unstructured":"Gollakota, S., Hassanieh, H., Ransford, B., Katabi, D., and Fu, K. (2011, January 15\u201319). They can hear your heartbeats: Non-invasive security for implantable medical devices. Proceedings of the ACM SIGCOMM 2011 Conference, Toronto, ON, Canada.","DOI":"10.1145\/2018436.2018438"},{"key":"ref_41","doi-asserted-by":"crossref","unstructured":"Duguma, D.G., Kim, J., Kim, B., and You, I. (2020, January 12\u201315). A Formal Security Verification on He and Zeadally\u2019s Authentication Protocol for IMD-Enabled Ambient Assisted Living System. Proceedings of the 2020 ACM International Conference on Intelligent Computing and its Emerging Applications, GangWon, Korea.","DOI":"10.1145\/3440943.3444735"},{"key":"ref_42","doi-asserted-by":"crossref","unstructured":"Kim, J., Lee, S., Duguma, D.G., Kim, B., and You, I. (2020, January 12\u201315). Comments on\u201d Securing implantable cardiac medical devices\u201d Use of radio frequency energy harvesting. Proceedings of the 2020 ACM International Conference on Intelligent Computing and its Emerging Applications, GangWon, Korea.","DOI":"10.1145\/3440943.3444733"},{"key":"ref_43","unstructured":"Boyd, C., and Mao, W. (1993). On a Limitation of BAN Logic. Workshop on the Theory and Application of of Cryptographic Techniques, Springer."},{"key":"ref_44","unstructured":"Von Oheimb, D. (2005, January 12\u201315). The high-level protocol specification language HLPSL developed in the EU project AVISPA. Proceedings of the APPSEM 2005 Workshop, Frauenchiemsee, Germany."},{"key":"ref_45","doi-asserted-by":"crossref","first-page":"2736","DOI":"10.1109\/TII.2018.2808190","article-title":"Context-sensitive access in industrial internet of things (IIoT) healthcare applications","volume":"14","author":"Alturjman","year":"2018","journal-title":"IEEE Trans. Ind. Inform."},{"key":"ref_46","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1109\/MCE.2017.2720193","article-title":"Authentication protocols for implantable medical devices: Taxonomy, analysis and future directions","volume":"7","author":"Challa","year":"2017","journal-title":"IEEE Consum. Electron. Mag."},{"key":"ref_47","unstructured":"Saho, N.J.G., and Ezin, E.C. (October, January 22). Comparative Study on the Performance of Elliptic Curve Cryptography Algorithms with Cryptography through RSA Algorithm. Proceedings of the CARI 2020-Colloque Africain sur la Recherche en Informatique et en Math\u00e9matiques Apliqu\u00e9es, Thi\u00e8s, Senegal."},{"key":"ref_48","unstructured":"Fog, A. (2021, November 20). Instruction tables: Lists of Instruction latencies, Throughputs and Micro-Operation Breakdowns for Intel, AMD and VIA CPUs. Available online: https:\/\/www.agner.org\/optimize\/instruction_tables."},{"key":"ref_49","unstructured":"FM4DD (2021, November 20). X509 Certificate Examples for Testing and Verification. Available online: http:\/\/fm4dd.com\/openssl\/certexamples.htm."}],"container-title":["Sensors"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1424-8220\/21\/24\/8383\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T07:48:54Z","timestamp":1760168934000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1424-8220\/21\/24\/8383"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,15]]},"references-count":49,"journal-issue":{"issue":"24","published-online":{"date-parts":[[2021,12]]}},"alternative-id":["s21248383"],"URL":"https:\/\/doi.org\/10.3390\/s21248383","relation":{},"ISSN":["1424-8220"],"issn-type":[{"type":"electronic","value":"1424-8220"}],"subject":[],"published":{"date-parts":[[2021,12,15]]}}}