A formal model for systematic design of key establishment protocols

Colin Boyd

Colin Boyd

Mounita Saha, Dipanwita RoyChowdhury

The design of a secure and efficient key establishment protocol is one of the toughest challenge in communication protocol design. In the literature many key establishment protocols claimed to be secure against some attacks were later shown to be weak against new attacks. In this work, we have identified a class of weakness named as insider-replay in some existing protocols and proposed a design principle to avoid the weakness. Based on the design principle, we have proposed an efficient key establishment protocol. The proposed protocol is shown to be provably secure under formal security model and averts insider-replay. We have also analyzed the efficiency of the proposed protocol in comparison with existing protocols.

Qiang Tang

Abstract. Two-party key establishment has been a very fruitful research area in cryptography, with many security models and numerous protocols proposed. In this paper, we take another look at the YAK protocol and the HMQV proto-cols and present some extended analysis. Motivated by our analysis, we reflect on the security properties that are desired by two-party key establishment protocols, and their formalizations. In particular, we take into account the in-terface between a key establishment protocol and the applications which may invoke it, and emphasize the concept of session and the usage of session identi-fier. Moreover, we show how to design a two-party key establishment protocol to achieve both key authentication and entity authentication properties in our security model.

M. Choudary Gorantla, Colin Boyd, Juan Manuel González Nieto

One-pass authenticated key establishment (AKE) protocols are arguably better suited to the ID-based environment than their two-pass counterparts. However, there is no ID-based one-pass AKE protocol proposed in the literature with a proof of security in an appropriate model. This paper addresses the current gap by proposing a new ID-based one-pass AKE protocol and proving it secure in a formal model. The security of the new protocol is treated under a model adapted from a formal security model for traditional certificate based AKE protocols. The proof of security is in the random oracle model and is based on the hardness of the bilinear Diffie-Hellman problem. The protocol also turns out to be the most efficient of all the previously known protocols. It can work over a class of asymmetric pairings for better efficiency at higher bit security levels.

Colin Boyd, Anish Mathuria