Formal security proofs for medical cryptographic protocols
*R. G. Hemanth KumarCorresponding authordrhemanthkumarrg@gmail.comDepartment of Forensic Medicine & ToxicologyKrishna Institute of Medical SciencesKrishna Vishwa Vidyapeeth (Deemed to be University)Karad, Maharashtra, 415539, IndiaView full profile → , Varun Kumar Sharmavarun1.sharma@niu.edu.inDepartment of Biotechnology and MicrobiologyNoida International UniversityGreater Noida, Uttar Pradesh, 201312, IndiaView full profile → , Saudagar Subhash Bardesaudagar.barde@vit.eduDepartment of Information TechnologyVishwakarma Institute of TechnologyPune, Maharashtra, 411037, IndiaView full profile → , Y. Vijay Kumarvijaykumar@outlook.comDepartment of Electronics & Communication EngineeringPragati Engineering CollegeKakinada, Andhra Pradesh, 533437, IndiaView full profile → , C. Kavithakavitha1616@vardhaman.orgDepartment of Computer Science and EngineeringVardhaman College of EngineeringShamshabad, Hyderabad, Telangana, 501218, IndiaView full profile → , Ponmurugan Panneerselvamponmurugan@maher.ac.inDepartment of ResearchMeenakshi Academy of Higher Education & ResearchChennai, Tamil Nadu, 600087, IndiaView full profile →
* Corresponding author · click or hover a name for details
- Received:
- 01 Mar 2026
- Published Online:
- 31 Oct 2026
- Article type:
- Research Article
- Language:
- EN
- Article no.:
- JIOS-2500
- Pages:
- 3753–3763
Abstract
Given the critical role of medical information in medical cryptographic processes, it is essential to have rigorous security validation to prevent any vulnerabilities in the authentication process that could lead to unauthorized access and access to clinical information and allow unauthorized treatment decisions to be made. This study introduces a formal security-proof framework to assess the security of authentication, confidentiality, integrity, anonymity and security of session-keys in connected healthcare settings. The proposed protocol uses finite field operations, cryptographic hashes, key derivation functions, random nonces, timestamps and medical professionals and patients. Adversarial games, mutual-authentication proofs, session-key indistinguishability and resistance to replay, impersonation, man-in-the-middle and privileged-insider attacks are discussed in the context of security. The formal reasoning approach has a negligible adversarial advantage, given the computational assumptions. Comparative evaluation shows the overhead of the authentication process is lower, but the protection of the medical devices is still high, even when considering the limited resources of medical devices. The framework provides a mathematically sound basis for designing reliable, private and effective healthcare communication systems in a heterogeneous clinical network and infrastructure.
Keywords
Subject Classifications
References
[1] D. G. Duguma, I. You, Y. E. Gebremariam, and J. Kim, “Can formal security verification really be optional? Scrutinizing the security of IMD authentication protocols,” Sensors, vol. 21, no. 24, Art. no. 8383 (2021), doi: 10.3390/s21248383.
[2] S. Lee, K. A. Kang, S. Lee, and J. Kim, “Exploring authentication protocols for secure and efficient Internet of Medical Things systems,” Electronics, vol. 14, no. 21, Art. no. 4164 (2025), doi: 10.3390/electronics14214164.
[3] J. Kim, J. Oh, D. Son, H. Kwon, P. V. Astillo, and I. You, “APSec1.0: Innovative security protocol design with formal security analysis for the artificial pancreas system,” Sensors, vol. 23, no. 12, Art. no. 5501 (2023), doi: 10.3390/s23125501.
[4] Z. Rajabinejad and S. M. Semnani, “Calculation and comparison of energy and energy based on Mostar index of the double-star graph and its line graph,” J. Discrete Math. Sci. Cryptogr., vol. 29, no. 4, pp. 1585–1594 (2025), doi: 10.47974/JDMSC-2246.
[5] H.-Y. Chen, Z.-Y. Wu, T.-L. Chen, Y.-M. Huang, and C.-H. Liu, “Security privacy and policy for cryptographic based electronic medical information system,” Sensors, vol. 21, no. 3, Art. no. 713 (2021), doi: 10.3390/s21030713.
[6] K. A. Delgado-Vargas, G. Gallegos-Garcia, and P. J. Escamilla-Ambrosio, “Cryptographic protocol with keyless sensors authentication for WBAN in healthcare applications,” Appl. Sci., vol. 13, no. 3, Art. no. 1675 (2023), doi: 10.3390/app13031675.
[7] N. J. Rad and R. Hasni, “Note on placement of security nodes in graphs associated to the Internet of Things,” J. Inf. Optim. Sci., vol. 47, no. 2, pp. 507–512 (2025), doi: 10.47974/JIOS-1572.
[8] X. Chen and H. Deng, “Efficient verification of cryptographic protocols with dynamic epistemic logic,” Appl. Sci., vol. 10, no. 18, Art. no. 6577 (2020), doi: 10.3390/app10186577.
[9] H. Lim, Y. Park, and Y. Park, “A PUF-based secure and lightweight authentication protocol for medical IoT environments,” Sensors, vol. 26, no. 10, Art. no. 3223 (2026), doi: 10.3390/s26103223.
[10] A. Singh, V. S. Sharma, S. Basheer, and C. L. Chowdhary, “A deep cryptographic framework for securing the healthcare network from penetration,” Sensors, vol. 24, no. 21, Art. no. 7089 (2024), doi: 10.3390/s24217089.
[11] M. Anagreh and P. Laud, “Security proof of single-source shortest distance protocols built on secure multiparty computation protocols,” Cryptography, vol. 9, no. 1, Art. no. 1 (2025), doi: 10.3390/cryptography9010001.
[12] A. Kilitçi Calayır and S. Alp, “A blockchain-based framework for privacy-preserving medical report sharing and diagnosis-free verification,” Appl. Sci., vol. 16, no. 13, Art. no. 6596 (2026), doi: 10.3390/app16136596.
[13] M. A. Khan, S. Ullah, T. Ahmad, K. Jawad, and A. Buriro, “Enhancing security and privacy in healthcare systems using a lightweight RFID protocol,” Sensors, vol. 23, no. 12, Art. no. 5518 (2023), doi: 10.3390/s23125518.
[14] S. Zhang, Y. Yin, N. Chen, and H. Ning, “A lightweight decentralized medical data sharing scheme with dual verification,” Cryptography, vol. 9, no. 4, Art. no. 69 (2025), doi: 10.3390/cryptography9040069.
[15] J. Piątkowski and S. Szymoniak, “Methodology of testing the security of cryptographic protocols using the CMMTree framework,” Appl. Sci., vol. 13, no. 23, Art. no. 12668 (2023), doi: 10.3390/app132312668.
