A Formally Verified Provisioning Protocol for Low-Cost IoT Devices

The growth of IoT has increased the need for robust device provisioning. However, many deployments operate under strict cost constraints. In the low-cost segment, dedicated secure elements are often not affordable. At the same time, complex global supply chains enlarge the attack surface and expose devices to cloning, tampering, and credential injection before deploy- ment. This setting requires a careful balance between security and cost. In this paper, we present a lightweight provisioning protocol designed for low-cost IoT devices without secure elements. The protocol is based on a simplified variant of the Noise framework, adapted to reduce protocol and implementation complexity while maintaining authentication and key-establishment guarantees within a precisely defined attacker model. Given the complexity of cryptographic protocol design, we formally model and verify the protocol in Tamarin to establish authentication and session- key secrecy under explicit trust assumptions. To the best of our knowledge, this is the first formally verified provisioning protocol specifically targeting low-budget IoT deployments. Our notion of lightweightness is structural, referring to protocol simplicity and reduced state-management requirements rather than to a full embedded performance evaluation. The verified guarantees concern disclosure through the modeled protocol and channel abstractions, while extraction of bootstrap key material from the provisioning firmware binary remains outside the scope of the formal analysis.