Provably-Secure

Mutual Authentication and Key Establishment Protocols

Lounge

Key establishment, a fundamental building block in cryptography, is defined to be any process whereby a shared secret key becomes available to two or more parties, for subsequent cryptographic use (Menezes, van Oorschot, andVanstone, 1997). Such a scheme can be broadly classified into key agreement or key transport depending on the nature of the session key (i.e., whether input to the session key is required from only one party or all the participating parties) (Boyd and Mathuria, 2003; Menezes, van Oorschot, andVanstone, 1997). The basis of many key establishment protocols relies on the Diffie--Hellman key exchange (Diffie and Hellman,1976), the RSA algorithm (Rivest, Shamir, and Adleman,1978), and more recently elliptic curve pairings (identity-based). In fact, the first key establishment protocol with public key properties is published by Diffie and Hellman (1976). Although a latter protocol of Merkle (1978), Merkle's puzzles, also achieves the key distribution goal, the protocol of Diffie and Hellman (1976) enjoys a better ratio between security and efficiency (Wolf, 1999).

Despite cryptographic key establishment protocols being the sine qua non of many diverse secure electronic commerce applications, the design of secure protocols is still notoriously hard. The difficulties associated in obtaining a high level of assurance in the security of almost any new or even existing protocols are well illustrated with examples of errors found in many such protocols years after they were published (Abadi, 1997; Abdalla, Bresson, Chevassut, and Pointcheval, 2006); Bao, 2003; Bao, 2004; Basin, Mödersheim, and Viganò, 2003; Boyd and Choo, 2005; Burmester, 1993; Kaliski, 2001; Cheng and Comley, 2006; Choo, 2006; Choo, Boyd, and Hitchcock, 2005; Choo, Boyd, and Hitchcock, 2005c; Choo, Boyd, Hitchcock, and Maitland, 2004a; Choo and Hitchcock, 2005; Donovan, Norris, and Lowe, 1999; Lowe, 1996; Mitchell and Yeun, 1998; Myasnikov, Shpilrain, and Ushakov, 2005;Nam, Kim, and Won, 2004; Ku and Wang, 2000; Shoup, 2001; Wan and Wang, 2004; Wang, Wang, and Xu, 2004; Wing, 1998; Wong and Chan, 2001; Zhang, 2005).

The study of cryptographic protocols for key establishment and authentication have led to the dichotomization of cryptographic protocol analysis techniques between the computer security approach and the computational complexity approach, as shown in Fig 1.

Fig 1. Overview of cryptographic protocol analysis techniques

[The Computer Security Approach]
In the 1990s academic cryptography started its move toward a mature discipline by demanding new standards of proof, with many researchers shifting their attention to using formal methods, especially in the last decade. Emphasis in the computer security approach is placed on automated machine specification and analysis (e.g., model checking and theorem proving). The Dolev and Yao (1983) adversarial model is the de-facto model used in formal specifications, where cryptographic operations are often used in a black box fashion ignoring the various cryptographic properties, resulting in possible loss of partial information. One of the main obstacles in this automated approach is the undecidability and intractability problems since the adversary can have an exponentially large set of possible actions (e.g., messages from adversary are unbounded in structural depth, number of possible values for some data fields is infinite) which result in a state explosion (Cervesato, Durgin, Lincoln, Mitchell, & Scedrov, 1999). Furthermore, protocols proven secure in such a manner could possibly be flawed (i.e., giving a false positive result -- analogous to a Type II error in hypothesis testing). From a real world practicality perspective, it is debatable whether proofs of security in this manner carry significant weight in the real world, due to their idealistic model. However, the computer security approach should be credited for proving insecurities in protocols (i.e., finding both known and previously unknown flaws in protocols) (Allamigeon and Blanchet, 2005; Basin, Mödersheim, and Viganò, 2003;Choo, 2006a;Choo, Boyd, and Hitchcock, 2005; Clarke, Jha, and Marrero, 2000; Steel and Bundy, 2005)

[The Computational Complexity Approach]
On the other hand, the computational complexity approach adopts a deductive reasoning process (i.e., the logical process of deriving a conclusion from a known premise) whereby the emphasis is placed on a proven reduction from the problem of breaking the protocol to another problem believed to be hard. The first treatment of computational complexity analysis for cryptography began in the 1980s (Goldwasser and Micali, 1984). It was made popular for key establishment protocols by Bellare & Rogaway (1993) whereby they formally defined a model of adversary capabilities with an associated definition of security and provided a proof of security for two-party entity authentication and key exchange protocols. Since then, there have been several extensions to the Bellare & Rogaway (1993) proof model, such as the Bellare & Rogaway (1995) key establishment model, the Bellare, Pointcheval, & Rogaway (2000) password-based mutual authentication and key establishment model, the Bresson, Chevassut, & Pointcheval (2001) group authenticated key establishment model, and the most recent Abdalla, Fouque, & Pointcheval (2005) password-based authenticated key establishment model. Independent yet related works based on Bellare, Canetti & Krawczyk (1998) by Canetti & Krawczyk (2001) and Shoup (1999) result in two new proof models, namely the Canetti-Krawczyk modular model (Canetti & Krawczyk, 2001) and the Shoup key exchange model (Shoup, 1999).

A complete (human-generated) mathematical proof with respect to cryptographic definitions provides a strong assurance that a protocol is behaving as desired. The history of mathematics is, however, full of erroneous proofs (Bundy, Jamnik, and Fugard, 2005). The difficulty of obtaining correct mathematical proofs has been illustrated in the virtuoso work of Lakatos (1976) whereby the many proofs and refutations for Euler's characteristic in algebraic topology are presented as a comedy of errors (many formulations for Euler's characteristic in algebraic topology, a theorem about the properties of polyhedra, have been tried, only to be refuted and replaced by another formulation).

The difficulty of obtaining correct computational proofs of security is also dramatically illustrated by the well-known problem with the OAEP mode for public key encryption (Shoup, 2001}. Although OAEP was one of the most widely used and implemented algorithms, it was several years after the publication of the original proof that a problem was found (and subsequently fixed in the case of RSA). Problems with proofs of protocol security have occurred too. Furthermore, such security proofs usually entail lengthy and complicated mathematical proofs, which are daunting to most readers (Koblitz and Menezes, 2004). The breaking of provably-secure protocols after they were published is evidence of the difficulty of obtaining correct computational proofs of protocol security. Despite these setbacks, we advocate that proofs are invaluable for arguing about security and certainly are one very important tool in getting protocols right (Choo, Boyd, and Hitchcock, 2005c).

[Motivations of Lounge]
Motivated by the absence of a compendium of provably-secure key establishment and/or mutual authentication protocols, this lounge aims to provide an updated brief summary of proposed key establishment and/or mutual authentication protocols proven secure in one of the earlier-mentioned models (Bellare & Rogaway, 1993; Bellare & Rogaway, 1995; Shoup, 1999; Bellare, Pointcheval, & Rogaway, 2000; Bresson, Chevassut, & Pointcheval, 2001; Canetti & Krawczyk, 2001; Abdalla, Fouque, & Pointcheval, 2005) and their properties. In doing so, we hope that this lounge will be useful for the wider research community.

1. Materials presented in this lounge includes results originally presented in the author's Ph.D. thesis titled "Key Establishment: Proofs and Refutations".
2. Protocols proven secure in one model might not be secure in another model as shown in recent work of Choo, Boyd, and Hitchcock (2005b), whereby they present a detailed comparison of the relative strengths of the notions of security between the Bellare--Rogaway and the Canetti--Krawczyk proof models. Abdalla, Fouque, & Pointcheval (2005) also demonstrate that a protocol proven secure in the Abdalla, Fouque, & Pointcheval (2005) model is also secure in the Bellare, Pointcheval, & Rogaway (2000) model.
3. Protocols proven secure in a model that restricts the adversary access to the Corrupt query are not proven secure against insider and unknown key share attacks, as shown by Choo, Boyd, and Hitchcock (2005b).

1. you cannot find what you are looking for AND
2. (you know of a relevant paper that is not listed (but should be listed) here OR
3. you are the author of a provable-secure protocol in any of these models),

Provably-Secure Protocols in the
Bellare&Rogaway (1993) Model

Provably-Secure Protocols in the
Bellare&Rogaway (1995) Model

Provably-Secure Protocols in the
Bellare, Rogaway,&, Pointcheval (2000) Model

Provably-Secure Protocols in the
Bresson, Chevassut, & Pointcheval (2001) Model

Provably-Secure Protocols in the
Abdalla, Fouque & Pointcheval (2005) Model

Provably-Secure Protocols in the
Canetti & Krawczyk (2001) Model

Provably-Secure Protocols in the Shoup (1999) Model

Summary of Notation

Summary of 123 Protocols' Properties