State space analysis in SHVT reveals that goal state 2 of De¬nition 10.1.1 is vio-

lated. The attack sequence is described in Attack 10.5.

Similar to Attack 10.4, at the end of Attack 10.5,

• Oracle ΠA has accepted with SKA = e(P, P)abc .

sid

sid sid

• Both oracles, ΠB A and ΠC A , think that a session (associated with session

sid

identi¬er, sidA ) has been initiated by the adversary, A . However, both ΠB A

sid

and ΠC A are asked Session-State Reveal queries prior to accepting any session

keys.

sid sid

sid

• Since ΠA and (ΠB A and ΠC A ) have different session identi¬ers, they are not

partners (according to De¬nition 2.3.10). Therefore, the adversary, A , is allowed

sid

to reveal both B and C without rendering session key of ΠA unfresh (according

to De¬nition 2.3.1).

10.3 Analysing Another Two Protocols With Claimed Proofs of Security 175

1. A ’’ B : sid, [a]P, AEB (NAB ), AEC (NAC )

The adversary, A , intercepts and deletes message from network. A

then sends intercepted message as her own to B, however, with a

different session identi¬er, sidA .

Note that A is able to claim ownership of the intercepted message

because the identity of the sender is not included in the encryption.

1. A ’’ B : sidA , [a]P, AEB (NAB ), AEC (NAC )

B upon receiving this message will think that A wants to establish

a session (associated with session identi¬er, sidA ) and proceeds as

per protocol speci¬cation.

2. B ’’ C : sidA , [a]P, [b]P, BEC (NBC ),

BEA (NBA ), AEC (NAC ),

MACNAB (sidA , [b]P, A )

3. C ’’ A : sidA , [b]P, [c]P,CEA (NCA ),

CEB (NCB ), MACNAC (sid, [c]P, A ),

MACNBC (sid, [c]P, B), BEA (NBA ),

MACNAB (sid, [b]P, A )

Note that both B and C think that the session (associated with sidA )

is being established with the adversary, A , because SIDB = SIDC =

sidA = SIDA = sid. Therefore, A, B, and C are not partners (see

De¬nition 2.3.10) and A is allowed to reveal both B and C without

rendering session key of A unfresh (see De¬nition 2.3.1).

A ’’ C : Session-State Reveal(C, sidA )

A ’’ B : Session-State Reveal(B, sidA )

sid sid

The internal states of ΠB A and ΠC A are revealed to the ad-

versary, A , after asking the Session-State Reveal queries, which

includes (NAB , b) and (NAC , c) respectively. With knowledge of

(NAB , b, NAC , c), A is able to construct respective ciphertexts and

MAC digests, and send fabricated messages to A impersonating C.

3. AC ’’ A : sid, [b]P, [c]P,CEA (NCA ),

CEB (NCB ), MACNAC (sid, [c]P, A),

MACNBC (sidA , [c]P, B),

BEA (NBA ), MACNAB (sid, [b]P, A)

4. A ’’ B : Some message.

The adversary, A , intercepts and deletes message from the network.

Note that the session key accepted by A is SKA = e(P, P)abc .

Attack 10.4: Attack Sequence on Protocol 10.2

sid sid

• Internal states of ΠB A and ΠC A are revealed to the adversary, A , with the

Session-State Reveal queries, which includes (NAB , b) and (NAC , c) respectively.

sid

With knowledge of these internal states, A is able to “make” ΠA accept the

session key, SKA = e(P, P)abc .

• With knowledge of b and c from earlier Session-State Reveal queries, A is able

to compute the session key accepted by A, e(aP, P)bc = SKA . Hence, AdvA (k) is

non-negligible, in violation of De¬nition 2.3.11.

176 10 Complementing Computational Protocol Analysis

1. A ’’ B : sid, [a]P, AEB (NAB ), AEC (NAC )

The adversary, A , intercepts and deletes message from network. A

then sends intercepted message as her own to B, however, with a

different session identi¬er, sidA .

Note that A is able to claim ownership of the intercepted message

because the identity of the sender is not included in the encryption.

1. A ’’ B : sidA , [a]P, AEB (NAB ), AEC (NAC )

B upon receiving this message will think that A wants to establish

a session (associated with session identi¬er, sidA ) and proceeds as

per protocol speci¬cation.

B ’’ C : sidA , [a]P, [b]P, BEA (NBA ),

2.

MACNAB (sidA , [b]P, A ),

AEC (NAC )

3. C ’’ A : sidA , [b]P, [c]P,CEA (NCA ),

MACNAC (sidA , [c]P, A ),

BEA (NBA ),

MACNAB (sidA , [b]P, A )

Note that both B and C thinks that the session (associated with ses-

sion identi¬er, sidA ) is being established with the adversary, A , be-

cause SIDB = SIDC = sidA = SIDA = sid. Therefore, A, B, and C

are not partners (see De¬nition 2.3.10) and A is allowed to reveal

both B and C without rendering session key of A unfresh (see De¬-

nition 2.3.1).

A ’’ C : Session-State Reveal(C, sidA )

A ’’ B : Session-State Reveal(B, sidA )

sid sid

The internal states of ΠB A and ΠC A are revealed to the ad-

versary, A , after asking the Session-State Reveal queries, which

includes (NAB , b) and (NAC , c) respectively. With knowledge of

(NAB , b, NAC , c), A is able to construct respective ciphertexts and

MAC digests, and send fabricated messages to A impersonating C.

AC ’’ A : sid, [b]P, [c]P,CEA (NCA ),

3.

MACNAC (sid, [c]P, A),

BEA (NBA ),

MACNAB (sid, [b]P, A)

4/5. A ’’ B/C : Some message.

The adversary, A , intercepts and deletes messages sent by A for both

B and C from the network. Note that the session key accepted by A

is SKA = e(P, P)abc .

Attack 10.5: Attack Sequence on Protocol 10.3

10.3 Analysing Another Two Protocols With Claimed Proofs of Security 177

10.3.2 Flaws in Refuted Proofs

The general notion of the existing proofs is to assume that there exists an adversary,

A , who can gain a non-negligible advantage in distinguishing the test key, and use

A to break the underlying DBDH problem. Such an adversary, ADBDH , against

the DBDH problem is built using A . The objective of ADBDH is to distinguish

between e(P, P)d ∈ G2 and e(P, P)abc ∈ G2 when given a bilinear map e, a generator

of P of G1 , an element e(P, P)d ∈ G2 , and a triple of elements aP, bP, cP ∈ G1 with

a, b, c, d ∈ Z— , where q is the prime order of the distinct groups G1 and G2 . Note

q

that the triple of elements a, b, c is not known to ADBDH .

In Attacks 10.4 and 10.5, the adversary, A , is allowed to ask for the ephemeral

secret keys (i.e., b and c) with a Session-State Reveal query (recall that ses-

sions with non-matching session identi¬ers and non-agreeing partner identi¬ers are

non-partners). Clearly, such a query is unable to be answered by ADBDH since

ADBDH does not know b and c as ADBDH is using A to break the underlying

DBDH problem. If ADBDH randomly selects two elements, b ∈ Z— and c ∈ Z— ,

q q

and returns this to A , A is able to check that b P = bP and c P = cP.

Hence, the proof simulation is aborted and ADBDH fails. Consequently, ADBDH