MQTT-HS: A formally verified and proxy-mediated hybrid security protocol for MQTT-based IoT networks

MQTT enables efficient communication in resource-constrained Internet of Things (IoT) systems but does not provide integrated protection against cryptographic and behavioral threats. This paper presents MQTT-HS, a proxy-mediated security protocol that combines certificate-based authentication, ephemeral ECDH/HKDF session establishment, AES-256-GCM payload protection, controlled key refresh, and metadata-based hierarchical intrusion detection with inline enforcement. ProVerif verified the modeled secrecy, authentication, replay-resistance, message-flow agreement, and epoch-key secrecy properties of the cryptographic core. MQTT-HS supports forward secrecy across expired epochs through fresh ephemeral ECDH material, independent epoch-key derivation, and secure erasure of obsolete key material. An ESP32 implementation delivered all 360 protected messages and completed six in-session rekeys, with an average AES-256-GCM encryption latency of 0.354 ms per message. Controlled runtime experiments rejected all evaluated replay, untrusted-certificate, and invalid-signature attempts. The hierarchical XGBoost IDS achieved balanced accuracies of 0.808, 0.960, and 0.862 across its three stages, although Stage 0 produced a 37.5% false-positive rate on the limited legitimate holdout subset. Compared with the evaluated mutual TLS baselines, MQTT-HS preserved more endpoint free heap and provided MQTT-aware detection and enforcement, while requiring greater network bandwidth and a trusted Security Proxy. The results support the feasibility of MQTT-HS under the evaluated prototype configuration.