Extending automated protocol state learning for the 802.11 4-way handshake

Abstract

We show how state machine learning can be extended to handle time out behaviour and unreliable communication mediums. This enables us to carry out the first fully automated analysis of 802.11 4-Way Handshake implementations. We develop a tool that uses our learning method and apply this to 7 widely used Wi-Fi routers, finding 3 new security critical vulnerabilities: two distinct downgrade attacks and one router that can be made to leak some encrypted data to an attacker before authentication.