Formal Verification of an Efficient Architecture to Enhance the Security in IoT

The Internet of Things (IoT) is one of the world's newest intelligent communication technologies. There are several kinds of novels about IoT architectures, but they still suffer from security and privacy challenges. Formal verification is a vital method for detecting potential weaknesses and vulnerabilities at an early stage. During this paper, a framework in the Event-B formal method will be used to design a formal description of the secure IoT architecture to cover the security properties of the IoT architecture. As well as using various Event-B properties like formal verification, functional checks, and model checkers to design different formal spoofing attacks for the IoT environment. Additionally, the Accuracy of the IoT architecture can be obtained by executing different Event-B runs like simulations, proof obligation, and invariant checking. By applied formal verification, functional checks and model checkers verified models of IoT-EAA architecture have automatically discharged 82.35% of proof obligations through different Event-B provers. Finally, this paper will focus on introducing a well-defined IoT security infrastructure to address and reduce the security challenges.