Formal Modeling of Greedy Behavior in Secure Internet of Things Networks

In the Internet of Things (IoT) paradigm, objects should communicate through secure wireless channels and would be able to connect to the Internet. IEEE 802.15.4e and its old versions are the de-facto standards for Wireless Sensor Networks (WSNs) based IoT. IEEE 802.15.4e and its old versions define a slotted CSMA-CA medium access control and physical layer of WSNs. The IoT may experience a multitude of malicious attacks. One critical attack that threatens the network availability is the greedy behavior. In this paper, we propose a UPPAAL model to describe greedy and sane behaviors of IoT devices. We are interested in the contention access period of the beacon-enabled mode of the slotted CSMA-CA. The developed model shows that we can assess and identify both honest and greedy devices. However, it is the first step towards thwarting this attack.