Decrypt {NB }EKA and obtain NB

?

NB = NB

Session key, MKB = H (sidB ||0||SKAB )

STATUS: Accepted

Protocol 7.2: A revised Yahalom protocol

Informally, the inclusion of the

• Identities of the participants2 and role asymmetry within the session key con-

struction effectively ensures some sense of direction. If the role of the partici-

pants or the identities of the (perceived) partner change, the session keys will

also be different. Hence, this provides resilience against unknown key share and

re¬‚ection attacks.

• Unique session identi¬er (sid) within the session key construction ensures that

session keys will be fresh. Moreover, it appears that the publication of sid upon

protocol completion results in A being unable to get B to accept nonce pair

(which is part of the published sid) as the session key. Recall a different sid also

mean a different session key. Hence, it appears that the type ¬‚aw attack revealed

on Protocol 7.1 by Basin, M¨ dersheim, and Vigan` [3, 5] is thwarted.

o o

7.2.1 Proof for Protocol 7.2

Theorem 7.2.1 Protocol 7.2 is a secure key establishment protocol if the underly-

ing authenticated encryption scheme is INT-PTXT secure as described in De¬ni-

tion 6.1.1 and both H and H1 are modelled as independent random oracles.

2 Such an approach is also recommended by National Institute of Standards and Technology

(NIST) [6]

7.2 A New Provably-Secure Protocol 121

The proof follows the approach described in Chapter 6.1.3.

7.2.1.1 Integrity attacker

We now construct a forger F against the security of the authenticated encryption

scheme, S E , described in De¬nition 6.1.1, using an adversary against Protocol 7.2,

A . We will say that the event successF occurs if F wins game G2 against S E .

Lemma 7.2.1 There is an ef¬cient algorithm F de¬ned using A such that if forge

occurs with non-negligible probability then successF occurs with non-negligible

probability .

In order to prove Lemma 6.1.2 we describe how F is constructed. When F runs

it receives access to the encryption and veri¬cation oracles of the authenticated en-

cryption scheme S E . Its output must be a forged ciphertext for a message m which

was not previously input to the encryption oracle.

In order to obtain the forgery F runs A by ¬rst choosing a user Ui for i ∈R [1, Q].

This user will be simulated as though its long-term key is the one used in S E . For

all other j ∈ [1, Q] with j = i, F generates the long-term shared key using the key

generation algorithm Kk . This allows F to answer all the oracle queries from A as

follows.

Send(U1 , s, M) For any well-formed queries to S, F can reply with valid cipher-

texts, by choosing the session key and forming the ciphertexts, either directly

using the known key or using the encryption oracle in the case of Ui . For queries

to initiate a protocol run, F can generate a random nonce and answer appropri-

ately. Finally, consider a query to either an initiator or responder oracle including

a claimed server message (corresponding to protocol messages 3 or 4). The rel-

evant ciphertext can be veri¬ed either directly using the known key or using the

veri¬cation oracle. If the ciphertext is veri¬ed correctly then the oracle accepts

and this information is returned to A .

Reveal(U, s) Since all session keys are known from running the Send(U, s, M)

queries the query can be trivially answered with the correct session key (if ac-

cepted).

Corrupt(U) As long as U = Ui all the private information is available and the

query can be answered. In the case U = Ui then the query cannot be answered

and F will abort and fail.

Test(U, s) Since all the accepted session keys are known from running the Send

queries the query can be trivially answered by identifying the correct session key.

F continues the simulation until a forgery event against S E occurs, or until A

halts. Note that as long as F does not abort then the simulation is perfect. If forge

occurs then the probability that the user involved is Ui equals 1/Q. In this case the

122 7 A Proof of Revised Yahalom Protocol

event successF occurs. Futhermore, in this case F does not abort since Ui cannot be

corrupted before the forge event. Therefore we arrive at the following upper bound.

Pr(forge) ¤ Q · Pr(successF ) (7.1)

7.2.1.2 Con¬dentiality attacker

For the second part of the proof, we assume that A gains an advantage without pro-

ducing a forgery. We construct an attacker with a non-negligible advantage against

the encryption scheme, X , using the adversary, A , as described in Chapter 6.1.3.2.

Two random keys K and K are chosen by the challenger for S E and X is given

access to the encryption oracles for these keys. First X chooses two users Ui and U j

for i, j ∈R [1, Q]. For all other k ∈ [1, Q], X generates the long-term key using the

key generation algorithm Kk . Next A chooses two random session keys K0 and K1 .

Suppose that QS is the maximum number of Send queries that A will ask of the

server and QH is the maximum number of hash queries that A will ask of the server.

X chooses a value s0 randomly in [1, QS ]. The idea is that X will inject the cipher-

texts Cb ,Cb into a random SendServer query. X proceeds to simulate responses for

A as follows. Let UI and UR denote the initiator and the responder respectively.

Note that we also require two separate lists of tuples, LH and LH1 to be main-

tained. If we are asked queries of the form H (SIDk ||0||SK) and H1 (SIDk ||1||SK),

i i

we check to see if the queries have been previously asked. If so, then the previous

answer stored in the respective list will be returned (to maintain consistency). Oth-

erwise, return a random value, v ∈R {0, 1}k . In addition, store this answer together

with the query in the respective list.

SendClient: In the case of U1 = UI , U2 = UR , and m = —, then this will start a

protocol run. This query can be successfully answered by X and the outgoing

message is some randomly chosen k-bit challenge NU1 .

SendClient: In the case of U1 = UR , U2 = UI , and m is some k-bit challenge, then

X will choose a unique k-bit challenge, NU2 ; computes the session identitifer,

sid = U1 ||U2 ||S||m||NU2 and the respective ciphertext; and successfully answer

this query.

SendServer: In the case of U1 = {UI ,UR }, U2 = S, and m is of the right format (as

per message 2 in protocol speci¬cation), then S will run the session key gener-

ator and output a session key not previously output and generates the respective

ciphertexts as the protocol speci¬cation demands.

SendClient: In the case of U1 = UI , U2 = UR , and m is of the right format (as

per message 3 in protocol speci¬cation). Since we assume that A is not able

to produce any MAC forgeries, all session keys (if accepted) are known from

the SendServer(U1 ,U2 , ι, m) queries. Hence, if the received ciphertext (MAC di-

gest) veri¬es correctly, the message must have been generated by X during a

SendServer query and in this case, X will output the decision δ = accept. Oth-

7.2 A New Provably-Secure Protocol 123

erwise, X will output the decision δ = reject, as the protocol speci¬cation de-

mands.

SendClient: If U1 = UI , U2 = UR , and m is of the right format (as per message

4 in protocol speci¬cation). Again under the assumption that A is not able to

produce any MAC forgeries, all session keys (if accepted) are known from the

SendServer(U1 ,U2 , ι, m) queries. Since we also know the keying materials for

both the session key and the one-time encryption/MAC key EK (used to encrypt

the nonce of UR ) are the same and if received ciphertext (MAC digest) veri¬es

correctly, the message must have been generated by X during a SendServer

query. Therefore, X will output the decision δ = accept. Otherwise, X will

output the decision δ = reject, as the protocol speci¬cation demands.

In all other cases the input to the SendClient or SendServer is invalid, X will

terminate and halt the simulation. Hence, SendClient and SendServer queries can

be correctly answered by X .

This completes the description of X . Since all the accepted session keys are known

from running the SendClient and SendServer queries, the Test query can be trivially

answered by identifying the correct session key.

Let lucky be the event that X does not fail during the Test query. When lucky

occurs, X wins game G1 whenever A is successful. This means that

Pr(successX |lucky) ≥ Pr(successA |forge).