A Modular Security Analysis of EAP and IEEE 802.11

The Extensible Authentication Protocol (EAP), specified in RFC 3748 [4], is a widely used authentication framework for network access control. It is particularly common in wireless networks, being used by protocols like IEEE 802.11 (Wi-Fi), IEEE 802.16 (WiMAX) and various 3G/4G mobile networks. The typical use case of EAP is in settings where a client seeks to gain access to a network controlled by an authenticator, but where the client and authenticator do not share any common credentials. EAP allows the client and authenticator to authenticate each other based on a mutually trusted server. Technically, EAP is not a specific authentication mechanism on its own, but rather specifies a certain generic three-party construction that composes other concrete authentication protocols into a unified framework. This provides applications of EAP the freedom to choose whatever concrete instantiation is suitable for their own specific setting. The success of this approach is apparent by the huge and diverse set of real-life deployments using the EAP framework.

Surprisingly then, given its prevalence and importance, there has been no formal reduction-based provable security analysis of EAP. One reason for this might be due to the general nature of EAP itself. As mentioned above, EAP is not a single protocol on its own, but relies on other sub-protocols to instantiate it. As such, many things in the EAP specification are left unspecified or considered out of scope. However, in order to conduct a formal security analysis of EAP, these details matter and require a careful treatment. Generally, the need to make assumptions on protocols outside of EAP makes analysis harder (see also [15]), because now it is not sufficient to consider a single protocol in isolation, but rather it has to be considered it in tandem with other protocols.

Another reason for the lack of provable security analyses of EAP might be the fact that it is a three-party protocol. As pointed out by Schwenk in his recent work on Kerberos [28], apart from a few papers like [3, 5, 8, 24, 28] relatively little work has been done on three-party protocols^{Footnote 1} in the computational setting compared to the huge literature on two-party protocols.

In this paper we aim to remedy this state-of-affairs by providing a formal reductionist analysis of EAP. We then build on our result to obtain a result for the extremely common IEEE 802.11 wireless standard with upper-layer authentication. Current results on IEEE 802.11 have so far only focused on the much simpler pre-shared key setting, while we can now provide an analysis of the full protocol. Below we will further expand upon our results, but first we provide a brief description of the EAP architecture and how IEEE 802.11 relates to it.

Review of EAP and IEEE 802.11. The general EAP architecture is shown in Fig. 1. The exchange begins with the client and trusted server authenticating each other using some concrete authentication protocol, like TLS. However, the whole TLS exchange is wrapped within a generic set of EAP messages, known as Request/Response messages. The combination of a concrete authentication protocol together with the EAP encapsulation is called an EAP method. Numerous EAP methods have been defined, with EAP-TLS being one of the most widely supported. Besides authenticating each other, the EAP-method usually also results in the client and server agreeing upon a shared key. The server will forward this key to the authenticator over some separately established channel. The EAP standard does not specify which protocol to use here, but in practice the de-facto standard is RADIUS [26].^{Footnote 2} Once the key is transported from the server to the authenticator—which so far has only operated in pass-through mode between the client and the server—the EAP exchange is technically complete. However, the client and authenticator now typically use the key distributed by EAP to authenticate each other using some link-layer specific protocol. If the link-layer media is a wireless link provided by the IEEE 802.11 protocol [2], then this entire exchange is usually referred to as “802.11 with upper-layer authentication”.

On the Difficulty of Modeling EAP. In this paper we consider the provable security of both EAP and 802.11 with upper-layer authentication in the game-based setting. We do this in a modular way: first considering the security properties provided by EAP and 802.11 in isolation, then using a composition theorem to link them together. However, since EAP inherently depends on other protocols, assessing the exact security guarantees it provides is in a sense harder than for “standalone” protocols like TLS, IKE and SSH. While the EAP specification defines the security requirements of each EAP method [4, Sect. 7], this only covers the communication between the client and the trusted server. Still, as pointed out in the beginning, it is more accurate to think of EAP as a three-party protocol. But RFC 3748 leaves unspecified how, for example, the derived key should be transferred from the server to the authenticator. Hence, solely using the security claims from RFC 3748 is not sufficient to decide the security of EAP considered as a three-party protocol. In fact, without making further assumptions on the various protocols that make up EAP, it is impossible to talk about “the” EAP and its security. Consequently, in order to be able to analyze EAP, we will have to make some assumptions on these protocols.

Firstly, in this paper we are going to assume that the communication between the authenticator and the trusted server takes place over a secure channel. Specifically, we model the link as a two-party authenticated channel establishment protocol (2P-ACCE) based on symmetric long-term pre-shared keys^{Footnote 3} (see Sect. 2.3 for a formal definition). Since most key-transport protocols used between the server and the authenticator support to be run over a secure channel (see e.g. RADIUS-over-TLS [30]), this assumption seems reasonable.

Second, a well-known issue with the EAP architecture is the so-called “lying authenticator problem”. Namely, a malicious authenticator may present false identity information to the client and the trusted server. Unless the EAP method provides a feature known as channel binding [14], there is no way for the client and server to verify that they are in fact talking to the same authenticator (see [14, Sect. 3] for examples of attacks that this may enable). Hence, in this paper we are generally going to assume that EAP provides channel binding, although we will also briefly explore the security guarantees provided by EAP without channel binding in Sect. 4.3. While there are a couple of ways to achieve channel binding in EAP (see [14, Sect. 4.1]), here we are only going to focus on the cryptographically simplest one, described in RFC draft draft-ohba-eap-channel-binding-02 [25]. In this approach, the client and authenticator identities are being input to the key-derivation step of EAP, cryptographically binding the session key to the right pair of identities (see Sect. 4.2 for details).

Our Contributions. The main contributions of this paper are the following.

• We provide the first reductionist-based provable security result for three-party EAP with channel binding.

• We show how the security guarantees of EAP can be upgraded by adding an additional key-confirmation step (modeled as a 2P-AKE). This corresponds to a common usage pattern where EAP is first used to bootstrap the establishment of a common key among the client and authenticator, then some lower-layer specific 2P-AKE is run between the client and authenticator to mutually prove possession of that key (in addition to establishing session keys for the lower-layer link).

• We provide the first game-based provable security result for the IEEE 802.11 4-way-handshake protocol in the pre-shared key setting. This corresponds to the setting typically found in home WLANs.

• More importantly however, the results above combine to provide the first reductionist-based provable-security result for the full IEEE 802.11 protocol with upper-layer authentication. This corresponds to the setting usually found in enterprise and university WLANs. For instance, the eduroam network, which is used to provide wireless roaming services to university and research institutions, uses IEEE 802.11 with upper-layer authentication.

• Our technical means for obtaining the above results are two modular composition theorems which may be of separate interest. Namely, the two theorems consider a fairly generic way of constructing a 3P-AKE protocol, using generic 2P-AKEs and secure channels as building blocks. For instance, both Kerberos and the AKA protocol used within the UMTS and LTE mobile networks, fit the description of our 3P-AKE construction. In particular, for the latter protocol, our theorems might enable a more general and modular analysis than the one recently provided by Alt et al. [5].

Technical Overview of Our Results. The main technical contributions of this paper are two fairly generic composition theorems which correspond to the “cryptographic core” of EAP and IEEE 802.11 with upper-layer authentication, respectively. To obtain these theorems, however, we have to provide an appropriate security model. Our starting point is the original 3P-AKE model of Bellare and Rogaway [8], but which we update to accommodate our needs. Most importantly, EAP and IEEE 802.11—both when considered separately and when combined—can achieve different levels of security. In order to capture these differences we have to define three different corruption models of differing strengths. These definitions are based on the eCK model^{Footnote 4} [21], and are primarily concerned with the level of adaptivity afforded to the adversary with respect to corruption queries. Preempting our own results a bit, we show that standalone EAP can achieve a restricted variant of forward secrecy, while IEEE 802.11 without upper-layer authentication achieves no forward secrecy (this is natural since it relies on symmetric primitives exclusively). However, when EAP and 802.11 are combined, the security is upgraded to achieve forward secrecy in our strongest corruption model. Briefly, the difference between the strongest security model and the intermediate one depends on what happens if the test-session does not have partner. When the test-session does not have a partner in the strongest model, the adversary is still allowed to learn all the long-term keys of the parties involved, as long as this happens after the test-session accepted. On the other hand, if the test-session does not have a partner in the intermediate model, then the adversary is forbidden from learning any of these long-term keys. If the test-session does have a partner, then there is no difference between the two models: the adversary is allowed to learn any long-term key at any time. The formal definitions of these models are provided in Sect. 2.2.

Intuitively, the reason why EAP on its own cannot achieve security in our strongest model is because it does not provide explicit entity authentication. Specifically, the client has no guarantee that the key-transport protocol between the server and authenticator actually took place without running some lower-link protocol to confirm. Suppose an adversary could learn the long-term key shared between the server and the authenticator after the client accepted, but before the key transport took place. Then it could simply impersonate the authenticator towards the server and have it send over the session key it previously established with the client. According to our strongest security model this adversary would be valid (since the exposure of the PSK happened after the client accepted this is allowed), whereas in the intermediate one it would not (since the client session does have a partner, the PSK cannot be exposed at all). Essentially, the purpose of the lower-layer protocol is to provide key-confirmation to the standalone EAP protocol, which ensures that the client will always have a partner before it accepts.

Besides the introduction of the three different corruption models, we only provide a few other changes to the original 3P-AKE model of Bellare and Rogaway [8]. For example, we support both asymmetric and symmetric long-term keys, and dispense with the explicit \(\mathsf {SendS}\) query to the trusted server (now modeled simply as a regular \(\mathsf {Send}\) query).

One thing we do keep from [8] however, is the concept of partner functions. Interestingly, the use of partner functions has seen rather limited adoption when compared to partnering based on matching conversations [7] or abstract session identifiers (SIDs) [6]. However, when modeling EAP, we are in the peculiar situation that the parties that we need to partner (the client and the authenticator) do not have any messages in common! Naturally, this makes partnering based on matching conversations more difficult, but it also severely limits our choice of SIDs: we are essentially forced to pick their session keys as the SID. While using the session key as the SID is reasonable in many settings (cf. [17]), it does not guarantee public partnering (see [11]). This is important for modular composition proofs like our own. While partnering functions have been criticized for being non-intuitive and hard to work with (even by Rogaway himself [27, Sect. 6]), they generalize more naturally to the three-party setting than SIDs. Essentially, this is because partner functions can take global transcript information into consideration rather than only the local views of the two partners. In a companion manuscript [10] we explore partner functions in more detail, showing their soundness as a partnering tool for analyzing key exchange protocols.

After proving the two composition results in Sect. 3 for generic protocols, we show how to apply them to EAP with and without upper-layer authentication in Sects. 4 and 5, respectively.

2.1 A Unified Execution Model

Protocol Participants. An AKE protocol is carried out by a set of parties \(U \in \mathcal {P}\), where U either takes on the role of initiator, responder or server, i.e., \(\mathcal {P}\) is partitioned into three disjoint sets \(\mathcal {I}\), \(\mathcal {R}\) and \(\mathcal {S}\), consisting of the initiators, responders and servers, respectively. In this paper we assume that all initiators and servers are in possession of a long-term asymmetric key-pair \((sk_U, pk_U)\), while all responders and servers share a symmetric pre-shared key \(K\). For every party holding a public key, we assume that the other parties have an authenticated copy of it.

Syntax. A protocol is a tuple \(\mathrm {\Pi }= (\mathsf {KG}, \varSigma )\) of probabilistic polynomial-time algorithms, where \(\mathsf {KG}\) specifies how long-term keys are generated for each party, and \(\varSigma \) specifies how (honest) parties behave. Each party \(U \in \mathcal {P}\) can take part in multiple executions of the protocol, both concurrently and subsequently, called a session. We use an administrative label to refer to the ith session at user U. This will sometimes also be simplified to \(\pi \). Associated to each session , there is a collection of variables that embodies the (local) state of during the protocol.

• \(sk_U,pk_U\) – the long-term private/public key of party U,

• \(\mathsf {peers}\) – a list of the identities of the intended communication peers of ,

• \(\mathsf {peerPK}\) – a list of the public keys of the parties in ,

• \(\mathsf {peerPSK}\) – a list of the long-term PSKs shared between U and ,

• – a vector of accept states ,

• \(k\in \lbrace 0, 1 \rbrace ^\lambda \cup \lbrace \bot \rbrace \) – the symmetric session-key derived by .

Only initiators and responders accepts sessions keys, i.e., if \(S \in \mathcal {S}\), then we always have . Note that this is pure formalism; we certainly except many protocols in which the trusted server might be in possession of the session key—in fact, the trusted server might be the one that choses and distributes it—we simply do no not associate it with the variable \(k\).

Remark 1

We use a list of acceptance states in order to model protocols that are logically built out of sub-protocols. The individual acceptance states provides a convenient way to signal to the adversary that a session has accepted in some intermediate sub-protocol \(\mathrm {\Pi }_i\) of the full protocol \(\mathrm {\Pi }\). By convention, we will let represent the running-state of the full protocol, and use to denote this state. Specifically, has the same role as the single running-state variable \(\alpha \) which is typically used by most other formal protocol models. Saying that \(\pi \) is running, or that it has accepted or rejected, refers to the value of \(\alpha _F\).

We require the following semantics of the variables and \(k\):

By convention, whenever we set \(\alpha _i = \mathsf {rejected}\), we also automatically set \(\alpha _j = \mathsf {rejected}\) for all \(i < j\), in accordance with (2). Moreover, we assume that the session key \(\pi .k\) is set only once.

A Unified Security Experiment. To define the security goals of both AKE and ACCE protocols we use the unified experiment shown in Fig. 2. Experiment \(\mathsf {Exp}_{\mathrm {\Pi },\mathcal {Q},\mathcal {A}}^{}(\lambda )\) is parameterized on the protocol \(\mathrm {\Pi }\), a query set \(\mathcal {Q}\), and the adversary \(\mathcal {A}\). While the query sets used to define AKE and ACCE security will be different, they will both contain the following “base” query set \(\mathcal {Q}_{base}\):

• \(\mathsf {NewSession}(U, [V, W])\): This query creates a new session at party U, optionally specifying its intended communication peers V and W. The state variables are initiated as follows: , , if V and/or W are specified as U’s peers, then , , , ^{Footnote 5} and (See footnote 5). It is required that U, V and W all have different roles. Finally, if \(U \in \mathcal {I}\), then also produces its first message m according to specification of protocol \(\mathrm {\Pi }\). Both the administrative label and m are returned to \(\mathcal {A}\).

• : If , return \(\bot \). Otherwise, \(\pi \) creates a response message \(m^*\) according to the specification \(\varSigma \). This depends on \(\pi \)’s role and current internal state. Both \(m^*\) and are returned to \(\mathcal {A}\).

• : If or \(U \in \mathcal {S}\), return \(\bot \). Else, return . From this point on is said to be revealed. Note that is not considered revealed if the \(\mathsf {Reveal}\) query was made before \(\pi \) accepted.

• \(\mathsf {LongTermKeyReveal}(U, [V])\): Depending on the second input parameter, this query returns a certain long-term key of party U.

  • \(\mathsf {LongTermKeyReveal}(U)\): If U has an associated private-public key-pair \((sk_U,pk_U)\), return the private key \(sk_U\).

  • \(\mathsf {LongTermKeyReveal}(U, V)\): If U and V share a symmetric long-term key \(K_{UV}\), return \(K_{UV}\).

  After a long-term key is leaked we say that it is exposed and the corresponding party corrupted.

Note that we are working in the post-specified peer model [13], meaning that the identities of a session’s peers might not necessarily be known by the session at the onset of the protocol, but are instead learned as the protocol progresses.

Protocol Correctness. It is required that a protocol satisfies the following correctness requirement. In an honest execution of the protocol between an initiator , a responder and a trusted server —meaning that all messages are faithfully transmitted between them according the protocol description—then all sessions end up accepting, and and both hold the same session key \(k\ne \bot \).

Remark 2

Note that experiment \(\mathsf {Exp}_{\mathrm {\Pi },\mathcal {Q},\mathcal {A}}(\lambda )\) does not provide any output and does not define any “winning condition” for \(\mathcal {A}\). Instead, it provides a single execution experiment on which we can define many different winning conditions. This is convenient when we later want to define AKE-security and ACCE-security.

Transcripts and Partner Functions. Consider a run of experiment \(\mathsf {Exp}_{\mathrm {\Pi },\mathcal {Q},\mathcal {A}}(\lambda )\), where \(\mathcal {Q}_{base} \subseteq \mathcal {Q}\). Let T be the ordered transcript consisting of all the \(\mathsf {Send}\) and \(\mathsf {NewSession}\) queries made by \(\mathcal {A}\), together with their responses. A transcript T is a prefix of \(T'\), written \(T \subseteq T'\), if the first |T| entries of \(T'\) are identical to T. We let \(\mathcal {T}\) denote the set of all possible transcripts generated from running experiment \(\mathsf {Exp}_{\mathrm {\Pi },\mathcal {Q},\mathcal {A}}(\lambda )\). To define partnering in our security analysis we use the concept of partner functions as introduced by Bellare and Rogaway [8].

Definition 1

(Partner functions). A partner function is a polynomial-time function \(f :\mathcal {T} \times (\mathcal {P} \setminus \mathcal {S}) \times \mathbb {N} \rightarrow ((\mathcal {P} \setminus \mathcal {S}) \times \mathbb {N}) \cup \lbrace \bot \rbrace \), subject to the following requirement

Instead of \(f (T, U,i) = (V,j)\), we also write , or even just if the exact identities of the sessions are irrelevant.

Definition 2

(Partnering). Let f be a partner function. A session \(\pi '\) is a partner to \(\pi \) if .

Remark 3

Partnering is only defined between initiators and responders. Servers are not considered partners to any session.

Partnering Soundness. For a security analysis based on partner functions to be meaningful, the partner function needs to satisfy certain soundness properties. Briefly, soundness demands that partners should: (1) end up with the same session key, (2) agree upon who they are talking to, (3) have compatible roles, and (4) be unique. These requirements are essentially the same as those demanded for SIDs through the “\(\mathsf {Match}\)-security” notion introduced by Brzuska et al. [11].

Definition 3

(Partnering soundness predicate). Consider a run of experiment \(\mathsf {Exp}_{\mathrm {\Pi },\mathcal {Q},\mathcal {A}}(\lambda )\), and let T be the corresponding transcript. Predicate \(\mathsf {Sound}\) is true if and only if the following holds for all \(T' \subseteq T\). If sessions and have both accepted and , then

1. 1.

   ,

2. 2.

   , , and \(W \in \mathcal {S}\),

3. 3.

   \(U \in \mathcal {I} \wedge V \in \mathcal {R}\) or \(U \in \mathcal {R} \wedge V \in \mathcal {I}\),

4. 4.

   there is no such that .

We let \(\mathsf {Exp}_{\mathrm {\Pi },\mathcal {Q},\mathcal {A}}^{\mathsf {Sound}}(\lambda ) \Rightarrow 1\) denote the event that predicate \(\mathsf {Sound}\) evaluated to true.

Remark 4

Note that predicate \(\mathsf {Sound}\) depends on the partner function f.

Remark 5

The use of partner functions to analyze key exchange protocols is rare in the literature. To the best of our knowledge, besides the original paper by Bellare and Rogaway [8], it has only been used in one other paper by Shoup and Rubin [29].

2.2 2P-AKE and 3P-AKE

Syntax. A 2P/3P-AKE protocol has the same syntax as the general protocol defined in Sect. 2.1. Moreover, in our framework, there is no syntactical difference between a 2P-AKE protocol and a 3P-AKE protocol. However, in a 2P-AKE protocol there is no trusted server session \(S \in \mathcal {S}\), and the session variables , \(\pi .\mathsf {peerPK}\) and contain at most a single entry.

AKE Security. Besides soundness, a secure AKE protocol is supposed to provide secrecy of the distributed session keys. To capture this, the base query set \(\mathcal {Q}_{base}\) is extended with the following query.

• : If or \(U \in \mathcal {S}\), return \(\bot \). Otherwise, draw a random bit b, and return ’s session key if \(b = 0\), or a random key if \(b = 1\). We call the test-session and the returned key the challenge-key. The \(\mathsf {Test}\) query can only be made once.

Let \(\mathcal {Q}= \mathcal {Q}_{base} \cup \lbrace \mathsf {Test} \rbrace \). Experiment \(\mathsf {Exp}_{\mathrm {\Pi },\mathcal {Q},\mathcal {A}}(\lambda )\) stops when \(\mathcal {A}\) outputs a bit \(b'\). The goal of the adversary is to correctly guess the secret bit b used to answer the \(\mathsf {Test}\) query. However, \(\mathcal {A}\) is only given “credit” if the chosen test-session was fresh. A session is fresh if the adversary did not learn its session by trivial means, for example by revealing it or by impersonating its peers after having obtained their long-term keys etc. Formally, in Fig. 3, we specify three freshness predicates \(\mathsf {Fresh}_{\mathsf {AKE}}\), \(\mathsf {Fresh}_{\mathsf {AKE}^w}\), and \(\mathsf {Fresh}_{\mathsf {AKE^{static}}}\), of various permissiveness with respect to long-term key leakage. Each freshness predicate also give rise to a corresponding security notion AKE, AKE\(^w\) and AKE\(^{\mathsf {static}}\).

The AKE model is our “partner function analogue” of the standard eCK model (as defined in the updated version [21] of the original paper [22]), with the main difference being that we do not consider leakage of ephemeral values. In particular, the AKE model captures both key-compromise impersonation (KCI) attacks and forward secrecy. KCI attacks are captured since the test-session’s own long-term private key can always be exposed by the adversary. Forward secrecy is captured since the adversary can, under certain conditions, learn the long-term keys of the peers of the test-session too. Specifically, the forward secrecy guarantees provided by the AKE model are rather strong: if a session has a partner, then the adversary is allowed to expose any long-term key it wants, while if the session does not have a partner, then the adversary must wait until after the session accepted before it can expose the relevant keys. Note that partnering is used to model passiveness by the adversary in the test-session. Intuitively, even if the adversary knew all the long-term keys before the test-session started, if the test-session ends up with a partner, then the adversary cannot actually have exploited its knowledge of the keys.

Compared to the AKE model, the AKE\(^w\) model is more restrictive with respect to forward secrecy: if the test-session does not have partner, then the adversary is disallowed from exposing any of the relevant long-term keys. The AKE\(^w\) model is similar to the two-pass variant of the eCK model (see [21, Definition 3]). As mentioned in the introduction, standalone EAP does not achieve security in the AKE model, but we will show that it is secure in the AKE\(^w\) model.

Finally, the AKE\(^{\mathsf {static}}\) model targets protocols that do not provide any forward secrecy, hence it disallows the adversary from exposing the long-term keys altogether (of course, the adversary is allowed to expose long-term keys unrelated to the test-session and its peers).

Definition 4

(Key-indistinguishability predicate). Suppose \(\pi \) was the test-session chosen by \(\mathcal {A}\) in a run of experiment \(\mathsf {Exp}_{\mathrm {\Pi },\mathcal {Q},\mathcal {A}}^{}(\lambda )\), b was the random bit used in answering the \(\mathsf {Test}\) query, and suppose \(b'\) was the final output of \(\mathcal {A}\). Define predicate \({\mathsf {AKE}}^* \in \lbrace {\mathsf {AKE}}, {\mathsf {AKE}}^w, {\mathsf {AKE}}^{\mathsf {static}} \rbrace \) as follows:

Let \(\mathsf {Exp}_{\mathrm {\Pi },\mathcal {Q},\mathcal {A}}^{{\mathsf {AKE}}^*}(\lambda ) \Rightarrow 1\) denote the event that \({\mathsf {AKE}}^*\) evaluated to true.

Definition 5

(AKE security). A protocol \(\mathrm {\Pi }\) is AKE \(^*\) -secure, if there exists a partnering function f, such that for all PPT adversaries \(\mathcal {A}\),

• is negligible in security parameter \(\lambda \), and

• is negligible in security parameter \(\lambda \),

where \(\mathrm {AKE}^* \in \lbrace \mathrm {AKE}, \mathrm {AKE}^w, \mathrm {AKE}^{\mathsf {static}} \rbrace \).

2.3 (2P)-ACCE

Syntax. A (2P)-ACCE protocol is a two-party protocol as defined in Sect. 2.1, together with an associated stateful authenticated encryption scheme (stAE) \(\mathsf {stE} = (\mathsf {st.Gen},\mathsf {stE.Init},\mathsf {stE.Enc},\mathsf {stE.Dec})\) (following [20]^{Footnote 6}). Intuitively, an ACCE protocol is an amalgamation of an ordinary 2P-AKE protocol and a secure channel based on symmetric keys, where the session keys of the 2P-AKE protocol are used to key the secure channel.

Correctness of the stAE scheme demands that if the deterministic algorithm \(\mathsf {st.Init}\) produced initial states \(st_E^0, st_D^0\); and the ACCE session key \(k\) was used to produce a sequence of ciphertext/state pairs \((C_i, st_E^{i+1}) \leftarrow \mathsf {stE.Enc}(k,m_i, st_E^i)\) such that \(C_i \ne \bot \) for all \(i \ge 0\); then one must have, for all \(i \ge 0\), that \(m'_i = m_i\) in the sequence of decryptions \((m'_i, st_D^{i+1}) \leftarrow \mathsf {stE.Dec}(k, C_i, st_D^i)\).

ACCE Security. To define security of an ACCE protocol, we extend the base query set \(\mathcal {Q}_{base}\) with two additional queries, \(\mathsf {Encrypt}\) and \(\mathsf {Decrypt}\), that allow the adversary to interact with the channels established in the protocol. The two queries are specified in Fig. 4.

Let \(\mathcal {Q}= \mathcal {Q}_{base} \cup \lbrace \mathsf {Encrypt}, \mathsf {Decrypt} \rbrace \). Experiment \(\mathsf {Exp}_{\mathrm {\Pi },\mathcal {Q},\mathcal {A}}(\lambda )\) stops when \(\mathcal {A}\) outputs a pair \((\pi , b')\), consisting of a session \(\pi \) and a bit \(b'\). The goal of the adversary, formally captured in the following predicate, is to break either the confidentiality or integrity of one of the channels established by a fresh session.

Definition 6

(ACCE predicates). Consider a run of experiment \(\mathsf {Exp}_{\mathrm {\Pi },\mathcal {Q},\mathcal {A}}(\lambda )\), and let T be the corresponding transcript. Suppose \((\pi , b')\) was the final output by \(\mathcal {A}\).

• Predicate is true if and only if, sometime during \(\mathsf {Exp}_{\mathrm {\Pi },\mathcal {Q},\mathcal {A}}(\lambda )\), \(\mathcal {A}\) made a \(\mathsf {Decrypt}\) query that output something other than \(\bot \) for a fresh session \(\pi \).

• Predicate is defined as follows:

  

  (6)

Let (resp. ) denote the event that (resp. ) evaluated to true.

Definition 7

(ACCE security). A protocol \(\mathrm {\Pi }\) is ACCE-secure, if there exists a partnering function f, such that for all PPT adversaries \(\mathcal {A}\), the following are all negligible in the security parameter \(\lambda \),

• ,

• ,

• .

Remark 6

Our definition of ACCE security is slightly different from the standard one introduced by Jager et al. [16]. Specifically, in the standard formulation of ACCE, the \(\mathsf {Decrypt}\) oracle is conditional, meaning that if \(\pi .b = 0\), then \(\mathsf {Decrypt}\) always returns \(\bot \) irregardless of whether the supplied ciphertext was a valid forgery or not. This is done in order to encode both the channel privacy and the channel integrity goal as a single distinguishing game. However, this makes proofs relying on ACCE security more cumbersome since the \(\mathsf {Decrypt}\) query does not actually provide a proper decryption oracle. By casting ACCE channel security as two separate security goals, the \(\mathsf {Decrypt}\) query becomes a proper decryption oracle. In the full version we prove that our definition of ACCE is equivalent with the standard one.

2.4 Explicit Entity Authentication

Explicit entity authentication is frequently considered one of the required security properties of a protocol. However, in this paper we will only prove/assume it for some protocols, because some of the protocols we consider simply cannot achieve it. The need for AKE protocols to provide explicit entity authentication has actually been somewhat disputed in the literature (see e.g. [8, Sect. 1.6], [27, Sect. 6] or [19, Sect. 1.2]). On the other hand, explicit entity authentication has always been part of the requirements of ACCE security [16, 18, 20]. Since the definition of entity authentication is formulated identically for both AKE and ACCE protocols, we give a merged definition here. Let \(\mathcal {Q}_{\mathsf {AKE}}\) denote the query set of the AKE experiment, and let \(\mathcal {Q}_{\mathsf {ACCE}}\) denote the query set of the ACCE experiment.

Definition 8

(Entity authentication predicate). Let T be the transcript of experiment \(\mathsf {Exp}_{\mathrm {\Pi },\mathcal {A}, \mathcal {Q}_{\mathsf {X}}}(\lambda )\). Predicate \(\mathsf {Auth}\) is true if and only if the following holds for all \(T' \subseteq T\). For all fresh sessions \(\pi \) in \(T'\):

Let denote the event that \(\mathsf {Auth}\) is true, where \(\mathsf {X} \in \lbrace \mathsf {AKE}, \mathsf {ACCE} \rbrace \).

Definition 9

(Explicit entity authentication). A protocol \(\mathrm {\Pi }\) provides explicit entity authentication if there exists partner function f, such that for all PPT adversaries \(\mathcal {A}\), it holds that

1. 1.

   \(\mathrm {\Pi }\) is \(\mathsf {X}\)-secure, and

2. 2.

   is negligible in security parameter \(\lambda \),

where \(\mathsf {X} \in \lbrace \mathsf {AKE}, \mathsf {AKE}^w, \mathsf {AKE}^{\mathsf {static}}, \mathsf {ACCE} \rbrace \).

Remark 7

Note that the explicit entity authentication of an AKE (resp. ACCE) scheme needs to hold with the same partner function as used to prove its AKE (resp. ACCE) security.

In this section we prove two composition theorems for two fairly generic constructions of 3P-AKE protocols. The first construction, shown as protocol \(\mathrm {\Pi }_3\) in Fig. 5, resembles the standalone EAP. It uses as building blocks any secure 2P-AKE protocol (in the strongest AKE model), any secure 2P-ACCE protocol, and a pseudorandom function for channel binding. The second construction, shown as protocol \(\mathrm {\Pi }_5\) in Fig. 5, resembles the EAP combined with a subsequent key-confirmation step, modeled here as a 2P-AKE protocol secure in the weakest AKE\(^{\mathsf {static}}\) model. We emphasize that the 3P-AKE protocol used as the underlying building block by protocol \(\mathrm {\Pi }_5\), does not necessarily have to be based on the \(\mathrm {\Pi }_3\) construction. Any 3P-AKE protocol secure according to the AKE\(^w\) model works. In Sects. 4 and 5, we will see how these generic constructions can be instantiated with EAP and IEEE 802.11 with upper-layer authentication, respectively.

3.1 2P-AKE + 2P-ACCE + Channel Binding \(\implies \) 3P-AKE\(^{w}\)

Construction. From a 2P-AKE protocol \(\mathrm {\Pi }_1\) (based on public keys), a 2P-ACCE protocol \(\mathrm {\Pi }_2\) (based on pre-shared symmetric keys), and a pseudorandom function \(\mathsf {PRF}\), we construct the 3P-AKE protocol \(\mathrm {\Pi }_3\) shown in Fig. 5. Specifically, protocol \(\mathrm {\Pi }_3\) works as follows. First, sub-protocol \(\mathrm {\Pi }_1\) is run between the initiator A and the trusted server S to derive an intermediate key \(k_{AS}\). A also communicates the identities A and B to S, where B is the identity of responder that A wants to talk to. Note that A knows both S and B at the beginning of the protocol whereas S learns about B from the identities communicated by A. Technically, this means that a session at A needs to be initialized with the identities of S and B (setting the \(\mathsf {peers}\) variable accordingly), while a session at S will update its \(\mathsf {peers}\) variable to include B after receiving this identity from A.

From \(k_{AS}\), both A and S derive the key \(k_{AB} \leftarrow \mathsf {PRF}(k_{AS},A,B)\). This key will be the ultimate session key shared between A and B in protocol \(\mathrm {\Pi }_3\). In order for S to transfer \(k_{AB}\) to B they establish a secure channel using sub-protocol \(\mathrm {\Pi }_2\). Once established, S sends the session key \(k_{AB}\) over the channel to B. Alongside \(k_{AB}\), the server S also sends the identity of A to B (causing the receiving B to update its \(\mathsf {peers}\) variable). For simplicity, we assume that the transfer of A and \(k_{AB}\) is done using a single channel message, which we call the \(C_{\mathrm {key}}\) message. Note that the initiator A accepts in protocol \(\mathrm {\Pi }_3\) when it has derived \(k_{AB}\), while the responder B accepts once it has received—and properly decrypted—the \(C_{\mathrm {key}}\) message, finally obtaining \(k_{AB}\).

Result. Our first composition result shows that protocol \(\mathrm {\Pi }_3\) is 3P-AKE\(^w\)-secure if sub-protocol \(\mathrm {\Pi }_1\) is 2P-AKE-secure, sub-protocol \(\mathrm {\Pi }_2\) is 2P-ACCE-secure, and \(\mathsf {PRF}\) is a pseudorandom function. Note that since \(\mathrm {\Pi }_3\) does not provide explicit entity authentication—in fact, no initiator session A will have a partner at the time it accepts—it cannot achieve security in the strongest AKE model due to the attack mentioned for standalone EAP in the introduction.

Roughly, the proof of the first composition theorem works as follows. The 2P-AKE-security of sub-protocol \(\mathrm {\Pi }_1\) allows us to swap out the intermediate keys \(k_{AS}\) with random ones. The PRF-security of the function \(\mathsf {PRF}\) then allows us to replace the derived session keys \(k_{AB}\) with random ones. Finally, the ACCE channel-privacy of sub-protocol \(\mathrm {\Pi }_2\) ensures that the adversary learns nothing about the session keys transfered in the \(C_{\mathrm {key}}\) messages.

However, in order to make our proof work, we have to make one technical assumption on the partner function of sub-protocol \(\mathrm {\Pi }_2\). Namely, we have to assume that it is symmetric, meaning that implies . Note that this requirement is straightforwardly met by partner functions based on SIDs.

Theorem 1

Let \(\mathrm {\Pi }_3\) be the protocol described in Sect. 3.1. If protocol \(\mathrm {\Pi }_1\) is 2P-AKE-secure, \(\mathrm {\Pi }_2\) is ACCE-secure using a symmetric partner function, and \(\mathsf {PRF}\) is a secure PRF, then there exists a partner function \(f_3\), such that protocol \(\mathrm {\Pi }_3\) is 3P-AKE\(^w\)-secure.

Concretely, if \(\mathrm {\Pi }_1\) is AKE-secure with the partner function \(f_1\), and \(\mathrm {\Pi }_2\) is ACCE-secure with the symmetric partner function \(f_2\), then we can create a partner function \(f_3\), and adversaries \(\mathcal {B}_1, \cdots , \mathcal {B}_4\) and \(\mathcal {D}\), such that

where is an upper bound on the number of sessions at each party.

Proof

We begin by defining the partner function \(f_3\) using the partner functions for sub-protocols \(\mathrm {\Pi }_1\) and \(\mathrm {\Pi }_2\).

Defining the Partner Function for \(\mathrm {\Pi }_3\) . Intuitively, \(f_3\) is constructed by “composing” the two partner functions \(f_1\) and \(f_2\) assumed to exist for sub-protocols \(\mathrm {\Pi }_1\) and \(\mathrm {\Pi }_2\). For example, if is an initiator session, then if there exists a trusted server session , such that and , That is, is ’s \(f_3\)-partner if there exists a server session that acts as the connection between them in the two sub-protocols \(\mathrm {\Pi }_1\) and \(\mathrm {\Pi }_2\).^{Footnote 7}

More detailed, when is an initiator session having intended peers B (responder) and S (server), then:

• if,

  1. 1.

     and ,

  2. 2.

     ,

  3. 3.

     (in particular, this means that received the same identities that sent on the A-S link Fig. 5),

• , otherwise.

When is a responder session having intended peers A and S, then \(f_3\) is defined similarly by “reversing” the order of \(f_1\) and \(f_2\):

• if,

  1. 1.

     and ;

  2. 2.

     ,

  3. 3.

     ,

• , otherwise.

Soundness. The soundness of \(f_3\) follows from the soundness of \(f_1\) and \(f_2\), the ACCE-security of protocol \(\mathrm {\Pi }_2\) (specifically, its channel integrity), together with the fact that \(\mathsf {PRF}\) is deterministic. The proof is given in the full version.

AKE \(^w\) -Security. The proof of AKE\(^w\)-security of protocol \(\mathrm {\Pi }_3\) is structured as a sequence of games. In the following, when we say that a certain game aborts, we mean that the challenger stops the execution of the experiment and outputs a random bit on \(\mathcal {A}\)’s behalf.

Game 0: This is the real 3P-AKE\(^w\) security game, hence

Game 1: This game proceeds as the previous one, but aborts if a fresh responder or trusted server session accepts maliciously in sub-protocol \(\mathrm {\Pi }_2\), meaning that it accepted without a partner in \(\mathrm {\Pi }_2\) according to \(f_2\).

Lemma 1

Proof

(Sketch). Reduction \(\mathcal {B}_1\) begins by creating all the long-term keys for sub-protocol \(\mathrm {\Pi }_1\) and selecting a random bit b. Essentially, \(\mathcal {B}_1\) will simulate the \(\mathrm {\Pi }_1\) part of \(\mathrm {\Pi }_3\) itself, while forwarding all messages pertaining to \(\mathrm {\Pi }_2\) to its 2P-ACCE challenger. In particular, \(\mathcal {B}_1\) creates all the intermediate keys \(k_{AS}\) itself, and from them derive the session keys \(k_{AB}\). In order to create the \(C_{\mathrm {key}}\) message of some trusted server session \(\pi \), \(\mathcal {B}_1\) issues an \(\mathsf {Encrypt}(\pi , k_{AB}, k_{AB})\) query to its own ACCE experiment. Moreover, when \(\mathcal {A}\) issues a \(\mathsf {Test}\) query, then depending on bit b, \(\mathcal {B}_1\) returns the real session key or a random key. When \(\mathcal {A}\) terminates, then \(\mathcal {B}_1\) terminates too (in this case no malicious accept has occurred).

To analyze \(\mathcal {B}_1\)’s winning probability, we only have to observe that \(\mathcal {B}_1\) provides a perfect simulation of \(\mathrm {\Pi }_3\) for \(\mathcal {A}\). This means that if a malicious accept occurs in sub-protocol \(\mathrm {\Pi }_2\), then a malicious accept also occurs in \(\mathcal {B}_1\)’s ACCE experiment.

   \(\square \)

Remark 8

Note that the abort condition in Game 1 does not mean that every session in protocol \(\mathrm {\Pi }_3\) will have a partner (according to \(f_3\)). In fact, all the initiator sessions in protocol \(\mathrm {\Pi }_3\) will accept without a partner.

Game 2: This game proceeds as the previous one, but it aborts if a fresh responder session accepts on receiving a \(C_{\mathrm {key}}\) message that was not legitimately produced by its partner in \(\mathrm {\Pi }_2\).

Lemma 2

Proof

(Sketch). \(\mathcal {B}_2\) works exactly like algorithm \(\mathcal {B}_1\) in the previous proof, but it also simulates the abort on malicious accept. This simulation is possible because the partnering function \(f_2\) is based on the public transcript \(T_2\). It only remains to argue that the new abort event of Game 2 implies a forgery in \(\mathcal {B}_2\)’s ACCE experiment. This amounts to showing that if a session in \(\mathrm {\Pi }_3\) is fresh according to \(\mathsf {Fresh}_{\mathsf {AKE^w}}\), then the corresponding session in \(\mathrm {\Pi }_2\) is fresh according to \(\mathsf {Fresh}_{\mathsf {ACCE}}\). But this is true because the \(\mathsf {Fresh}_{\mathsf {AKE^w}}\) predicate is more restrictive than the \(\mathsf {Fresh}_{\mathsf {ACCE}}\) predicate.    \(\square \)

Game 3: In this game the challenger tries to guess the test-session chosen by \(\mathcal {A}\), together with its eventual partner (if any). If the guess is wrong, or if \(\mathcal {A}\) violates the freshness of the guessed test-session, the challenger aborts with a random output. Technically, the challenger proceeds as follows.

For \(m \le n\), let \([m,n] \overset{\mathrm {def}}{=}\lbrace m, m+1, \cdots n \rbrace \). First, the challenger randomly guesses the test-session , where is an upper bound on the number of sessions at each party. Then, depending on the role of U, the challenger either guess or as the expected partner of (U, i), where a pick of \(j=0\) means that (U, i) is not expected to get any partner session at its peer V. Finally, the challenger aborts by outputting a random bit if either of the following bad event occurs:

1. (i)

   (U, i) was not selected as the test-session by \(\mathcal {A}\).

2. (ii)

   (U, i) was guessed to be without a partner, but gets one.

3. (iii)

   (U, i) was guessed to have a partner, but either gets none or someone different from (V, j).

4. (iv)

   \(\mathcal {A}\) makes a \(\mathsf {Reveal}\) or \(\mathsf {Corrupt}\) query that would make (U, i) unfresh.

Lemma 3

Proof

The occurrence of the bad events is independent from \(\mathcal {A}\)’s view up to the moment of where the bad event occurs. When none of the bad events occurs, then \(\mathcal {A}\)’s success probability is the same in \(G_{2}\) and \(G_{3}\), and the challenger guesses the right (pair of) session(s) with probability at least . And if a bad event occurs, then \(\mathcal {A}\) wins \(G_3\) with probability at least 1 / 2.    \(\square \)

In the remaining games, let denote the guessed test-session, and let denote its expected partner. Define the co-partner of \(\pi ^*\) to be the trusted server session being involved in the protocol run between \(\pi ^*\) and \(\pi '\). Specifically, if \(\pi ^*\) is an initiator, then its co-partner is defined to be \( f_{1,T_1}(\pi ^*)\); while if \(\pi ^*\) is a responder, then its co-partner is defined to be \(f_{2,T_2}(\pi ^*)\).

Game 4: This game proceeds as the previous one, except that it swaps out the intermediate key \(k_{AS}\) derived in sub-protocol \(\mathrm {\Pi }_1\) with a random key for the guessed initiator session (either \(\pi ^*\) or \(\pi '\)) and its co-partner (if any).

Lemma 4

Proof

(Sketch). Reduction \(\mathcal {B}_3\) begins by drawing a random bit b and creates all the long-term PSKs for sub-protocol \(\mathrm {\Pi }_2\). It also guesses the sessions \(\pi ^*\) and \(\pi '\) as in Game 3. \(\mathcal {B}_3\) then runs \(\mathcal {A}\) and forwards all of its queries pertaining to sub-protocol \(\mathrm {\Pi }_1\) to its own AKE experiment, while all queries pertaining to sub-protocol \(\mathrm {\Pi }_2\) reduction \(\mathcal {B}_3\) answers itself using the PSKs it created. It also implements all the abort conditions of the previous games. To answer \(\mathcal {A}\)’s \(\mathsf {Test}(\pi ^*)\) query, \(\mathcal {B}_3\) does the following. If \(b = 1\) then it responds with a random key as normal. If \(b = 0\) and \(\pi ^*\) is an initiator session, then \(\mathcal {B}_3\) forwards \(\mathcal {A}\)’s \(\mathsf {Test}(\pi ^*)\) query to its own AKE game to obtain \(\pi ^*\)’s intermediate key \(k_{AS}\) in sub-protocol \(\mathrm {\Pi }_1\). \(\mathcal {B}_3\) then uses \(k_{AS}\) to derive the session key \(k_{AB}\) which it returns to \(\mathcal {A}\). If \(b = 0\) and \(\pi ^*\) is a responder session, then by our abort conditions, \(\pi ^*\) must have a co-partner by Game 1. To obtain the intermediate key \(k_{AS}\) needed to derive \(k_{AB}\), \(\mathcal {B}_3\) queries to its own AKE experiment and returns \(k_{AB}\) to \(\mathcal {A}\). When \(\mathcal {A}\) outputs its guess \(b'\), then \(\mathcal {B}_3\) stops and outputs 0 if \(b = b'\), and 1 otherwise.

Note that if the test-query in \(\mathcal {B}_3\)’s own AKE experiment returns real keys \(k_{AS}\), then \(\mathcal {B}_4\) perfectly simulates Game 3, while if it returns random keys then \(\mathcal {B}_3\) simulates Game 4. However, we still need to argue that the test-session chosen in \(\mathcal {B}_3\)’s experiment is fresh. If \(\pi ^*\) is an initiator session then \(\mathcal {B}_3\) also uses \(\pi ^*\) as the test-session in its own AKE experiment, hence it is fresh since the predicate \(\mathsf {Fresh}_{\mathsf {AKE}^w}\) is more restrictive than \(\mathsf {Fresh}_{\mathsf {AKE}}\). If \(\pi ^*\) is a responder session, then the test-session chosen by \(\mathcal {B}_3\) is \(\pi ^*\)’s co-partner , so we need to argue that is fresh in \(\mathcal {B}_3\)’s AKE experiment. There are two cases to consider: either \(\pi ^*\) has an \(f_3\)-partner or it does not. If \(\pi ^*\) does have a partner (which by Game 3 must be \(\pi '\)), then \(\mathcal {A}\) cannot have made any \(\mathsf {Reveal}(\pi ')\) queries since this would violate the AKE\(^w\)-freshness of \(\pi ^*\). Moreover, since \(f_3\) is constructed from \(f_1\) and \(f_2\), \(\pi '\) must be ’s \(f_1\)-partner. Thus, \(\mathcal {B}_3\) is also allowed to forward any \(\mathsf {Corrupt}\) query to either A or S without violating the freshness of according to \(\mathsf {Fresh}_{\mathsf {AKE}}\). If \(\pi ^*\) does not have an \(f_3\)-partner, then \(\mathcal {A}\) cannot have made any \(\mathsf {Corrupt}\) query to A or S (since this would violate AKE\(^w\)-freshness), and thus neither has \(\mathcal {B}_3\). Moreover, if \(\pi ^*\) does not have an \(f_3\)-partner then in particular its co-partner cannot have an \(f_1\)-partner. Thus, \(\mathcal {B}_3\) can safely forward all of \(\mathcal {A}\)’s \(\mathsf {Reveal}\) queries without violating the AKE-freshness of .    \(\square \)

Game 5: This game proceeds as the previous one, except that when deriving the session key \(k_{AB}\) for the guessed initiator session (either \(\pi ^*\) or \(\pi '\)) and its co-partner (if it exists), the challenger uses a random function \(\$(\cdot , \cdot )\) rather than \(\mathsf {PRF}(k_{AS}, \cdot , \cdot )\).

Lemma 5

Proof

Algorithm \(\mathcal {D}\) has access to an oracle \(\mathcal {O}\) which either implements the function \(\mathsf {PRF}(\widetilde{k}, \cdot , \cdot )\) with an independent and uniformly distributed key \(\widetilde{k}\), or a random function \(\$(\cdot , \cdot )\). \(\mathcal {D}\) begins by drawing a random bit b and creates all the long-term keys for sub-protocols \(\mathrm {\Pi }_1\) and \(\mathrm {\Pi }_2\). Next, it runs \(\mathcal {A}\) and answers all its queries according to Game 4 by using the keys it created, except that it answers \(\mathcal {A}\)’s \(\mathsf {Test}(\pi ^*)\) query as follows. If \(b=1\), then \(\mathcal {D}\) returns a random key. If \(b=1\), then \(\mathcal {D}\) answers as follows. If \(\pi ^*\) is an initiator session, then \(\mathcal {D}\) answers with \(\mathcal {O}(U,V)\) (recall that and ). If \(\pi ^*\) is a responder session, then \(\mathcal {D}\) answers with \(\mathcal {O}(V', U')\), where \(V'\) and \(U'\) were the identities that the co-partner of \(\pi ^*\) received over the initiator-server link in Fig. 5 (recall that if \(\pi ^*\) is a responder session it is guaranteed to have a co-partner by Game 1). When \(\mathcal {A}\) outputs its guess \(b'\), then \(\mathcal {D}\) stops and outputs 0 if \(b = b'\), and 1 otherwise.

When \(\mathcal {D}\)’s oracle \(\mathcal {O}\) implements \(\mathsf {PRF}\), then \(\mathcal {D}\) perfectly simulates Game 4, while if \(\mathcal {O}\) implements a random function \(\$(\cdot ,\cdot )\), then \(\mathcal {D}\) perfectly simulates Game 5. Thus, the advantage difference of \(\mathcal {A}\) winning in Game 4 and Game 5 corresponds exactly to the probability difference that \(\mathcal {D}\) outputs 1 when interacting with \(\mathsf {PRF}\) or a random function \(\$(\cdot ,\cdot )\) as its oracle \(\mathcal {O}\).    \(\square \)

Note that by the change in Game 5, the session key of \(\pi ^*\) and \(\pi '\) is derived using a random function rather then the pseudorandom function \(\mathsf {PRF}\). In the following, let \(\widetilde{k_{AB}}\) denote the session key derived in this manner at the co-partner of \(\pi ^*\) (if it exists).

Game 6: This game proceeds as the previous one, but when creating the \(C_{\mathrm {key}}\) message of the co-partner of \(\pi ^*\), the challenger encrypts the “dummy” string \(0^\lambda \) instead of the session key \(\widetilde{k_{AB}}\). If this \(C_{\mathrm {key}}\) message is eventually delivered to the intended responder session (either \(\pi ^*\) or \(\pi '\)), then its session key is still set to \(\widetilde{k_{AB}}\) however.

Lemma 6

Proof

(Sketch). Reduction \(\mathcal {B}_4\) begins by drawing a random bit b and creates all the long-term keys for sub-protocol \(\mathrm {\Pi }_1\). It also guesses the sessions \(\pi ^*\) and \(\pi '\) as in Game 3, and implements all of the abort conditions introduced so far. All of \(\mathcal {A}\)’s queries pertaining to sub-protocol \(\mathrm {\Pi }_1\) \(\mathcal {B}_4\) answers itself using the long-term keys it created, while queries pertaining to sub-protocol \(\mathrm {\Pi }_2\) \(\mathcal {B}_4\) forwards to its own ACCE experiment. In particular, \(\mathcal {B}_4\) creates the \(C_{\mathrm {key}}\) message of a server session as follows.

If is not the co-partner of the test-session \(\pi ^*\), then \(\mathcal {B}_4\) makes the query to its ACCE experiment, where “A” is the identity of the initiator that \(\pi \) received on the A-S link in Fig. 5, and \(k_{AB}\) is the session key \(\mathcal {B}_4\) derived from \(\pi \)’s intermediate key \(k_{AS}\) in sub-protocol \(\mathrm {\Pi }_1\). The returned ciphertext is used as the \(C_{\mathrm {key}}\) message of . If \(\pi \) is the co-partner of \(\pi ^*\), then \(\mathcal {B}_4\) instead makes the query to create \(C_{\mathrm {key}}\).

Finally, when \(\mathcal {A}\) outputs its guess \(b'\), then \(\mathcal {B}_4\) outputs the following to its ACCE experiment. If the test-session \(\pi ^*\) has a co-partner , then \(\mathcal {B}_4\) outputs if \(b = b'\) and otherwise. If the test-session does not have a co-partner, then \(\mathcal {B}_4\) simply outputs an arbitrary session together with a random bit.

Note that if the test-session does not have a co-partner then there is no difference between Game 5 and Game 6, and \(\mathcal {B}_4\) perfectly simulates it. If the test-session has a co-partner , and in \(\mathcal {B}_4\)’s ACCE experiment, then \(\mathcal {B}_4\) perfectly simulates Game 5 (since the \(C_{\mathrm {key}}\) message of is an encryption of the actual session key \(k_{AB}\)). On the other hand, if then \(\mathcal {B}_4\) perfectly simulates Game 6 (since the \(C_{\mathrm {key}}\) message of is an encryption of \(0^{\lambda }\)). What remains to show that is fresh in \(\mathcal {B}_4\)’s ACCE experiment, i.e., that is fresh according to predicate \(\mathsf {Fresh}_{\mathsf {ACCE}}\).

Suppose first that the test-session \(\pi ^*\) is a responder. This is where we will use the assumption that the partner function \(f_2\) for sub-protocol \(\mathrm {\Pi }_2\) is symmetric. By Game 1 \(\pi ^*\) has a co-partner , and by the symmetry of \(f_2\) we also have . It follows that is fresh according to \(\mathsf {Fresh}_{\mathsf {ACCE}}\) (note that since \(\mathcal {B}_4\) makes no \(\mathsf {Reveal}\) query to in its ACCE experiment, we only have to consider the exposure of its PSK).

Now suppose the test-session is an initiator. There are two cases to consider: either \(\pi ^*\) has an \(f_3\)-partner or it does not have an \(f_3\)-partner. If \(\pi ^*\) has an \(f_3\)-partner \(\pi '\), then by the construction of \(f_3\) from \(f_1\) and \(f_2\), we have in particular that . Again, this implies that is fresh according to \(\mathsf {Fresh}_{\mathsf {ACCE}}\). Conversely, if \(\pi ^*\) does not have an \(f_3\)-partner, then none of the long-term keys and PSKs of its peers can be exposed if \(\pi ^*\) is to be fresh according to \(\mathsf {Fresh}_{\mathsf {AKE^w}}\). In particular, this means that the long-term PSK of must be unexposed. Thus, is fresh according to \(\mathsf {Fresh}_{\mathsf {ACCE}}\) (this is regardless of whether it has an \(f_2\)-partner or not).    \(\square \)

Concluding the Proof of Theorem 1. We argue that \(\mathsf {Adv}_{\mathrm {\Pi }_3,\mathcal {A},f_3}^{\mathsf {G_6}}(\lambda )=0\). By the change in Game 5, the session key of the test-session \(\pi ^*\) is derived using a random function \(\$(A, B)\), where “A” and “B” are the identities of the initiator and responder that \(\pi ^*\) believes took part in this protocol run. We claim that the only other session that holds a session key derived from \(\$(\cdot , \cdot )\) using the same identities “A” and “B”, is \(\pi ^*\)’s partner \(\pi '\) (if it exists).

First, note that the random function is evaluated for at most two sessions: one initiator session and one server session. Second, the session key derived by the server session is delivered to at most one responder session. Finally, the identities used to evaluate \(\$(\cdot , \cdot )\) at the initiator and server might be different since the adversary can modify the communicated identities at the A-S link in Fig. 5.

However, if the adversary modifies these identities, then the initiator and server derive independent keys, which ultimately means that the initiator and responder will have independent keys too. Moreover, the initiator and responder sessions will not be partners since the communicated identities at the S-B link in Fig. 5 will be different too (recall that \(f_3\)-partnering includes the sessions’ recorded peers, and by Game 2 the adversary is unable to change the \(C_{\mathrm {key}}\) message). On the other hand, if the identities were the same, then the initiator and responder session would necessarily be \(f_3\)-partners. This follows because the initiator has the server session as its co-partner (in sub-protocol \(\mathrm {\Pi }_1\)), and the server session’s \(C_{\mathrm {key}}\) message is only delivered to its co-partner (in sub-protocol \(\mathrm {\Pi }_2\)). Combined with their agreement on their peers, this means that they would be partners by the definition of \(f_3\).

Altogether, since the session key of the test-session is derived using an independent random function, and since the corresponding \(C_{\mathrm {key}}\) message leaks nothing about the session key by Game 6, the adversary has zero advantage in Game 6 as claimed. Combining all the lemmas yields the theorem.    \(\square \)

Note that the conclusion above only holds because of the channel binding. In particular, if the identities of A and B did not go into to the evaluation of the pseudorandom function \(\mathsf {PRF}\), then \(\mathrm {\Pi }_3\) would be vulnerable to a simple UKS attack: just change the responder identity sent over the (unauthenticated) A-S link from B to \(B'\). Without channel binding, A and \(B'\) obtain the same session key but disagree on their intended peers.

3.2 3P-AKE\(^{w}\) + 2P-AKE \(\implies \) 3P-AKE

Construction. From a 3P-AKE protocol \(\mathrm {\Pi }_3\) and a 2P-AKE protocol \(\mathrm {\Pi }_4\), we construct the 3P-AKE protocol \(\mathrm {\Pi }_5\) shown in Fig. 5. Specifically, protocol \(\mathrm {\Pi }_5\) works as follows. First, sub-protocol \(\mathrm {\Pi }_3\) is run between A, B and S in order to establish an intermediate “session key” \(K_{\mathrm {\Pi }_3}\). Then, sub-protocol \(\mathrm {\Pi }_4\) is run between A and B using \(K_{\mathrm {\Pi }_3}\) as the their shared “long-term key”. The session key derived in \(\mathrm {\Pi }_4\) becomes A and B’s final session key in \(\mathrm {\Pi }_5\).

Result. Our second composition result shows that protocol \(\mathrm {\Pi }_5\) is 3P-AKE-secure if sub-protocol \(\mathrm {\Pi }_3\) is 3P-AKE\(^w\)-secure and sub-protocol \(\mathrm {\Pi }_4\) is 2P-AKE\(^{\mathsf {static}}\)-secure with explicit entity authentication. We remark that the last requirement is necessary in order for our proof to go through. In fact, \(\mathrm {\Pi }_5\) inherits the property of explicit entity authentication from sub-protocol \(\mathrm {\Pi }_4\). On the other hand, while \(\mathrm {\Pi }_4\) does not achieve forward secrecy on its own, protocol \(\mathrm {\Pi }_5\) does. The reason is that within \(\mathrm {\Pi }_5\), sub-protocol \(\mathrm {\Pi }_4\) is merely used to upgrade the security of \(\mathrm {\Pi }_3\), which does provide forward secrecy (albeit limited).

Theorem 2

Let \(\mathrm {\Pi }_5\) be the protocol described in Sect. 3.2. If protocol \(\mathrm {\Pi }_3\) is 3P-AKE\(^w\)-secure and protocol \(\mathrm {\Pi }_4\) is 2P-AKE\(^{\ \mathsf {static}}\)-secure with explicit entity authentication, then there exists a partner function \(f_5\) such that protocol \(\mathrm {\Pi }_5\) is 3P-AKE-secure.

Concretely, for partner functions \(f_3\) and \(f_4\), we can create a partner function \(f_5\), and adversaries \(\mathcal {B}_1\), \(\mathcal {B}_2\) and \(\mathcal {B}_3\), such that

where is an upper bound on the number of sessions at each party.

The proof of Theorem 2 is very similar to that of Theorem 1 and is provided in the full version.

4.1 EAP with Channel Binding

In this section we explore the security guarantees provided by EAP. As mentioned in the introduction, there is no single definitive version of EAP which we can use for this purpose, because the specification itself (RFC 3748 [4]) leaves many of its components undefined. Thus, any analysis of EAP will have to make assumptions on these components.

In Theorem 1, let us identify sub-protocol \(\mathrm {\Pi }_1\) with the EAP method run between the client and the trusted server. Let sub-protocol \(\mathrm {\Pi }_2\) be the key-transport protocol run between the server and the authenticator. Finally, suppose that EAP employs the channel binding mechanism defined in [25]. Then we immediately get the following result for EAP.

Theorem 3

(3P-AKE \(^{w}\) security of EAP). If the chosen EAP method used within EAP is 2P-AKE-secure, the key-transport protocol is 2P-ACCE-secure, and the employed key derivation function is a secure PRF that provides channel binding on the client’s and authenticator’s identities, then EAP is 3P-AKE\(^w\)-secure.

To be even more concrete, we can also instantiate sub-protocols \(\mathrm {\Pi }_1\) and \(\mathrm {\Pi }_2\) with some actual protocols. For example, Brzuska et al. [12] recently showed that the EAP-TLS method constitutes a secure 2P-AKE protocol, thus satisfying the requirements on sub-protocol \(\mathrm {\Pi }_1\). For sub-protocol \(\mathrm {\Pi }_2\) we take RADIUS-over-TLS [30], which then reduces to the security of TLS. Multiple papers [9, 16, 18, 20, 23] have shown TLS to be a secure 2P-ACCE protocol. Hence, RADIUS-over-TLS fulfills the requirement on sub-protocol \(\mathrm {\Pi }_2\).

4.2 Channel-Binding Scope

In Theorems 1, and 3, we assumed that the channel binding mechanism included the identity of the client and the authenticator in order to bind the identities cryptographically to the session key. Implicitly, this also assumes that all identities are globally unique and belong to the same namespace. This is a standard assumption when doing cryptographic modeling. However, in reality, the various links in EAP take place over different types of communication media with different types of identities and addressing schemes. For instance, in IEEE 802.11 with upper-layer authentication, the communication between the client and the access point is based on link-layer addresses, the communication between the client and the server is typically based on usernames (client) and domain names (server), while the communication between the server and the access point might be based solely on IP addresses. Mapping between these identifiers is not always straightforward (see [15]). In fact, some of the identifiers might not even be available to all the protocol participants. Specifically, since the communication between the client and the access point happens at the link-layer, the IP addresses used by the access point towards the server might not be available to the client unless the access point broadcasts it. In practice, most link-layer protocols have facilities for providing this kind of information to the client^{Footnote 8}, but there is no guarantee that the authenticator will actually provide it.

Moreover, in some settings this information may not even be relevant. For example, in a WLAN supported by many access points, the client might not care about which specific access point it connects to, as long as it connects to a legitimate access point of that WLAN. Thus, in this case the granularity of the channel-binding should not be at the individual access point level, but rather at the WLAN level, defined by all the access points broadcasting the same network identifier (SSID). However, in this case the security guarantees provided by the channel-binding will be weaker. Specifically, when channel-binding occurs at the individual level, then the corruption of a single access point will not influence clients connecting to access points having a different identity. On the other hand, when channel-binding occurs at the network level, then a single corrupted access point will affect all connections within that network. In this case, the channel binding only protects connections occurring in networks having a different SSID.

More generally, the information included in the channel-binding defines the scope of the protection it provides, and can include more than just identities. For instance, physical media types, data rates, cost-information, channel frequencies, etc., can all be used as input to the channel-binding. The specifications for channel-binding within EAP [14, 25] leaves open exactly the kind of information that should go into the binding, because the amount of information that will be available to both the client and the server can vary.

4.3 EAP Without Channel Binding

Without channel binding, it suffices to compromise a single access point in order to compromise an entire network. As access points are typically not highly protected devices, this is a substantial attack vector on enterprise networks. Even if the channel binding only included the network name, it would clearly be an upgrade over EAP without channel binding, and comes at essentially no cost. The situation in the AKA protocol used in the UMTS and LTE mobile networks is similar. The AKA protocol is similarly structured as the EAP protocol^{Footnote 9}, where a mobile client that wants to connect to a base station first has to authenticate to its home operator. So-called authentication vectors, which in particular includes a session key, are then forwarded from the operator to the base station in much the same way as the server forwards the session key to the authenticator in EAP. Moreover, similar to many EAP methods, the AKA protocol too lacks channel-binding for its authentication vectors. In their recent analysis of the AKA protocol, Alt et al. [5] noted (Sect. 5) this lack of channel-binding, and suggested a fix identical to the key-derivation approach analyzed in this paper.

5.1 Description of the IEEE 802.11 Protocol

IEEE 802.11 [2] is the most widely used standard for creating WLANs. It supports three modes of operation depending on the network topology: infrastructure mode, ad-hoc mode, and mesh network mode. In ad-hoc mode and mesh-networking mode there is no central infrastructure, and the wireless clients talk directly to each other. On the other hand, in infrastructure mode the clients only communicate through an access point (AP), which provides connectivity to a larger WAN. In this paper we only cover IEEE 802.11 in infrastructure mode, which is by far the most common mode.

The IEEE 802.11 protocol is a layer 2 protocol, aiming to secure the wireless link between the client and the AP. It defines two main security protocols: the 4-Way-Handshake (4WHS), used to authenticate and establish session keys between the client and the AP; and the Counter Mode CBC-MAC protocol (CCMP), used to secure the actual application data. We will only cover the 4WHS in this paper.

The 4WHS is based on a symmetric Pairwise Master Key (\(\mathrm {PMK}\)), shared between the client and the AP. The analysis of IEEE 802.11 will therefore crucially depend on how this \(\mathrm {PMK}\) is obtained. In Sect. 5.2 we will analyze the 4WHS when the \(\mathrm {PMK}\) is simply taken for granted, i.e., the \(\mathrm {PMK}\) is a pre-shared key. This is already quite significant on its own because it corresponds to the setting found in virtually every wireless home-network. Still, in most enterprise and university environments, the \(\mathrm {PMK}\) is not a pre-shared key, but is rather distributed to the client and AP through some upper-level authentication mechanism involving a mutually trusted server. While technically outside the scope of the IEEE 802.11 standard, the de-facto protocol for this is EAP. The analysis of IEEE 802.11 with upper-level authentication is the topic of Sect. 5.3.

5.2 Analyzing the 4-Way-Handshake

The 4WHS is shown in Fig. 6. It depends on a pseudorandom function \(\mathsf {PRF}\) and a MAC scheme \(\varSigma = (\mathsf {kg}, \mathsf {MAC}, \mathsf {Vrfy})\). Identities are based on the parties’ 48-bit link-layer addresses. This makes it possible to compare the parties’ identities based on their corresponding numerical values. Particularly, the functions \(\max \lbrace A,B \rbrace \) and \(\min \lbrace A,B \rbrace \) returns, respectively, the largest and the smallest of two link-layer addresses A and B. We use the notation \([x]_k \overset{\mathrm {def}}{=}x \Vert \sigma \) to denote a message x together with its MAC tag \(\sigma \), computed with \(\varSigma .\mathsf {MAC}\) and key k.

The 4WHS begins with the AP sending the message \(m_1 = \eta _{AP} \Vert p_1\) to the client C, where \(\eta _{AP}\) is a nonce and \(p_1\) is some auxiliary information included in the IEEE 802.11 packet.

On receiving \(m_1\), C generates its own nonce \(\eta _C\) and derives a key \(\mathrm {PTK}= k_\mu \Vert k_\alpha \leftarrow \mathsf {PRF}_K(P \Vert \eta )\) using the pseudorandom function \(\mathsf {PRF}\) and the long-term key it shares with AP. Here \(P \Vert \eta = \min \lbrace AP, C \rbrace \Vert \max \lbrace AP, C \rbrace \Vert \min \lbrace \eta _{AP},\eta _C \rbrace \Vert \max \lbrace \eta _{AP}, \eta _C \rbrace \). The sub-key \(k_\alpha \) will be the session key output by the 4WHS, while \(k_\mu \) will be used by the MAC scheme \(\varSigma \) to protect the handshake messages. After deriving \(\mathrm {PTK}\), C creates and sends the next protocol message \(m_2 = [\eta _C \Vert p_2]_{k_\mu }\).

On receiving \(m_2 = [\eta _C \Vert p_2]_{k_\mu }\), AP uses the containing nonce \(\eta _C\) to derive the keys \(\mathrm {PTK}= k_\mu \Vert k_\alpha \leftarrow \mathsf {PRF}_K(P \Vert \eta )\). Using \(k_\mu \) as the key, it verifies the integrity of \(m_2\) with the MAC scheme \(\varSigma .\mathsf {Vrfy}\). If the verification goes through, AP creates and send the third protocol message \(m_3 = [\eta _{AP} \Vert p_3]_{k_\mu }\).

On receiving \(m_3\), C first verifies it using the MAC key \(k_\mu \). If the check goes through, it sends out the final handshake message \(m_4 = [p_4]_{k_\mu }\). Additionally, it sets its own acceptance state to \(\alpha = \mathsf {accepted}\). Once AP receives and verifies \(m_4\), it sets its acceptance status to \(\alpha = \mathsf {accepted}\) too.

Remark 9

The fourth handshake message \(m_4\) serves no cryptographic purpose and could safely have been omitted. However, to stay true to the actual 4WHS, we leave it in.

In the following analysis, let \(\mathcal {P}_{AP} = \mathcal {I}\) and \(\mathcal {P}_{C} = \mathcal {R}\), i.e., in the 4WHS protocol APs are the initiators and the clients are the responders.

Theorem 4

The 4WHS protocol is AKE\(^{\ \mathsf {static}}\)-secure. In particular, for any PPT adversary \(\mathcal {A}\), there exists a partner function f and algorithm \(\mathcal {D}\), such that

where is the number of sessions at each party, and \({n_{P}}= |\mathcal {P}_C | + |\mathcal {P}_{AP}|\).

For this protocol it is natural to use SIDs as our partnering mechanism. However, because our paper is phrased in terms of partnering functions, we “synthetically” encode the SID as a partnering function by saying that the partner session is the first other session that gets the same SID \(P \Vert \eta \). Taking the first one is important because a partner function is a function and not a relation.

Proof

Suppose \(P \Vert \eta = \min \lbrace U, V \rbrace \Vert \max \lbrace U, V \rbrace \Vert \min \lbrace \eta _{U},\eta _V \rbrace \Vert \max \lbrace \eta _{U}, \eta _V \rbrace \) was the string that input to its pseudorandom function \(\mathsf {PRF}\). Then is defined to be the first session at V that input the same string \(P \Vert \eta \) to its \(\mathsf {PRF}\). Note that this can be computed based on publicly available transcript information.

Soundness. The soundness of f is immediate from its definition and \(\mathsf {PRF}\) being deterministic.

AKE \(^{\mathsf {static}}\) -Security.

Game 0: This is the real 2P-AKE security game, hence

Game 1: This game proceeds as the previous one, but aborts if not all the nonces in the game are distinct, hence

Game 2: In this game the challenger guesses the pre-shared key that will be used by the test-session and aborts if that guess was wrong, hence

Let \(\mathrm {PMK}^*\) denote the guessed pre-shared key. Note that by the \(\mathsf {Fresh}_{\mathsf {AKE^{static}}}\) requirement (Fig. 3), \(\mathrm {PMK}^*\) cannot be exposed.

Game 3: In this game the challenger replaces the pseudorandom function \(\mathsf {PRF}\) with a random function \(\$(\cdot )\) in all evaluations using the guessed pre-shared key \(\mathrm {PMK}^*\). That is, calls of the form \(\mathsf {PRF}(\mathrm {PMK}^*,\cdot )\) are instead answered by \(\$(\cdot )\).

Lemma 7

\(\mathsf {Adv}_{\mathsf {4WHS},\mathcal {A},f}^{\mathsf {G_{2}}}(\lambda ) \le \mathsf {Adv}_{\mathsf {4WHS},\mathcal {A},f}^{\mathsf {G_{3}}}(\lambda ) + \mathsf {Adv}_{\mathsf {PRF},\mathcal {D}}^{\mathsf {prf}}(\lambda ) .\)

Proof

Algorithm \(\mathcal {D}\) has access to an oracle \(\mathcal {O}\), which either implements the function \(\mathrm {\Pi }.\mathsf {PRF}(\widetilde{\mathrm {PMK}}, \cdot )\) for some independently and uniformly distributed key \(\widetilde{\mathrm {PMK}}\), or it implements a truly random function \(\$(\cdot )\). \(\mathcal {D}\) begins by choosing a random bit b and guessing a client-AP pair (C, AP). All computations that would normally involve the pre-shared key of C and AP, algorithm \(\mathcal {D}\) will instead forward to its oracle \(\mathcal {O}\). For all other client-AP pairs, \(\mathcal {D}\) creates their the pre-shared keys itself, allowing it to simulate them perfectly. If \(\mathcal {A}\) outputs \(b'\), then \(\mathcal {D}\) outputs 1 if \(b=b'\), and 0 otherwise.

When \(\mathcal {O} = \mathrm {\Pi }.\mathsf {PRF}(\widetilde{\mathrm {PMK}}, \cdot )\), then \(\mathcal {D}\) perfectly simulates Game 2 since the \(\mathrm {PMK}\)s are chosen independently and uniformly at random; while when \(\mathcal {O} = \$(\cdot )\), then \(\mathcal {D}\) perfectly simulates Game 3.    \(\square \)

Concluding the Proof of Theorem 4. Suppose the test-session in Game 3 accepted with the “SID” \(P \Vert \eta \). By Game 1 we know that the only sessions that evaluated the pseudorandom function on this SID was the test-session and possibly its partner. However, by Game 3 the PRF is now a truly random function unavailable to the adversary (since we are in the static corruption model). In particular, this means that the \(\mathrm {PTK}\) derived by the test-session (and possibly its partner) is a truly random string \(\widetilde{\mathrm {PTK}} = \widetilde{k_\mu } \Vert \widetilde{k_\alpha } \leftarrow \lbrace 0, 1 \rbrace ^{2\lambda }\), and where \(\widetilde{k_\alpha }\) is independent of all other values. Thus, \(\mathsf {Adv}_{\mathsf {4WHS},\mathcal {A},f}^{\mathsf {G_{3}}}(\lambda ) = 0\), and Theorem 4 follows.    \(\square \)

We now turn to proving explicit entity authentication for the 4WHS.

Theorem 5

The 4WHS provides explicit entity authentication. In particular, for any PPT adversary \(\mathcal {A}\), there exists algorithms \(\mathcal {D}\) and \(\mathcal {F}\), such that

where f, , and \({n_{P}}\) are the same as in Theorem 4.

Proof

This proof uses the exact same three game hops as in the proof of Theorem 4, differing only in its interpretation of the guessed pre-shared key \(\mathrm {PMK}^*\): instead of hoping that \(\mathrm {PMK}^*\) belongs to the test-session, we now hope that it belongs to the first session that accepts maliciously. To recap, in Game 3 the challenger aborts if any nonces collide, or the first session that accepts maliciously uses a different pre-shared key then \(\mathrm {PMK}^*\). Moreover, all evaluations of \(\mathsf {PRF}(\mathrm {PMK}^*, \cdot )\) are replaced with a truly random function \(\$(\cdot )\). Since all the game hops are the same, we only have the analyze the probability that a session accepts maliciously in Game 3.

Lemma 8

Proof

The forger \(\mathcal {F}\) has access to two oracles \(\mathcal {O}^{\mathsf {MAC}}\) and \(\mathcal {O}^{\mathsf {Vrfy}}\), which implements the \(\mathsf {MAC}\) and \(\mathsf {Vrfy}\) algorithms of the MAC scheme \(\varSigma \) for some independent random key \(\widetilde{k_\mu }\). Among all the sessions that use \(\mathrm {PMK}^*\), \(\mathcal {F}\) will guess a random session \(\pi ^*\) and embed the oracles \(\mathcal {O}^{\mathsf {MAC}}\) and \(\mathcal {O}^{\mathsf {Vrfy}}\) into it. Let \(V^*\) denote the intended communication partner of \(\pi ^*\). We consider two cases based on whether \(\pi ^*\) is a client or an AP.

Case \(U^* \in \mathcal {P}_{AP}\). \(\mathcal {F}\) will simulate Game 3 by creating all the pre-shared keys and implementing the random function \(\$(\cdot )\) by lazy-sampling. However, when creating and verifying the handshake messages of \(\pi ^*\), it will use the oracles \(\mathcal {O}^{\mathsf {MAC}}\) and \(\mathcal {O}^{\mathsf {Vrfy}}\). Specifically, when receiving the handshake message \(m_2\), \(\pi ^*\) will accept only if \(\mathcal {O}^{\mathsf {Vrfy}}(m_2) = 1\). Moreover, if any session accepts maliciously before \(\pi ^*\), then \(\mathcal {F}\) aborts. Additionally, \(\mathcal {F}\) also aborts if the nonce \(\eta _C\) contained in \(m_2\) was created by a session at \(V^*\) that received the correct nonce \(\eta _{AP}\) from \(\pi ^*\). Note that this event simply means that \(\mathcal {F}\)’s guess of \(\pi ^*\) was wrong, because if \(\pi ^*\) were to accept on receiving this \(m_2\) message, it could not have accepted maliciously by the definition of f, since the session creating \(\eta _C\) would be its partner (here we are also using that all the nonces are unique).

By the uniqueness of nonces, and the assumptions above, no session will evaluate \(\$(\cdot )\) on the same input as \(\pi ^*\). Hence, embedding the oracles \(\mathcal {O}^{\mathsf {MAC}}\), \(\mathcal {O}^{\mathsf {Vrfy}}\) into \(\pi ^*\) provides a perfect simulation of Game 3. But this means that \(\pi ^*\) accepts maliciously iff \(\mathcal {O}^{\mathsf {Vrfy}}(m_2) = 1\), with \(m_2\) being a valid forgery.

Case \(U^* \in \mathcal {P}_{C}\). Similar to the previous case, \(\mathcal {F}\) embeds \(\mathcal {O}^{\mathsf {MAC}}\), \(\mathcal {O}^{\mathsf {Vrfy}}\) into \(\pi ^*\), and aborts if the guess was wrong. This again provides a perfect simulation of Game 3, and \(\pi ^*\) accepts maliciously iff the call to \(\mathcal {O}^{\mathsf {Vrfy}}\) is a valid forgery.

Since in both cases malicious acceptance by \(\pi ^*\) implies a forgery for \(\varSigma \), the lemma follows.    \(\square \)

5.3 Security of IEEE 802.11 with Upper-Layer Authentication

In enterprise and university networks it is both inconvenient and less secure for every user to share a common \(\mathrm {PMK}\) when accessing the WLAN. In these environments, user authentication is instead handled by a central authentication server, which is then accessed via some EAP variant. While the IEEE 802.11 standard technically allows for upper-level authentication mechanisms other than EAP, the de-facto standard is EAP. Since we have already proved that certain variants of EAP satisfies the 3P-AKE\(^w\) notion (Theorem 3), and that the 4WHS is a secure 2P-AKE protocol with static corruption (Theorems 4 and 5); the security of IEEE 802.11 with upper-level authentication now follows directly by applying our second composition theorem (Theorem 2) with and .

Theorem 6

(3P-AKE security of IEEE 802.11 w/upper-layer authentication). If the \(\mathrm {PMK}\) for the 4WHS is derived using a variant of EAP that is 3P-AKE\(^w\)-secure, then the IEEE 802.11 protocol with upper-layer authentication is 3P-AKE-secure.