Modeling and Formal Verification of the Ticket-based Handoff Authentication Protocol for Wireless Mesh Networks

Abstract

As Wireless Mesh Networks (WMNs) are growing day-by-day, a seamless and secure handoff is gaining significant importance for supporting multi-hop WMNs. On this point, various authentication protocols, such as the ticket-based handoff authentication, for wireless mesh networks have been proposed. Modeling and formal verification of the aforementioned protocol using CPN Tools and ASK-CTL statement are the purposes of this paper. To this aim, the resistance of the protocol against attacks, such as the man in the middle attack is investigated and then, it is concluded that it is secure.