This paper proposes a modelling and verification approach for data transmission over a multichannel wireless local area network (WLAN). The approach uses typed first-order logic as a specification language. We analyse a system which transmits data securely in the presence of the classic Man in The Middle (MitM) attack using Alloy. We develop a methodology for representing secure message exchange on a multi-channel WLAN which uses a changeable array and indices, instead of the message itself so that we can avoid both passive and active MitM attacks. We analyse the model for vulnerabilities and specify assertions for secure data transmission over a multichannel WLAN.
|Title of host publication||2012 IEEE 11th International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom)|
|Number of pages||8|
|Publication status||Published - 2012|