Contents I. Introduction
The Internet of Things (IoT) describes physical objects equipped with sensors, processing capabilities, software, and other technologies that enable them to establish connections and exchange data with other devices and systems via the Internet or other communication networks [1, 2, 3, 4, 5]. However, with the proliferation of physical devices connected to the internet, ensuring safety and security has become a critical challenge for the IoT, particularly as these devices handle sensitive data. Due to the open nature of the internet, connected devices are vulnerable to attacks and exploitation, and unsecured IoT systems can have catastrophic consequences, posing a risk to both user and smart object security. Moreover, the IoT market is expanding rapidly across various industries, and as a result, IoT devices are frequently designed to meet demand requirements rather than prioritize application security. For this reason, the industry needs to take a more holistic approach to integrating smarter systems. After all, a smarter gadget does not mean a more secure gadget. To ensure the security of IoT devices at an early stage, it is crucial to detect potential vulnerabilities and weaknesses during the design phase. Formal Verification is a process of proving or disproving the correctness of a system with regard to a specific formal specification or property. Theorem Proving and Model Checking are the two most common approaches for automatic Formal Verification, which can be used early in the design process. Theorem Proving relies primarily on high-order logic and mathematical frameworks to build formulas that correlate to system behavior. On the other hand, given a model of the implementation and a formula representing a property in a specific language, Model Checking consists of algorithmically verifying if the formula is satisfied by the model. This article provides an overview of the current state of formal approaches, including tools, languages, and processes for communication protocol security in the IoT. The article is organized into several sections. In Section 2, we review the related work. In Section 3, we provide a general introduction to Formal Verification methods and review the commonly used communication protocols within the IoT domain. In Section 4, we delve into the tools and methods employed in the research literature to detect weaknesses and vulnerabilities in selected protocols using Formal Verification techniques. Finally, we conclude the paper in Section 5, where we present the concluding remarks, summarizing the main contributions and their significance.
