A Multi-agent Approach Toward the Security Analysis of the 802.11i Handshake Protocol

Wireless mesh networks (WMNs) are now increasingly deployed because of their low up-front cost, easy network maintenance, robustness, and reliable self coverage. It is important to guarantee the security properties of the WMN to ensure a desired secure system. In this paper, we formally verify the authentication of a WMN. We start with translating a WMN into a multi-agent system (MAS), where each node represents an agent of the MAS. The purpose is to benefit from the existing state-of-the-art verification techniques applicable in the multi-agent domain. We then prove the authentication property of the WMN. Our contributions include: translating a wireless mesh network into a formal multi-agent framework, representing the authentication property as MAS´s formal specification, and applying the strand system verification strategy to prove the correctness of MAS´s authentication