’’ ’ ’

’ ’ ’’

rA,2

g , rE

K4 = (grA,2 )b

’’ ’ ’

’ ’ ’’

k2,1 , e1

← ’ ’ ’ k2,1 = h2 (gb , grA,1 , K1 )

’ ’ ’’

e1 ∈R {0, 1}k

. .

. .

. .

k2,4 , e4

← ’ ’ ’ k2,4 = h2 (gb , grA,2 , K4 )

’ ’ ’’

k2,1 , e2

?

e4 ∈R {0, 1}k

k2(S1(A)) = k2,1 ←’ ’ ’

’ ’ ’’

k2,4 , e3

?

k2(S2(A)) = k2,4 ←’ ’ ’

’ ’ ’’

d d ?

’ ’ 1’ ’ ’ ’ 1’ ’ rE = h1 (gd1 (ga )e2 )

d1 = tA,1 ’ ae2 mod q ’’ ’ ’ ’’ ’ ’

d d ?

’ ’ 2’ ’ ’ ’ 2’ ’ rE = h1 (gd2 (ga )e3 )

d2 = tA2 ’ ae3 mod q ’’ ’ ’ ’’ ’ ’

kAB(1) = h0 (gb , grA,1 , (gb )rA,1 ) kBA(1) = h0 (gb , grE , (grE )b )

kAB(2) = h0 (gb , grA,2 , (gb )rA,2 ) kBA(2) = h0 (gb , grE , (grE )b )

Attack 10.3: New attack 2 on Protocol 10.1

10.3 Analysing Another Two Protocols With Claimed Proofs of

Security

Both Protocols 10.2 and 10.3 carry claimed proofs of security in the CK2001 model

[14]. The notation used is as follows:

• A, B, and C denote the protocol participants exchanging a secret (session) key,

• XEY denotes the encryption by X intended for Y ,

• MACNXY (·) denotes the generated MAC digest of some message using the one-

time MAC key, NXY ,

• NXY denotes the randomly generated nonce by X intended for Y ,

• a, b, and c denote the randomly generated ephermeral private keys of A, B, and

C respectively.

The reader might notice that the session identi¬er, sid, in the speci¬cations of Proto-

cols 10.2 and 10.3 appear to be constructed differently from that discussed in Chap-

ter 9.3. If we had follow the revised construction for session identi¬ers presented in

10.3 Analysing Another Two Protocols With Claimed Proofs of Security 173

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

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

MACNAB (sid, [b]P, A), AEC (NAC )

3. C ’’ A : sid, [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)

4. A ’’ B : sid, [c]P, MACNBA (sid, [a]P, B),

MACNCA (sid, [a]P,C),CEB (NCB ),

MACNBC (sid, [c]P, B)

5. B ’’ C : sid, MACNCB (sid, [b]P,C),

MACNCA (sid, [a]P,C)

Session key SK = e(P, P)abc

Protocol 10.2: Hitchcock“Boyd“Gonz´ lez Nieto tripartite key exchange protocol 8

a

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

2. B ’’ C : sid, [a]P, [b]P, BEA (NBA ),

MACNAB (sid, [b]P, A), AEC (NAC )

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

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

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

4. A ’’ B : sid, [c]P,

MACNBA (sid,C, [a]P, [c]P, B),

MACNCA (sid, [a]P, [b]P,C)

5. A/B ’’ C : sid, MACNCA (sid, [a]P, [c]P,C)

Session key SK = e(P, P)abc

Protocol 10.3: Hitchcock“Boyd“Gonz´ lez Nieto tripartite key exchange protocol 9

a

the earlier discussion, session identi¬ers should be

sidA = H (A||B||C||NAB ||NAC ||NBA ||NBC ||NCA ||NCB ) = sidB = sidC ,

where sidU denotes the session identi¬er of some protocol participant, U.

However, such a construct does not appear to be feasible for Protocols 10.2 and 10.3

since not all protocol participants have full view of the messages exchanged. For ex-

ample, B does not know NAC and C does not know NAB .

10.3.1 Protocol Analysis

The attack sequences and the internal states can be examined by viewing the reach-

ability graphs produced by SHVT. The analyses were run on a Pentium IV 2.4 GHz

computer with 1024 Mb of RAM and the analysis statistics are shown in Figure 10.6.

174 10 Complementing Computational Protocol Analysis

Protocol Analysis # Players # Runs Run-Time New Flaws?

Protocol 10.2 3 2 Approximately 3 mins Yes

Protocol 10.3 “ ditto “

Fig. 10.6 Analysis statistics

10.3.1.1 Analysis of Protocol 10.2

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.4.

At the end of Attack 10.4,

• 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).

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.