IGI Global eBooks

The Provably Secure Formal Methods for Authentication and Key Agreement Protocols

Jianfeng Ma, Xinghua Li

Published Jan 18, 2011• 0 citations

Abstract

In the design and analysis of authentication and key agreement protocols, provably secure formal methods play a very important role, among which the Canetti-Krawczyk (CK) model and universal composable (UC) security model are very popular at present. This chapter focuses on these two models and consists mainly of three parts: (1) an introduction to CK model and UC models; (2) A study of these two models, which includes an analysis of CK model and an extension of UC security model. The analysis of CK model presents its security analysis, advantages, and disadvantages, and a bridge between this formal method and the informal method (heuristic method) is established; an extension of UC security model gives a universally composable anonymous hash certification model. (3) The applications of these two models. With these two models, the four-way handshake protocols in 802.11i and Chinese wireless LAN (WLAN) security standard WLAN authentication and privacy infrastructure (WAPI) are analyzed.Request access from your librarian to read this chapter's full text.

DOI: 10.4018/9781599048994.ch015

Related papers

The Provably Secure Formal Methods for Authentication and Key Agreement Protocols

Jianfeng Ma, Xinghua Li

IGI Global eBooksJan 1, 20081 citation

Formal Security Definition and Efficient Construction for Roaming with a Privacy-Preserving Extension

Duncan S. Wong, Guomin Yang, Xiaotie Deng

Abstract: In a secure roaming scenario, a user U travels to a foreign network and communicates with a foreign server V securely so that no one other than U and V can obtain the messages exchanged between them. U may also want to travel anonymously so that no one including V can find out its identity or trace its whereabouts except its home server H. There have been many key establishment protocols proposed for secure roaming. A typical application of these protocols is the mobile roaming service which may be deployed to interconnected WLAN and 3G networks. Despite the importance of these protocols, most of the protocols are analyzed heuristically. They are lack of formal security treatment. In this paper, we propose a formal key exchange definition and formalize secure roaming under the Canetti-Krawczyk (CK) model. We also propose a formal model for capturing the notions of user anonymity and untraceability. By using the modular approach supported by the CK-model, we construct an efficient key exchange protocol for roaming and then extend it to support user anonymity and untraceability. The protocols are efficient and each of them requires only four message flows among the three parties U, H and V. For building our protocols, we construct a one-pass counter based MT-authenticator and show its security under the assumption of a conventional MAC secure against chosen message attack.

Apr 7, 202021 citations

Universally composable key exchange protocol for WLAN

Haojun Zhang, Qi Qinglei

The security is the core in the applications of WLAN. The 4-WAY handshake protocol realized the key exchange and update in the WLAN security basement framework which was defined by IEEE 802. 11i. The analysis showed that the 4-WAY handshake was vulnerable to denial-of-service attack. This paper advanced the modified session key agreement protocol, 3-WAY,which was showed that it provided better information authentication,integrality protection and efficiency. In addition,analyzed the 3-way handshake protocol in the universally composable ( UC) security model and proved that this new protocol could realize the key-exchanged ideal function and came to the universally composable security. This new protocol has abroad flexibility.

Jisuanji yingyong yanjiuJan 1, 20100 citations

Analysis of Two Provably Secure Authenticated Key Exchange Protocols in the eCK Model

Xuexian Hu

The extended Canetti-Krawczyk(eCK) model proposed by LaMacchia et al.is currently regarded as the strongest security model for authenticated key exchange(AKE) protocols.In the eCK model,the adversary can make queries on the test session,and reveal both ephemeral private keys,both long-term keys,or one of each from the two different parties.In this paper,we analyze two AKE protocols designed in the eCK model based on the definition of eCK model.We propose ephemeral keys compromised attacks and long-term keys compromised attacks on one of them,and also propose ephemeral keys compromised attacks on the other one.The results of analysis show that both of them are insecure in the eCK model.

Journal of Wuhan UniversityJan 1, 20100 citations

Security extension for the Canetti-Krawczyk model in identity-based systems

LIXinghua, MAJianfeng, SangJaeMoon

The Canetti-Krawczyk (CK) model is a formalism for the analysis of keyexchange protocols, which can guarantee many security properties for the protocols proved secure by this model. But we find this model lacks the ability to guarantee key generation center (KGC) forward secrecy, which is an important security property for key-agreement protocols based on Identity. The essential reason leading to this weakness is that it does not fully consider the attacker's capabilities. In this paper, the CK model is accordingly extended with a new additional attacker's capability of the KGC corruption in Identity-based systems, which enables it to support KGC forward secrecy.

Science China Information SciencesJan 1, 20050 citations

Universally Composable Notions of Key Exchange and Secure Channels (Extended Abstract)

Ran Canetti, Hugo Krawczyk

Recently, Canetti and Krawczyk (Eurocrypt'2001) formu- lated a notion of security for key-exchange (ke) protocols, called SK- security, and showed that this notion suffices for constructing secure channels. However, their model and proofs do not suffice for proving more general composability properties of SK-secure ke protocols. We show that while the notion of SK-security is strictly weaker than a fully-idealized notion of key exchange security, it is sufficiently robust for providing secure composition with arbitrary protocols. In particular, SK-security guarantees the security of the key for any application that desires to set-up secret keys between pairs of parties. We also provide new definitions of secure-channels protocols with similarly strong com- posability properties, and show that SK-security suffices for obtaining these definitions. To obtain these results we use the recently proposed framework of uni- versally composable (UC) security. We also use a new tool, called non- information oracles, which will probably find applications beyond the present case. These tools allow us to bridge between seemingly limited indistinguishability-based definitions such as SK-security and more pow- erful, simulation-based definitions, such as UC security, where general composition theorems can be proven. Furthermore, based on such compo- sition theorems we reduce the analysis of a full-fledged multi-session key- exchange protocol to the (simpler) analysis of individual, stand-alone, key-exchange sessions.

Jan 1, 200219 citations