Automated analysis of Secure Internet of Things Protocols

Formal security analysis has proven to be a useful tool for tracking modifications in communication protocols in an \emph{automated} manner, where full security analysis of revisions requires minimum efforts. In this paper, we formally analyzed prominent IoT protocols and uncovered many critical challenges in practical IoT settings. We address these challenges by using formal symbolic modeling of such protocols under various adversaries and security goals. Further this paper extends formal analysis to cryptographic Denial-of-Service (DoS) and demonstrates that a vast majority of IoT protocols are vulnerable to such resource exhaustion attacks. We present a cryptographic DoS attack countermeasure that can be generally used in many IoT protocols. Our study of prominent IoT protocols such as CoAP and MQTT shows the benefits of our approach.