Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

IGI Global eBooks

The Provably Secure Formal Methods for Authentication and Key Agreement Protocols

Jianfeng Ma, Xinghua Li

Published Jan 1, 2008• 1 citation
Publisher

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.

DOI
10.4018/978-1-59904-899-4.ch015

Related papers

The Provably Secure Formal Methods for Authentication and Key Agreement Protocols

Jianfeng Ma, Xinghua Li

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.

IGI Global eBooks•Jan 18, 2011•0 citations

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, 2020•21 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 yanjiu•Jan 1, 2010•0 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 University•Jan 1, 2010•0 citations

On Formal Models for Secure Key Exchange.

Victor Shoup

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...

•Jan 1, 1999•323 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 Sciences•Jan 1, 2005•0 citations
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.
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 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.
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.
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.
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...
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.