Modelling and Analysis of DTLS: Power Consumption and Attacks

IoT devices are ubiquitous in modern society. These devices are often constrained by computational power, memory, and energy consumption. DTLS is a protocol that is widely used by IoT devices, including critical industrial IoT systems, as the transport layer for secure and authenticated communication. In this paper we create a formal model of DTLS in Uppaal SMC and show how statistical model checking can be used to analyse, evaluate, and optimise energy consumption for the protocol. In particular we model and analyse different network scenarios, and show how energy consumption is highly dependent on the specific usage scenario. Based on this, we propose and analyse solutions to reduce energy consumption in common scenarios. Finally, we extend our model with an active attacker trying to drain as much energy as possible from the target system by (ab)using DTLS. Analysing and preventing such Denial of Service attacks is essential for critical systems.