Modelling a multichannel security protocol to address Man in the Middle attacks

Abstract

Unlike wired networks, wireless networks cannot be physically protected, mak ing them greatly at risk. This study looks into advanced ways of implementing security techniques in wireless networks. It proposes using model checking and the orem proving to prove and validate a security protocol of data transmission over multi-channel in Wireless Local Area Networks (WLANs) between two sources. This can help to reduce the risk of wireless networks being vulnerable to Man in the Middle (MitM) attacks. We model secure transmission over a two-host two-channel wireless network and consider the transmission in the presence of a MitM attack. The main goal of adding an extra channel to the main channel is to provide security by stopping MitM from getting any readable data once one of these channels has been attacked. We analyse the model for vulnerabilities and specify assertions for secure data transmission over a multi-channel WLAN. Our approach uses the model analyser Alloy which uses a Satisfiability (SAT) solver to find a model of a Boolean formula. Alloy characterizations of security models are written to analyse and verify that the implementation of a system is correct and achieves security relative to assertions about the model of our security protocol. Further, we use the Z3 theorem prover to check satisfiability using the Satisfiability Modulo Theories (SMT) solver to generate results. Using Z3 does not involve high costs and can help with providing reliable results that are accurate and practical for complex designs. We conclude that, based on the results we achieved from analysing our pro tocol using Alloy and Z3 SMT solver, the solvers complement each other in their strengths and weaknesses. The common weakness is that neither can tell us why the model is inconsistent, if it is inconsistent. We suggest that an approach of be ginning with modelling a problem using Alloy and then turning to prove it using Z3, increases overall confidence in a model.