An Energy‐Conscious, Regulation‐Ready and Formally Verified Security Protocol for Low‐Power Medical and Safety Devices

This paper presents a formally verified, lightweight security protocol for energy‐constrained IoT devices operating in regulated environments, with a primary focus on wearable medical systems. The protocol is designed to meet emerging cybersecurity requirements from HIPAA, GDPR and Health Canada and combines Ed25519‐based mutual authentication, ephemeral Curve25519 key exchange and ChaCha20‐Poly1305 authenticated encryption to provide secure, in‐transit protection across heterogeneous nodes with minimal computational and energy overhead. Formal verification using ProVerif and Scyther establishes resilience against key compromise, replay and session confusion, with guarantees of end‐to‐end authentication, forward secrecy, nonce freshness and key integrity in multi‐node settings. Practical feasibility is evaluated through a dual‐phase methodology. A Python‐based simulation framework examines runtime behaviour under adversarial and fault‐prone conditions, enabling analysis of implementation‐level state transitions and recovery behaviour beyond symbolic models. The protocol is then deployed on an STM32L431‐based ECG wearable relayed through a mobile gateway to a cloud server, representing a CPU‐bound short‐range IoT platform. Energy profiling using Nordic PPK2 shows a daily protocol overhead of approximately 7.91 mWh, under 16% of the system energy budget, supporting over 30 days of secure operation per charge. Complementary evaluation on a cellular IoT platform with hardware‐backed security further demonstrates that regulation‐ready secure communication is feasible across heterogeneous low‐power IoT deployments without compromising runtime efficiency.