Second composition theorem

3P-AKE

^wfs

+ 2P-AKE

^nfs

= ⇒ 3P-AKE

^fs

In this section we state and prove our second composition theorem. This result corresponds to the cryptographic core of full EAP.

Construction. From a 3P-AKE protocol Π₃ and a PSK-based 2P-AKE pro-tocol Π₄, we construct the 3P-AKE protocol Π₅ shown in Figure 4.1. Specifi-cally, protocol Π₅works as follows. First sub-protocol Π₃ is run betweenA,B andS in order to establish an intermediate keyK_Π3. Then sub-protocol Π₄ is run betweenA andB usingK_Π3 as the their PSK. The session key derived in sub-protocol Π₄ becomesA andB’s final session key in protocol Π₅.

Result. Our second composition result shows that protocol Π₅ is 3P-AKE secure if sub-protocol Π₃is 3P-AKE^wfssecure and sub-protocol Π₄is 2P-AKE^nfs secure with explicit entity authentication. We remark that the last requirement is necessary in order for our proof to go through. In fact, Π₅ inherits the property of explicit entity authentication from sub-protocol Π₄. Moreover, while Π₄ does not necessarily achieve any forward secrecy on its own, protocol Π₅ does. The reason is that within Π₅, sub-protocol Π₄ is merely used to upgrade the security of Π₃ from weak forward secrecy to full forward secrecy.

For technical reasons, we additionally need to assume some minimal struc-ture on sub-protocol Π₄beyond it being a 2P-AKE protocol. In particular, we require that the probability that two sessions at the same party end up with the same local transcriptτ in sub-protocol Π₄should be “small”. Formally, we demand that the probability of such a transcript collision should be statistically bounded by some function of the number of parties and sessions. This tech-nical requirement is needed in order be able to apply a local partner function to the transcript of sub-protocol Π₄ (see the proof of Claim 4.18).

Theorem 4.12. LetΠ₅be the 3P-AKE protocol constructed from the 3P-AKE protocolΠ₃and 2P-AKE protocolΠ₄as described in the construction above. Let f₃ and f₄ be partner functions, where f₄ is required to be local. Then, for any adversary A in security experiment AKE^fs against protocol Π₅, we can create a partner functionf₅ and algorithmsB1 andB2, such that

Adv^3P_Π5^-_,f^AKE₅ ^fs(A)≤3n²·Adv^3P_Π3^-_,f^AKE₃ ^wfs(B1) + 2n²·Adv^2P_Π4^-_,f^AKE₄ ^nfs(B2) + 2 , (4.21) where n = (n_π + 1)· |I ∪ R|, n_π is the maximum number of sessions that A creates at each party, and = (|I ∪ R|, n_π) is a function that bounds the probability that two sessions at the same party get the same local transcript in protocolΠ₄.

The idea of the proof is as follows. Using that sub-protocol Π₃ is 3P-AKE^wfs secure, we can replace the intermediate key K_Π3 coming out of Π₃ with a random key for the test-session. This then allows us to reduce the 3P-AKE^fs security of protocol Π₅ to the 2P-AKE^nfs of sub-protocol Π₄, since the now random intermediate key of the test-session is identically distributed with the PSKs used in Π₄. The partner functionf₅will be composed out off₃ and f₄, so that two sessions aref₅-partners if and only if they aref₃-partners and f₄-partners.

The main difficulty of the proof lies in the first step, i.e., replacing the intermediate key of the test-session with a random key. The issue is that A plays in a security game that hasfull forward secrecy, whereas the reduction B1to sub-protocol Π₃plays in a security game with onlyweakforward secrecy.

As such,Ais allowed strictly more Corruptqueries than whatB1 can do itself.

The question is howB1 can simulate the 3P-AKE^fs security game for Awhile still keeping the test-session fresh in its own 3P-AKE^wfs security game.

This is where we use that sub-protocol Π₄ provides explicit entity authen-tication. Essentially, it guarantees that the test-session must have a partner in protocol Π₅. By definition of f₅, this implies that it must also have anf₃ -partner in sub-protocol Π₃. But recall from Table 3.1 that when the test-session has a partner, then there is no difference between the AKE^fsand AKE^wfs mod-els! Thus, as long as we can show that the test-session has a partner in protocol Π₅, we are fine. Consequently, we first prove as an initial lemma that protocol Π₅ provides explicit entity authentication.

Proof of Theorem 4.12. We begin by defining the partner function f₅ for pro-tocol Π₅. We construct f₅ from the partner functions f₃ and f₄ given for sub-protocols Π₃ and Π₄ as follows:

f_5,T5(π) =π⇐⇒(f_3,T3(π) =π)∧(f_4,T4(π) =π), (4.22) where T₃ and T₄ are the transcripts one gets from T₅ by restricting to the messages pertaining to sub-protocols Π₃ and Π₄, respectively. The soundness of f₅ follows directly from the soundness off₃ and f₄. Moreover, like in the proof of the first composition theorem (Theorem 4.2), we assume for simplicity thatf₃andf₄ have perfect soundness. It follows thatf₅has perfect soundness too.

4.3.1 Explicit entity authentication

Lemma 4.13. Withf₅as defined above, and everything else as otherwise stated in Theorem 4.12, we have that

Adv^3P_Π5^-_,f^AKE₅ ^fs-EA(A)≤2n²·Adv^3P_Π3^-_,f^AKE₃ ^wfs(B1) +n²·Adv^2P_Π4^-_,f^AKE₄ ^nfs-EA(B2) + .

Proof.

Game 0: This is the original 3P-AKE^fs-EA security experiment, hence Adv^G_Π^0-EA

5,f5(A) =Adv^3P_Π5^-_,f^AKE₅ ^fs-EA(A). (4.23) Game 1: In this game the challenger aborts if two sessions at the same party end up with the same local transcriptτ in sub-protocol Π₄. By definition of the function this gives

Adv^G_Π^0-EA

5,f5(A)≤Adv^G_Π^1-EA

5,f5(A) + . (4.24) Game 2: This game implements a selective security game where the adver-sary is required to commit to the session that will accept maliciously first.

Specifically, at the beginning of the game the adversary must first choose a pair (U, i), with i ∈ [1, n_π]. The game then proceeds as in Game 1, except that if some session accepts maliciously before πⁱ_U, the challenger aborts the game and outputs 0 (i.e., Aloses). In particular, this includes the possibility thatAmakes a query that rendersπⁱ_U unfresh (which would precludeπⁱ_U from accepting maliciously).

Claim 4.14.

Adv^G_Π^1-EA

5,f5(A)≤n_π· |I ∪ R| ·Adv^G_Π^2-EA

5,f5(A). (4.25) Proof. The proof is essentially the same as for Game 2 in Theorem 4.2 (Claim 4.5), only that this time the selective security adversary guesses one session rather

than two.

In the remaining games, letπⁱ_U denote the session that the adversary com-mits to in Game 2. Note thatπ_Uⁱ is not necessarily the same as the test-session chosen by the adversary.

Game 3: This game extends the selective security requirement of Game 2 by demanding that the adversary also commits to the partner of π_Uⁱ in sub-protocol Π₃ (if any). Specifically, at the beginning of the game the adversary must pick a pair (U, i) as in Game 2, but it must also pick a pair (V, j), with j ∈[0, n_π]. Game 3 then proceeds as in Game 2, but it additionally aborts if π_Uⁱ gets a different f₃-partner thanπ^j_V in sub-protocol Π₃. This includes the case thatπ_Uⁱ gets anf₃-partner ifj = 0.

Remark 4.15. Note that there is no contradiction betweenπ_Uⁱ accepting ma-liciously in protocol Π₅according to partner functionf₅, while simultaneously

having anf₃-partner in sub-protocol Π₃.

Claim 4.16.

Adv^G_Π^2-EA

5,f5(A)≤(n_π+ 1)·max{|I|,|R|} ·Adv^G_Π^3-EA

5,f5(A). (4.26) Proof. Again, from an adversaryA that plays against thesingle selective se-curity requirement of Game 2, we can create an adversary A against thetwo selective security requirements of Game 3. Basically, afterAoutputs its com-mitment to a pair (U, i), thenAguesses another pair (V, j) (conditioned on the role ofU), and outputs (U, i) and (V, j) as its own commitments to Game 3.

In the remaining games, let π_V^j denote the (possibly empty) f₃-partner of π_Uⁱ that the adversary commits to in Game 3 in addition toπⁱ_U.

Game 4: This game proceeds as the previous one, but it replaces the inter-mediate keyK_Π3 ofπ_Uⁱ andπ^j_V in sub-protocol Π₃with a random key K.

Claim 4.17.

Adv^G_Π^3-EA

5,f5(A)≤Adv^G_Π^4-EA

5,f5(A) +Adv^3P_Π3^-_,f^AKE₃ ^wfs(B1). (4.27) Proof. We show that if it is possible to distinguish Game 3 and Game 4, then we can create an algorithmB1that breaks the 3P-AKE^wfssecurity of sub-protocol Π₃. ReductionB1 begins by choosing a random bitb_sim. It then runsA and implements all the abort conditions introduced so far. All ofA’sSend queries that pertain to the 3P-AKE sub-protocol Π₃, B1 forwards to its 3P-AKE^wfs security game. For all sessions different from π_Uⁱ and π_V^j, B1 obtains their intermediate keys K_Π3 in sub-protocol Π₃ by making a corresponding Reveal query to its 3P-AKE^wfs game.

On the other hand, when the first session out ofπⁱ_U andπ_V^j accepts in sub-protocol Π₃, thenB1instead makes aTestquery to obtain its intermediate key K_Π3 in protocol Π₅. Let k^∗ denote this key. When the second session out of π_Uⁱ and π^j_V accepts in sub-protocol Π₃, it is assigned the same key k^∗ as its intermediate key in sub-protocol Π₃.

B1 simulates sub-protocol Π₄ itself using the intermediate keys it obtained for sub-protocol Π₃ as the PSKs for Π₄. To answerA’sTestquery, B1 uses the bit b_sim it drew in the beginning of the simulation. Finally, whenπⁱ_U accepts in protocol Π₅, thenB1 stops it simulation and outputs a 0 to its 3P-AKE^wfs game ifπ_Uⁱ accepted maliciously, and a 1 otherwise.

Before analyzingB1’s advantage, we argue that ifπⁱ_U accepts maliciously in B1’s simulation, then both πⁱ_U and π^j_V are valid test-targets in its 3P-AKE^wfs

game, i.e., fresh according to predicate Fresh_AKEwfs. Recall that B1 selects its test-session based on which ofπⁱ_U andπ^j_V accepted first in sub-protocol Π₃. We consider three cases:

• j = 0: In this case πⁱ_U is chosen as the test-session, and B1 makes no Reveal query towards it in its 3P-AKE^wfs game because it uses theTest query to obtain its intermediate key. Sinceπ_Uⁱ does not have anf₃-partner (j= 0), there are of course no otherRevealqueries that could have made πⁱ_U unfresh.

We claim thatB1 also never issued aCorruptquery toπⁱ_U’s peers. To see this, note that ifπⁱ_U is to accept maliciously in protocol Π₅, then it must be fresh according to predicateFresh_AKEfs. In particular, this means that Acannot issue anyCorruptqueries toπ_Uⁱ’s peersbeforeπⁱ_U accepted.⁵ But B1stops its simulation immediately onceπⁱ_U accepts, so noCorruptquery will actually be forwarded toπ_Uⁱ’s peers inB1’s 3P-AKE^wfsexperiment in this case.

• j = 0 and π_Uⁱ chosen as test-session: Again, B1 makes no Revealquery towardsπⁱ_U orπ^j_V in its 3P-AKE^wfsgame, since they are both handled by theTestquery. Moreover, sinceπ_Uⁱ has an f₃-partner (j= 0), it remains AKE^wfs fresh even if its peers are corrupted.

• j = 0 and π_V^j chosen as test-session: By symmetry of the f₃ partner function,π_V^j hasπⁱ_U as itsf₃-partner, and thus the argument is the same as for the above case.

Taken together, the above cases show that no-matter which one ofπⁱ_U and π_Vⁱ was selected as the test-session byB1, it will be fresh according to predicate Fresh_AKEwfs in B1’s 3P-AKE^wfs game ifπ_Uⁱ accepted maliciously.

Finally, we analyze B1’s advantage. Let bdenote the challenge-bit used to answerB1’s Testquery in its 3P-AKE^wfs game. If b= 0, thenB1’sTestquery is answered with a real key, andB1simulates Game 3 perfectly for Aup until the point whenπ_Uⁱ accepts (in protocol Π₅). Thus:

Pr[Exp^AKE_Π3,Q^wfs(B1)⇒1|b= 0] =Adv^G_Π^3-EA

5,f5(A). (4.28) On the other hand, ifb= 1, meaning thatB1’sTestquery is answered with a random key, then B1 perfectly simulates Game 4. SinceB1 only outputs a

5Recall that predicateFresh_AKEfs forbids anyCorruptquery to a session’s peers if (1) it does not have a partner, and (2) it has not accepted yet. This corresponds exactly to the setting we are in when a session accepts maliciously.

1 to its 3P-AKE^wfs security game ifAloses inB1’s simulation, i.e., ifπⁱ_U does not accept maliciously, we have

Pr[Exp^AKE_Π3,Q^wfs(B1)⇒1|b= 1] = 1−Adv^G_Π⁴₅^-_,f^EA₅(A). (4.29) Thus,B1’s advantage is

Adv^3P-AKE_Π3,f3 ^wfs(B1) = 2·Pr[Exp^AKE_Π,Q^wfs(B1)⇒1]−1 (4.30)

= Pr[Exp^AKE_Π,Q^wfs(B1)⇒1|b= 0]

+ Pr[Exp^AKE_Π,Q^wfs(B1)⇒1|b= 1]−1

(4.31)

=Adv^G_Π^3-EA

5,f5(A)−Adv^G_Π^4-EA

5,f5(A), (4.32)

as stated in the claim.

Since the intermediate key K_Π3 of π_Uⁱ and π_V^j is replaced with an inde-pendent uniformly random key in Game 4, we can finally show that if πⁱ_U accepts maliciously in Game 4, then it must have accepted maliciously in sub-protocol Π₄.

Claim 4.18.

Adv^G_Π^4-EA

5,f5(A)≤Adv^2P_Π4^-_,f^AKE₄ ^nfs-EA(B2). (4.33) Proof. If Awins in Game 4, we can create the following algorithm B2 which breaks the explicit entity authentication of sub-protocol Π₄. Algorithm B2

begins by creating all the long-term keys for sub-protocol Π₃ and drawing a random bitb_sim. It then runsAand simulates sub-protocol Π₃ itself using the intermediate keys coming out of sub-protocol Π₃as the PSKs for sub-protocol Π₄. Additionally, for all sessions different fromπⁱ_U and π^j_V, B2 also simulates sub-protocol Π₄ itself. On the other hand, to simulate sub-protocol Π₄forπⁱ_U and π_V^j, B2 instead forwards the corresponding queries to its own 2P-AKE^nfs security game. OnceAstops and outputs a guessb, thenB2 stops too.

For sessions different fromπ_Uⁱ andπ^j_V,B2simulates Game 4 perfectly since it created all the keys. However,B2 also perfectly simulatesπ_Uⁱ andπ_V^j, since by the change in Game 4, their intermediate key K_Π3 from sub-protocol Π₃ is replaced with an independent uniformly random keyK. This is identically distributed to the long-term PSK used inB2’s 2P-AKE^nfssecurity game, so by forwarding theSend queries directed toπ_Uⁱ andπ^j_V to its 2P-AKE^nfs game,B2

perfectly simulates these sessions too.

It remains to argue that if π_Uⁱ accepts maliciously in Game 4, then it must also have accepted maliciously inB2’s 2P-AKE^nfssecurity game. First we claim that sessionπ_V^j cannot be π_Uⁱ’sf₄-partner in sub-protocol Π₄.

• If j = 0, then B2 never creates a corresponding proxy session in its 2P-AKE^nfs security game, hence π_Uⁱ cannot possibly have a partner there.

• If j = 0, then π_V^j by definition (Game 3) must be πⁱ_U’s f₃-partner in sub-protocol Π₃. But ifπ^j_V wasalso thef₄-partner ofπ_Uⁱ in sub-protocol Π₄, then by the construction of f₅ from f₃ and f₄, π_V^j would be πⁱ_U’s f₅-partner—contradicting the fact that π_Uⁱ was supposed to accept mali-ciously.

There is one subtlety with the arguments above: technically we need to show that πⁱ_U and π_Vⁱ are f₄-partners in Game 4 if and only if they are f₄ -partners inB2’s 3P-AKE^nfs-EA security game. However, theT₄transcript from Game 4 containsmanysessions, while the transcriptT_B2 fromB2’s 2P-AKE^nfs security game contains at most two: π_Uⁱ and π_V^j. In particular, transcriptT_B2 is the restriction T₄

πⁱ_U,π_Vⁱ of T₄. But evaluating the same partner function on these two transcripts does not necessarily have to yield the same answer.

This is where we use the assumption that f₄ is a local partner function (see Definition 3.5). Namely, since f₄ is local, we have that πⁱ_U and πⁱ_V are f₄ -partners based onT₄if and only if they aref₄-partners based on the restriction T₄

π_Uⁱ,π_Vⁱ—provided that T₄ is a unique transcript, i.e., no two sessions at the same party have the same local transcriptτ. But this is exactly what the abort condition in Game 1 ensures.

Having shown that πⁱ_U does not accept with an f₄-partner in B2’s 2P-AKE^nfs-EA security game, we only have to show that π_Uⁱ is fresh according to predicateFresh_AKEnfs. But this is true sinceB2makes noCorruptquery at all in its 2P-AKE^nfs security game, and also makes no Revealquery to πⁱ_U. Thus π_Uⁱ accepts maliciously in B2’s 2P-AKE^nfs security game whenever it accepts

maliciously in Game 4, proving Claim 4.18.

Combining the bounds from Game 1 to Game 4 with Claim 4.18 yields

Lemma 4.13.

4.3.2 AKE

^fs

security

Given Lemma 4.13, which shows that Π₅provides explicit entity authentication, we can now proceed with the proof of Theorem 4.12.

Game 0: This is the real 3P-AKE^fssecurity game, hence Adv^G_Π⁰

5,f5(A) =Adv^3P_Π5^-_,f^AKE₅ ^fs(A).

Game 1: In this game, the challenger aborts if a session accepts maliciously in protocol Π₅, whence

Adv^G_Π⁰_5,f5(A)≤Adv^G_Π¹_5,f5(A) +Adv^3P_Π5^-_,f^AKE₅ ^fs-EA(A). (4.34) The remaining game hops are essentially the same as those of Lemma 4.13.

Hence, we merely state their descriptions and corresponding bounds, but omit the proofs.

Game 2: In this game the challenger aborts if two sessions at the same party end up with the same local transcript τ in sub-protocol Π₄. By definition of the function this gives

Adv^G_Π¹_5,f5(A)≤Adv^G_Π²_5,f5(A) + . (4.35) Game 3: This game implements a selective security game where the adversary has to commit to a test-session and its partner (required to exist by Game 1).

Specifically, at the beginning of the game the adversary must output two pairs (U, i) and (V, j). The game then proceeds as in Game 2, except that if either of the following events occur, then the challenger penalizes the adversary by outputting a random bit at the end.

(i) Neitherπ_Uⁱ norπ^j_V were selected as the test-session byA.

(ii) πⁱ_U andπ_V^j did not get partnered to each other.

Claim 4.19.

Adv^G_Π²

5,f5(A)≤(n²_π· |I| · |R|)/2·Adv^G_Π³

5,f5(A). (4.36) In the remaining games, letπ_Uⁱ andπ^j_V denote the two sessions the adversary commits to in the selective security game.

Game 4: This game proceeds as the previous one, but it replaces the inter-mediate keyK_Π3 ofπ_Uⁱ andπ^j_V in sub-protocol Π₃with a random key K.

Claim 4.20.

Adv^G_Π³_5,f5(A)≤Adv^G_Π⁴_5,f5(A) + 2·Adv^3P_Π3^-_,f^AKE₃ ^wfs(B1). (4.37) Finally, any successful attack on protocol Π₅in Game 4 can be transformed into a successful attack on sub-protocol Π₄.

Claim 4.21.

Adv^G_Π⁴

5,f5(A)≤Adv^2P_Π4^-_,f^AKE₄ ^nfs(B2). (4.38)

Concluding the proof of Theorem 4.12. Combining the bounds from Section 4.3.2 to Game 4 with Claim 4.21, we get

Adv^3P_Π5^-_,f^AKE₅ ^fs(A)≤Adv^3P_Π5^-_,f^AKE₅ ^fs-EA(A) + 2n²·Adv^3P_Π3^-_,f^AKE₃ ^wfs(B1) +n²·Adv^2P_Π4^-_,f^AKE₄ ^nfs(B2) + .

(4.39)

The concrete bound of Theorem 4.12 now follows by applying Lemma 4.13

to Equation (4.39).

In document A Modular Security Analysis of EAP and IEEE 802.11 (sider 91-99)