⎨
⎪⎩
1 if (b =π.b)∧FreshACCE(π) =true 0 if (b =π.b)∧FreshACCE(π) =true b←←{0,1} ifFreshACCE(π) =false
(3.9)
LetExpACCEΠ,Q (A)⇒ddenote the event thatACCE=d. TheACCE advan-tage of an adversaryAis
AdvACCEΠ,f (A)def= 2·Pr[ExpACCEΠ,Q (A)⇒1]−1. (3.10)
3.5 Explicit entity authentication
One can observe the following consequence of our AKE4 security definition. If a fresh session comes to accept a session key, then there can be at most one other session holding the same key, and this session must necessarily be its partner. Why? Suppose not, i.e., assume thatπ andπ accepts the same key but are not partners. If so, then the adversary can reveal one of them, test the other, and trivially break the AKE protocol—contradicting its supposed AKE security. Thus,π and π must either have been partners or not accepted the
4The following applies equally to the ACCE security definition.
same key. By soundness (Definition 3.6), this implies that a fresh session π that accepts a key is assured that this key will be shared by at most one other session π, and that this session will reside at π’s intended peer. However, notice that this authentication property isimplicit in the sense that a session has no guarantee that its partner actually exists. For example, consider the client in EAP: after completing the EAP method with the server, it cannot know whether the subsequent key transfer from the server to the authenticator actually took place (at least without any further communication).
The opposite of implicit authentication is explicit authentication. Here the existence of a partner is guaranteed. Thus, explicit authentication adds the following aliveness property to a protocol. If a session at party A comes to accept, believing it has talked to partyB, then some corresponding (unique) session atB must actually have contributed to this protocol run.
Note that the question of whether explicit (entity) authentication should be considered a requirement of secure AKE protocols is somewhat disputed in the literature (see [BR95, §1.6], [Rog04, §6], and [Kra03, §2.1]). Basically, the argument is that whether or not a partner is actually “out there” is ultimately irrelevant; it is the usage of the key that matters. For instance, even though the EAP client might not have a parter, once it starts using its accepted key, no one except its intended peer will actually be able to communicate with it. Thus, in the bigger picture, it is not so clear what benefits explicit authentication brings over implicit authentication. Consequently, most formal AKE models today do not require explicit entity authentication as a necessary security feature.
Remark 3.11. As opposed to computational AKE protocol models, which mostly treat authentication as an ancillary to the goal of key exchange,symbolic protocol models have historically focused extensively on the goal of authenti-cation itself. As a result, they also have more refined definitions of authentica-tion, including elaborateauthentication hierarchiesthat consist of notions like
“weak-aliveness”, “injective-agreement”, and “non-injective-sync”; see Chap-ter 4 of the book by Cremers and Mauw [CM12]. Our colloquial usage of the term “aliveness” in the preceding paragraph should not be interpreted in the literal sense of these technical notions (although the closest thing would prob-ably be a combination of “weak-aliveness-role” and “injective-agreement”—see
Figure 4.13 in [CM12]).
Within our framework, the notion of explicit entity authentication is inter-changeable with another property called key-confirmation. Key-confirmation is the property that if a session accepts a key, then it is assured that some other session must also have computed the same key (see [Fis+16] for a formal treatment of key-confirmation). Again, it might be debatable how useful this property is in practice, but it nevertheless is the key feature that allows us to
upgrade the security of EAP from weak forward secrecy to full forward secrecy.
For this reason we find it useful to provide a formal definition of explicit en-tity authentication (and hence key-confirmation). However, we stress that the security properties we ultimately aim to satisfy in this thesis are key indistin-guishability (AKE) and channel security (ACCE), as defined by Definition 3.7 and Definition 3.10, respectively. Explicit entity authentication is mostly used as a means to an end in order to achieve these goals.
Since explicit entity authentication is defined identically for AKE and ACCE protocols, we provide a single generic definition here.
Definition 3.12 (Explicit entity authentication). Let M be a security model. Consider a run of experimentExpΠ,Q(A) and fix a partner functionf. A sessionπ is said to haveaccepted maliciously if all of the following hold:
1. π.αF =accepted, 2. FreshM(π) =true, 3. fT(π) =⊥.
LetExpMΠ,Q-EA(A)⇒1 denote the event that a session has accepted maliciously.
TheEA advantageof an adversaryAis
AdvMΠ,f-EA(A)def= Pr[ExpMΠ,Q-EA(A)⇒1], (3.11) whereM∈ {AKE∗,ACCE}.
Note that Definition 3.12 needs to be paired with soundness in order to be meaningful. That is, consider the partner function f that partners each session to itself the moment it is created. For this choice of partner function AdvMΠ,f-EA(A) equals 0 for all adversariesA. Likewise, when we combine explicit entity authentication with, say, AKE security, then we only care about an adversary’s advantage given thesamepartner function for both notions.
Security of EAP
Contents
4.1 Modeling EAP. . . 60 4.1.1 Client–server EAP method . . . 60 4.1.2 Server–authenticator key transport protocol . . . 62 4.1.3 Client–authenticator protocol . . . 63 4.1.4 Related work on EAP . . . 65 4.2 First composition theorem . . . 66 4.3 Second composition theorem. . . 80 4.3.1 Explicit entity authentication . . . 81 4.3.2 AKEfssecurity . . . 86 4.4 Application to EAP . . . 88 4.4.1 EAP without channel binding . . . 89 4.4.2 Channel binding scope . . . 89
In this chapter we analyze the security of EAP using the formal models in-troduced in Chapter 3. However, first we need to precisely define what we mean by EAP and what type of security properties we expect it to provide. Recall from Section 2.1 that EAP is not a single protocol but rather a protocol frame-work which inherently depends on other concrete protocols. As summarized in Figure 2.1, EAP is essentially a composition of three separate protocols:
an EAP method between the client and the server, a key-transport protocol between the server and the authenticator, and a link-layer specific protocol be-tween the client and the authenticator. The EAP standard [RFC3748] is mostly agnostic as to which concrete protocol to actually use for each of these different parts.
59