Paper 2025/2322

Ghost of Sessions Past: Distributed and Forward Secure Key Establishment for Implantable Medical Devices

Abstract

Implantable Medical Devices (IMDs) operate for decades in dynamic and adversarial environments, where device loss, backend compromise, and eventual post-explantation access are realistic long-term threats. Existing IMD security mechanisms largely focus on secure pairing and access control, but rely on long-lived secrets. As a result, a compromise occurring years after deployment can retroactively expose previously recorded patient telemetry. Limiting such damage requires forward secrecy. However, achieving forward secrecy in IMDs is challenging due to strict energy constraints, intermittent connectivity, and safety requirements, which make frequent public-key operations on the implant impractical. We present \emph{Chronos}, a distributed, symmetric-only key establishment protocol that provides forward secrecy for IMDs without requiring public-key cryptography on the implant. \emph{Chronos} evolves cryptographic state across sessions using lightweight primitives on the device, ensuring that past communications remain confidential even under post-compromise exposure. State consistency, resynchronisation, and recovery are coordinated by a threshold-based distributed backend, eliminating single points of failure and enabling controlled emergency operation when the user's device is unavailable, while preserving patient-centric access control. We formally analyse \emph{Chronos} using ProVerif under a Dolev--Yao adversary with post-session compromise capabilities, establishing secrecy, agreement, forward secrecy, and correctness of emergency and recovery mechanisms. We implement \emph{Chronos} end-to-end, including an Android client, distributed backend services, and implant-side firmware on both a 16-bit MSP430 and a 32-bit ARM Cortex-M33 microcontroller. Our evaluation shows that forward secrecy with recovery from state inconsistency is achievable within realistic IMD constraints, with negligible impact on device energy budgets even under pessimistic usage assumptions.