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 roam- ing 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 ap- proach 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.