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.
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.
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.
With the advancement in Internet-based technologies, network applications are no longer just limited to one-to-one communication; instead, it has become a publicly accessible resource. Regardless of this growth, such applications bring specific challenges concerning authentication, integrity, and privacy. Cryptography stands as an ideal solution to overcome these issues through an interactive method of secure communication called Key Exchange. Key exchange protocols allow two or more entities to agree upon a shared secret transmitted over a public channel without revealing any information to an eavesdropper.
This thesis contributes to the design and analysis of the variants of key exchange protocols along with their applications. As per the security requirements, the proposed schemes are either designed in an interactive model or a non-interactive model. Each scheme undergoes a series of formal and informal security analysis. The formal analysis provides simulation result using cryptographic models. Whereas, an informal analysis showcases the theoretical proves on known attacks where an adversary controls the network. The performance analysis maps the protocol’s efficiency based on the computation cost and communication size.
The first contribution introduces an interactive two-party authenticated key exchange protocol. We begin by investigating the security flaws in an existing system such as, lack of user anonymity, trace attack, clogging attack, and failure to resist replay attack. Then proposed an authenticated self-certified key exchange protocol that overcomes the addressed issues. Also, it eliminates the requirements of a trusted certificate authority to authorize the entities. The scheme achieves anonymity during session execution, mutual authentication and enables session key agreement.Based on the ideology, an application is designed, forsecure communication between ad-hoc nodes in a mobile ad-hoc network.
The second contribution contributes to the design of an Identity-based authenticated three-party key exchange protocol that overcomes the incapability of managing huge
peer-to-peer communication and high computation cost faced by two-party authenticated key exchange protocols. The proposed scheme preserves user privacy by enabling the property of anonymity and ensures non-repudiation. Based on the ideology, an application is designed to establish a secure session key between two users with the help of a trusted server for an electronic payment system.
The third contribution proposes an interactive pairing-free certificateless authenticated group key agreement scheme suitable for a resource constrained mobile network. The scheme allows any user to join or leave the group dynamically. The key agreement protocol devised in this scheme ensures un-deniability property by incorporating the signcryption, and unsigncryption algorithm.
The final contribution presents a non-interactive Identity-based deniable authentication protocol that allows an intended receiver to identify the origin of a given message without being able to prove sender’s identity to a third party.
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.
Abstract. In 2001, Canetti and Krawczyk proposed a security model (CKmodel) for authentication protocols. They also gave an indistinguishabilitybased definition for key exchange protocols. Since then the model has almost exclusively been used for analyzing key exchange protocols, although it can be applied to authentication protocols in general. The model not only captures a large class of attacks but also provides a modular approach to the design of authentication protocols. However, the model does not capture the property of Key Compromise Impersonation (KCI) Resilience. Until now, analysis concerning this property has mostly been done heuristically and restricted to key exchange protocols only. Previous attempts on formalizing KCI have mostly been done in some ad hoc manner and additional proofs have to be given specifically for the security of KCI resilience. In this paper, we propose an extension to the CK-model, which allows, for the first time, the KCI attacks to be considered in authentication protocols in general, rather than restricted to key exchange protocols, and no more additional proofs are required specifically for KCI security. With the revival of interest in identity-based (ID-based) cryptography, there have been many new ID-based key exchange protocols proposed. Despite the fact that some of them have been proven in some restricted versions of a model proposed by Bellare and Rogaway in 1993 and some others have been proven in the original CK-model, there is no rigorous model specifically for ID-based key exchange security. In particular, forward secrecy against compromised Key Generation Server (KGS-FS) has never been captured even though this notion is more important and stronger than the perfect forward secrecy in ID-based key exchange. For this, we further extend our model to ID-based setting and capture the property of KGS-FS for ID-based key exchange security. 1
A new formal security model for session key exchange protocols in the public key setting is proposed, and several efficient protocols are analyzed in this model. The relationship between this new model and previously proposed models is explored, and several interesting, subtle distinctions between static and adaptive adversaries are explored. We also give a brief account of anonymous users. 1 Introduction In this paper, we investigate formal models of security for authenticated key exchange protocols in a public key setting where the only trusted party is an off-line certification authority. Our work follows up on that of Bellare, Canetti, and Krawczyk [2], which is grounded in the multi-party simulatability tradition (see, e.g., [1]). This approach seems very attractive, because it formulates security in terms of the service a session key protocol should provide to a higher level protocol, rather than getting mired in the details of session key protocols themselves, many of which ar...
In cellular systems, user devices (UEs) establish secure sessions with each other through a trusted server such as the Home Subscriber Server (HSS) or Authentication Center (AuC). The proposed two-party authenticated key establishment allows two users to authenticate and exchange encrypted data with minimal involvement of the server -improving efficiency and scalability in mobile communication. Moreover, this paper presents a cryptanalysis of two post-quantum authentication and key agreement protocols proposed by Dabra et al. and Kumar et al. Our analysis identifies specific weaknesses, a design flaw in the registration phase of Dabra et al.’s protocol, and vulnerabilities to identity guessing and impersonation attacks in Kumar et al.’s scheme. Motivated by these findings, we propose a new communication framework for a two-party authenticated key establishment protocol assisted by a server. In the proposed model, user UA initiates communication by sending a request to a central server and receives a corresponding response to establish an authenticated session key with user UB. Notably, user UB does not need to interact with the server during session initiation or key derivation phases, thereby significantly reducing communication overhead and enhancing efficiency. Through extensive formal analysis and simulation, our protocol achieves 21.37% and 19.99% improvement in computational efficiency and 35.13% and 21.05% reduction in communication overhead compared to the lattice-based authenticated key agreement protocols of Dabra et al. and Kumar et al., respectively. Furthermore, the proposed scheme ensures key freshness, meaning that each session key is unique and has never been used in any prior communication session. This guarantees that every session remains protected by a distinct cryptographic key, even when the same users communicate repeatedly. Additionally, user UA can establish a secure session with user UB without revealing its identity to either UB or any intermediate server, thereby preserving user anonymity. Overall, the proposed protocol offers strong privacy guarantees while enabling secure, authenticated communication with a minimal number of message exchanges.