Abstract
LoRaWAN (Low-power Wide-Area Networks) is the main specification for application-level IoT (Internet of Things). The current version, published in October 2017, is LoRaWAN 1.1, with its 1.0 precursor still being the main specification supported by commercial devices such as PyCom LoRa transceivers. Prior (semi)-formal investigations into the security of the LoRaWAN protocols are scarce, especially for Lo-RaWAN 1.1. Moreover, amongst these few, the current encodings [4], [9] of LoRaWAN into verification tools unfortunately rely on much-simplified versions of the LoRaWAN protocols, undermining the relevance of the results in practice. In this paper, we fill in some of these gaps. Whilst we briefly discuss the most recent cryptographic-orientated works [5] that looked at LoRaWAN 1.1, our true focus is on producing formal analyses of the security and correctness of LoRaWAN, mechanised inside automated tools. To this end, we use the state-of-the-art prover, Tamarin. Importantly, our Tamarin models are a faithful and precise rendering of the LoRaWAN specifications. For example, we model the bespoke nonce-generation mechanisms newly introduced in LoRaWAN 1.1, as well as the "classical" but shortdomain nonces in LoRaWAN 1.0 and make recommendations regarding these. Whilst we include small parts on device-commissioning and application-level traffic, we primarily scrutinise the Join Procedure of LoRaWAN, and focus on version 1.1 of the specification, but also include an analysis of Lo-RaWAN 1.0. To this end, we consider three increasingly strong threat models, resting on a Dolev-Yao attacker acting modulo different requirements made on various channels (e.g., secure/insecure) and the level of trust placed on entities (e.g., honest/corruptible network servers). Importantly, one of these threat models is exactly in line with the LoRaWAN specification, yet it unfortunately still leads to attacks. In response to the exhibited attacks, we propose a minimal patch of the LoRaWAN 1.1 Join Procedure, which is as backwards-compatible as possible with the current version. We analyse and prove this patch secure in the strongest threat model mentioned above. This work has been responsibly disclosed to the LoRa Alliance, and we are liaising with the Security Working Group of the LoRa Alliance, in order to improve the clarity of the LoRaWAN 1.1 specifications in light of our findings, but also by using formal analysis as part of a feedback-loop of future and current specification writing.