A modular security analysis of EAP and IEEE 802.11

Abstract

We conduct a reduction-based security analysis of the Extensible Authentication Protocol (EAP), a widely used three-party authentication framework. We show that the main EAP construction, considered as a 3P-AKE protocol, achieves a security notion which we call AKEw under the assumption that the EAP method employs channel binding. The AKEw notion resembles two-pass variant of the eCK model. Our analysis is modular and reflects the compositional nature of EAP. Furthermore, we show that the security of EAP can easily be upgraded by adding an additional key-confirmation step. This key-confirmation step is often carried out in practice in the form of a link-layer specific AKE protocol that uses EAP for bootstrapping its authentication. A concrete example of this is the extremely common IEEE 802.11 4-Way-Handshake protocol used in WLANs. Building on our modular results for EAP, we get as our second major result the first provable security result for IEEE 802.11 with upper-layer authentication.