We examine the role of session identifiers (SIDs) in security proofs for key establishment protocols. After reviewing the practical importance of SIDs we use as a case study the three-party server-based key distribution (3PKD) protocol of Bellare and Rogaway, proven secure in 1995. We show incidentally that the partnership function used in the existing security proof is flawed. There seems to be no way to define a SID for the 3PKD protocol that will preserve the proof of security. A small change to the protocol allows a natural definition for a SID and we prove that the new protocol is secure using this SID to define partnering.
We examine the role of session identifiers (SIDs) in security proofs for key establishment protocols. After reviewing the practical importance of SIDs we use as a case study the three-party server-based key distribution (3PKD) protocol of Bellare and Rogaway, proven secure in 1995. We show incidentally that the partnership function used in the existing security proof is flawed. There seems to be no way to define a SID for the 3PKD protocol that will preserve the proof of security. A small change to the protocol allows a natural definition for a SID and we prove that the new protocol is secure using this SID to define partnering.
We study the problem of secure key establishment. We critically examine the security models of Bellare and Rogaway (1993) and Canetti and Krawczyk (2001) in the computational complexity approach, as these models are central in the understanding of the provable security paradigm. We show that the partnership definition used in the three-party key distribution (3PKD) protocol of Bellare and Rogaway (1995) is flawed, which invalidates the proof for the 3PKD protocol. We present an improved protocol with a new proof of security. We identify several variants of the key sharing requirement (i.e., two entities who have completed matching sessions, partners, are required to accept the same session key). We then present a brief discussion about the key sharing requirement. We identify several variants of the Bellare and Rogaway (1993) model. We present a comparative study of the relative strengths of security notions between the several variants of the Bellare-Rogaway model and the Canetti-Krawczyk model. In our comparative study, we reveal a drawback in the Bellare, Pointcheval, and Rogaway (2000) model with the protocol of Abdalla and Pointcheval (2005) as a case study.
We prove a revised protocol of Boyd (1996) secure in the Bellare-Rogaway model. We then extend the model in order to allow more realistic adversary capabilities by incorporating the notion of resetting the long-term compromised key of some entity. This allows us to detect a known weakness of the protocol that cannot be captured in the original model. We also present an alternative protocol that is efficient in both messages and rounds. We prove the protocol secure in the extended model. We point out previously unknown flaws in several published protocols and a message authenticator of Bellare, Canetti, and Krawczyk (1998) by refuting claimed proofs of security. We also point out corresponding flaws in their existing proofs. We propose fixes to these protocols and their proofs. In some cases, we present new protocols with full proofs of security. We examine the role of session key construction in key establishment protocols, and demonstrate that a small change to the way that session keys are constructed can have significant benefits. Protocols that were proven secure in a restricted Bellare-Rogaway model can then be proven secure in the full model. We present a brief discussion on ways to construct session keys in key establishment protocols and also prove the protocol of Chen and Kudla (2003) secure in a less restrictive Bellare-Rogaway model. To complement the computational complexity approach, we provide a formal specification and machine analysis of the Bellare-Pointcheval-Rogaway model using an automated model checker, Simple Homomorphism Verification Tool (SHVT). We demonstrate that structural flaws in protocols can be revealed using our framework. We reveal previously unknown flaws in the unpublished preproceedings version of the protocol due to Jakobsson and Pointcheval (2001) and several published protocols with only heuristic security arguments. We conclude this thesis with a listing of some open problems that were encountered in the study.
We examine the role of session key construction in provablysecure key establishment protocols. We revisit an ID-based key establishment protocol due to Chen & Kudla (2003) and an ID-based protocol 2P-IDAKA due to McCullagh & Barreto (2005). Both protocols carry proofs of security in a weaker variant of the Bellare & Rogaway (1993) model where the adversary is not allowed to make any Reveal query. We advocate the importance of such a (Reveal) query as it captures the known-key security requirement. We then demonstrate that a small change to the way that session keys are constructed in both protocols results in these protocols being secure without restricting the adversary from asking the Reveal queries in most situations. We point out some errors in the existing proof for protocol 2P-IDAKA, and provide proof sketches for the improved Chen & Kudla’s protocol. We conclude with a brief discussion on ways to construct session keys in key establishment protocols.
Although the Yahalom protocol, proposed by Burrows, Abadi, and Needham in 1990, is one of the \nmost prominent key establishment protocols analysed by researchers from the computer security community (using automated proof tools), a simplified version of the protocol is only recently proven secure by Backes and Pfitzmann [(2006) On the Cryptographic Key Secrecy of the Strengthened Yahalom Protocol. Proc. IFIP SEC 2006] in their cryptographic library framework. We present a protocol for key establishment that is closely based on the Yahalom protocol. We then present a security proof in the Bellare, M. and Rogaway, P. [(1993a). Entity Authentication and Key Distribution. Proc. of CRYPTO 1993, Santa Barbara, CA, August 22–26, LNCS, Vol. 773, pp. 110–125. Springer-Verlag, Berlin] model and the random oracle model. We also observe that no partnering mechanism is specified within the Yahalom protocol. We then present a brief discussion on the role and the possible construct of session identifiers (SIDs) as a form of partnering mechanism, which allows the right session key to be identified in concurrent protocol executions. We then recommend that SIDs should be included within protocol specification rather than consider SIDs as artefacts in protocol proof.
A flaw lied in the security definition of the Bellare-Rogaway 3PKD model,which was proposed by Bellare and Rogaway for three-party key distribution in 1995,was discovered.To reveal it,a new three-party key distribution proto-col P-Flaw was proposed.The protocol was provably secure under the Bellare-Rogaway 3PKD model.However the pro-tocol was not secure enough to withstand the server spoofing attack,known session key attack,and replay attack.The absence of the origin recognition for the distributed session key accounts for the flaw.Accordingly,the security definition of the Bellare-Rogaway 3PKD model was corrected based on matching conversation.
Although the Yahalom protocol, proposed by Burrows, Abadi, and Needham in 1990, is one of the most prominent key establishment protocols analysed by researchers from the computer security community (using automated proof tools), a simplified version of the protocol is only recently proven secure by Backes and Pfitzmann [(2006) On the Cryptographic Key Secrecy of the Strengthened Yahalom Protocol. Proc. IFIP SEC 2006] in their cryptographic library framework. We present a protocol for key establishment that is closely based on the Yahalom protocol. We then present a security proof in the Bellare, M. and Rogaway, P. [(1993a). Entity Authentication and Key Distribution. Proc. of CRYPTO 1993, Santa Barbara, CA, August 22–26, LNCS, Vol. 773, pp. 110–125. Springer-Verlag, Berlin] model and the random oracle model. We also observe that no partnering mechanism is specified within the Yahalom protocol. We then present a brief discussion on the role and the possible construct of session identifiers (SIDs) as a form of partnering mechanism, which allows the right session key to be identified in concurrent protocol executions. We then recommend that SIDs should be included within protocol specification rather than consider SIDs as artefacts in protocol proof.
In this paper, we investigate the notion of partnership as found in security models for key exchange protocols. Several different approaches have been pursued to define partnership, with varying degrees of success. We aim to provide an overview and criticism of the various definitions and point out some pitfalls that can be encountered when trying to define partnership. As a result, we propose an intuitive way of defining partnership directly from equality of session keys. In addition, we show that authentication can be captured using a definition of partnership by equality of partner identifiers, and give proofs that both definitions achieve what we expect from them.