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

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

• Type: Journal
• Year: 2008
• Where: JUCS
• Authors: Guomin Yang, Duncan S. Wong, Xiaotie Deng
• Keywords: JUCS 2008, Key Exchange, Secure Roaming, Secure Roaming Scenario