Provably Secure Practical Lightweight Post-Quantum Key Establishment for IoMT

Abstract

This paper introduces PQ-LiteKEM, a formally verified, lightweight post-quantum security protocol for energy- and resource-constrained Internet of Medical Things (IoMT) devices. Addressing near-term quantum threats and emerging regulatory mandates such as the EU Cyber Resilience Act, the protocol mitigates the ‘harvest-now-decrypt-later’ (HNDL) quantum threat by securing sensitive physiological data over low-powered wireless channels. PQ-LiteKEM's architecture pairs lightweight symmetric-key mutual authentication, tied to dynamic hardware fingerprints, with ML-KEM-512 encapsulation and AES-256-GCM authenticated encryption. Formal verification through ProVerif and Scyther confirms security against key compromise, replay, and man-in-the-middle attacks, with provable session forward secrecy, mutual authentication, and session integrity. PQ-LiteKEM is validated on an ESP32-S3-powered wearable sensor communicating with a Raspberry Pi edge gateway over a BLE testbed. Performance profiling measured a total cryptographic latency of 5.9 ms and a peak memory footprint of 9 kB, approximately 0.1% of available RAM. These results show that post-quantum cryptographic guarantees are achievable on constrained medical sensors without sacrificing runtime efficiency, and that the approach generalises beyond BLE to other wireless channels.