Energy-Conscious and Regulation-Ready Security Protocol for Wearable Medical Devices: From Formal Proofs to Deployment

Abstract

This paper introduces a formally verified, lightweight security protocol tailored for energy-constrained wearable medical devices operating in regulated healthcare environments. Designed to satisfy emerging cybersecurity mandates from HIPAA, GDPR, and Health Canada, the protocol incorporates Ed25519-based mutual authentication, ephemeral Curve25519 key exchange, and ChaCha20- Poly1305 authenticated encryption, providing in-transit protection across heterogeneous nodes with minimal computational and energy overhead. Formal verification through ProVerif and Scyther confirms strong resilience against key compromise, replay, and session confusion, with verified guarantees of end-to-end authentication, forward secrecy, nonce protection, and key integrity across multi-node interactions. To ensure practical feasibility, the protocol was validated through a dual-phase evaluation strategy. A Python-based simulation testbed enabled controlled symbolic testing, adversarial fault injection, and modular verification of cryptographic behavior and session dynamics. This was followed by real-world deployment on an STM32L431-powered ECG wearable, relayed through an Android node to a cloud server. Energy profiling with Nordic PPK2 measured only 7.91mWh of daily security overhead, under 16% of system budget, supporting 30+ days of secure operation per charge. The total system consumption ( 58mWh/day) remains lower than many reported BLE-ECG designs [1, 35] that lack full-stack security, demonstrating that strong cryptographic guarantees can be achieved without exceeding typical power budgets. These results affirm that regulatory-compliant, secure communication is feasible in embedded MedTech systems without compromising runtime efficiency, offering a reproducible model for future IoMT protocol research and deployment.