83

84 5 Comparison of Bellare“Rogaway and Canetti“Krawczyk Models

2: The powers of the probabilistic, polynomial-time (PPT) adversary. The

CK2001 model enjoys the strongest adversarial power (compared to the Bellare“

Rogaway models) as the adversary is allowed to ask the Session-State Reveal

query that will return all the internal state (including any ephemeral parameters

but not long-term secret parameters) of the target session to the adversary. In

contrast, most models only allow the adversary to reveal session keys for uncor-

rupted parties. In the original BR93 and BPR2000 models, the Corrupt query is

not allowed. This restricts the adversary from corrupting any principal at will, and

hence the adversary is unable to learn the internal state of the corrupted principal.

In this chapter, we consider the BR93 model which allows the adversary access

to a Corrupt query as explained in Chapter 2.3.1. However, we consider the origi-

nal BPR2000 model without Corrupt query because the basic notion of BPR2000

freshness restricts the adversary, A , from corrupting anyone in the model (i.e.,

effectively restricting A from asking any Corrupt query) as described in Chap-

ter 2.3.2. However, we show that the omission of such a (Corrupt) query in the

BPR2000 model allows an insecure protocol to be proven secure in the model.

3: The modular approach adopted in the CK2001 model. A major advantage of

the CK2001 model is its modular approach whereby protocols may be proven

secure in an ideal world (AM) model in which the passive adversary is prevented

from fabricating messages coming from uncorrupted principals, and translating

such a protocol proven secure in the AM into one that is secure in the more re-

alistic real world model (the UM). As Boyd, Mao, and Paterson [5] have pointed

out, the CK2001 modular approach facilitates an engineering approach to proto-

col design, where protocol components may be combined by “mix and match”

to tailor to the application at hand. Such a mix and match approach is analogous

to a Java API library.

4: The provable security goals provided by the models. Both the BR93 and

BPR2000 models provide provable security for entity authentication & key dis-

tribution, whilst the BR95 model provides provable security for only the key

distribution. Intuitively, protocols that provide both entity authentication and key

distribution are “stronger” than protocols that provide only key distribution. In

this chapter, we refer to the BR93 and BPR2000 models that provide provable

security for only key distribution as BR93 (KE) and BPR2000 (KE) respectively,

and the BR93 and BPR2000 models that provide provable security for both en-

tity authentication & key distribution as BR93 (EA+KE) and BPR2000 (EA+KE)

respectively. To the best of our knowledge, no distinction has ever been made be-

tween the Bellare“Rogaway model and its variants shown in Figure 5.1.

We are motivated by the observations that no formal study has been devoted to

the comparisons of relations and relative strengths of security between the Bellare“

Rogaway and Canetti“Krawczyk models. Although Shoup [8] provides a brief dis-

cussion on the Bellare“Rogaway models and the Canetti“Krawczyk model, his

discussion is restricted to an informal comparison between the Bellare“Rogaway

model and his model, and between the Canetti“Krawczyk model and his model.

5 Comparison of Bellare“Rogaway and Canetti“Krawczyk Models 85

Bellare“Rogaway [2, 3, 4]

“

BR93 BR95 BPR2000

BR93 (KE) BR93 (EA+KE) BPR2000 (KE) BPR2000 (EA+KE)

Fig. 5.1 The proof models and their variants

This work may ease the understanding of future security protocol proofs (proto-

cols proven secure in one model may be automatically secure in another model),

and protocol designers can make an informed decision when choosing an appropri-

ate model in which to prove their protocols secure. Our main results are summarized

in Figures 5.2 and 5.3.

The notation x ’ y (or y ← x) denotes that protocols proven secure in model x

will also be secure in model y (i.e., implication relation where x implies y), x y

(or y x) denotes that protocols proven secure in model x do not necessarily sat-

isfy the de¬nition of security in model y. The numbers on the arrows represent the

section in which the proof is provided, and the numbers in brackets on the arrows

represent the sections in which the implication relation is proven.

5.1.7⊥

BR93 (KE) CK2001

(5.1.6)

5.1.4

5.2,5.1.5

5.1.4 5.2,5.1.5

5.1.4

5.1.2

5.1.1.1 (5.1.3,5.1.4)

5.1.8

BPR2000 (KE) BR95

5.2

holds if SIDs are constructed in the same manner in both models.

⊥ holds if SIDs are not de¬ned to be the concatenation of messages exchanged during the protocol

run.

Fig. 5.2 Notions of security

We observe that if SIDs in the CK2001 model are de¬ned to be the concatenation of

messages exchanged during the protocol run, then the implication CK2001 ’ BR93

86 5 Comparison of Bellare“Rogaway and Canetti“Krawczyk Models

holds, and the CK2001 model offers the strongest de¬nition of security compared

to the BR93 model.

BPR2000 (EA+KE)

CK2001

5.1.1

5.2

5.1.3∇ (5.1.6)

BR93 (EA+KE)

BR93 (KE)

∇ holds if SIDs are de¬ned to be the concatenation of messages exchanged during the protocol

run.

Fig. 5.3 Additional comparisons

The proofs of the implication relations and counter-examples for non-implication

relations shown in Figures 5.2 and 5.3 are presented in Chapter 5.1. In these

counter-examples, we demonstrate that these protocols though secure in the existing

proof model (in which they are proven secure) are insecure in another “stronger”

proof model. Chapter 5.2 presents the drawback in the original formulation of

the BPR2000 model by using a three-party password-based key exchange proto-

col (3PAKE) due to Abdalla and Pointcheval [1] as a case study.

Material presented in this chapter has appeared in the following publication:

• Kim-Kwang Raymond Choo, Colin Boyd, and Yvonne Hitchcock. Examining

Indistinguishability-Based Proof Models for Key Establishment Protocols. In Bi-

mal Roy, editor, Advances in Cryptology - Asiacrypt 2005, volume 3788/2005

of Lecture Notes in Computer Science, pages 585“604, Springer-Verlag, 2005.

5.1 Relating The Notions of Security