Mipshop V. Narayanan Internet-Draft Motorola Expires: December 30, 2005 N. Venkitaraman Motorola Labs H. Tschofenig Siemens G. Giaretta TILab J. Bournelle GET/INT June 28, 2005 Handover Keys Using AAA draft-vidya-mipshop-handover-keys-aaa-00.txt Status of this Memo By submitting this Internet-Draft, each author represents that any applicable patent or other IPR claims of which he or she is aware have been or will be disclosed, and any of which he or she becomes aware will be disclosed, in accordance with Section 6 of BCP 79. Internet-Drafts are working documents of the Internet Engineering Task Force (IETF), its areas, and its working groups. Note that other groups may also distribute working documents as Internet- Drafts. Internet-Drafts are draft documents valid for a maximum of six months and may be updated, replaced, or obsoleted by other documents at any time. It is inappropriate to use Internet-Drafts as reference material or to cite them other than as "work in progress." The list of current Internet-Drafts can be accessed at http://www.ietf.org/ietf/1id-abstracts.txt. The list of Internet-Draft Shadow Directories can be accessed at http://www.ietf.org/shadow.html. This Internet-Draft will expire on December 30, 2005. Copyright Notice Copyright (C) The Internet Society (2005). Abstract This document describes a AAA-assisted key management protocol to Narayanan, et al. Expires December 30, 2005 [Page 1] Internet-Draft Handover Keys Using AAA June 2005 generate session keys between a mobile node (MN) and an access router (AR) for the purpose of securing handoff signaling messages. As such, it specifies a message exchange between the MN and the AR, payloads to carry keying material and parameters in the AAA infrastructure, and assumptions that must hold in order for this protocol to work. The idea is that the key derived between a mobile node and an access router through this protocol can be used in fast handovers (both IPv4 and IPv6). Table of Contents 1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.1 Goals and Assumptions . . . . . . . . . . . . . . . . . . 3 1.2 Applicability . . . . . . . . . . . . . . . . . . . . . . 4 2. Terminology . . . . . . . . . . . . . . . . . . . . . . . . . 5 3. Protocol Overview . . . . . . . . . . . . . . . . . . . . . . 5 3.1 Mobile Node Handoff Related Operation . . . . . . . . . . 7 4. Message Formats . . . . . . . . . . . . . . . . . . . . . . . 7 4.1 Handover Key Request (HKReq) . . . . . . . . . . . . . . . 8 4.2 Handover Key Response (HKResp) . . . . . . . . . . . . . . 9 5. Protocol Details . . . . . . . . . . . . . . . . . . . . . . . 10 5.1 Mobile Node Considerations . . . . . . . . . . . . . . . . 11 5.2 Access Router Considerations . . . . . . . . . . . . . . . 12 5.3 AAA Server Considerations . . . . . . . . . . . . . . . . 14 6. Security Considerations . . . . . . . . . . . . . . . . . . . 15 6.1 Procedure to establish a Handover Master Key . . . . . . . 15 6.2 Authentication and key exchange protocol . . . . . . . . . 16 6.3 AAA infrastructure . . . . . . . . . . . . . . . . . . . . 19 6.4 FMIPv6 . . . . . . . . . . . . . . . . . . . . . . . . . . 19 7. IANA Considerations . . . . . . . . . . . . . . . . . . . . . 19 8. Acknowledgments . . . . . . . . . . . . . . . . . . . . . . . 19 9. References . . . . . . . . . . . . . . . . . . . . . . . . . . 19 9.1 Normative References . . . . . . . . . . . . . . . . . . . 19 9.2 Informative References . . . . . . . . . . . . . . . . . . 20 Authors' Addresses . . . . . . . . . . . . . . . . . . . . . . 20 A. Deriving the Handover Master Key . . . . . . . . . . . . . . . 21 A.1 Identity Derivation for the Mobile Node . . . . . . . . . 23 B. RADIUS Handover Key Attributes . . . . . . . . . . . . . . . . 23 C. Diameter Handover Key Application . . . . . . . . . . . . . . 26 C.1 New Messages . . . . . . . . . . . . . . . . . . . . . . . 26 C.2 AVPs . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 C.3 Diameter Flow of Messages . . . . . . . . . . . . . . . . 26 D. Alternate Approaches . . . . . . . . . . . . . . . . . . . . . 27 E. Formal Analysis . . . . . . . . . . . . . . . . . . . . . . . 28 Intellectual Property and Copyright Statements . . . . . . . . 32 Narayanan, et al. Expires December 30, 2005 [Page 2] Internet-Draft Handover Keys Using AAA June 2005 1. Introduction Fast Mobile IPv6 FMIPv6 [1] specifies a fast handoff protocol for IPv6 mobile nodes. It requires tunneling of packets from an old access router to the mobile node. For this purpose, the FMIPv6 signaling messages between the mobile node and the access router must be secured to ensure FMIPv6 support for a legitimate mobile node that has been authorized to obtain such services. The FMIPv6 protocol itself does not provide a method to establish a session key and the corresponding parameters between the mobile node and the access router required for this purpose. This document describes a AAA-assisted key management protocol to generate session keys between a mobile node and an access router for usage in the context of FMIPv6. As such, it specifies: o A message exchange between the MN and the AR o Payloads to carry keying material and parameters in the AAA infrastructure o Derivation of a new session key for handoff purposes based on a shared secret 1.1 Goals and Assumptions This document has been written with the following goals and assumptions in mind. o The protocol is designed to leverage the existence of AAA infrastructure to establish session keys for securing Fast MIPv6 signaling messages. AAA is widely deployed today due to the usage of AAA-based network access authentication infrastructure. The AAA server is used to authenticate and authorize the MN for fast handovers prior to generation of the handover key. The solution presented in this document relies on the AAA infrastructure components to derive and distribute keying material keys for handover support. o A Handover Master Key (HMK) between the MN and the home AAA server (AAAH ) is required for this protocol to be able to derive handover keys between the MN and AR. The exact method of establishing or deriving this HMK is outside the scope of this document. No particular method is mandated for this protocol to work but we illustrate an example approach using the Application Master Session Key (AMSK), as defined in EAP, in Appendix A. Due to deployment considerations, it may be practical to use the Narayanan, et al. Expires December 30, 2005 [Page 3] Internet-Draft Handover Keys Using AAA June 2005 method to derive the HMK. o Key naming of the HMK is provided using the Network Access Identifier (NAI). In order to provide identity protection, it may be undesirable to reuse the same NAI as used for network access authentication. For sake of identity protection, it may be desirable to have the AAA server to derive an ephemeral identity at the time of HMK creation that can be used in subsequent creation of handover keys. o It is further assumed that a security association exists between each AR and the AAA server. If a AAAL or other proxies are used (as it is typical in a roaming environment) then the AR will likely share a security association only with its local AAA server (AAAL) instead of the user's home AAA server (AAAH). The AAAL in this case acts as a AAA proxy between the AR and the AAAH server. These security associations protect the signaling message exchange including the transport of keying material and other security sensitive parameters. o The protocol does not introduce any new required steps at the time of handover. Any new messages introduced for deriving handover keys can be exchanged prior to the handover process. o The protocol has been designed such that the compromise of one AR does not lead to the compromise of any other AR. No AR is able to view the key of another AR - keys are transferred securely from the AAA server directly to the AR requesting it. 1.2 Applicability Although this document is focused on FMIPv6, it is applicable to other protocols as well. In the context of FMIPv6, the key derived using this protocol can be used to secure the Fast Binding Update (FBU) sent from the MN to the PAR as specified in FMIPv6 [1]. This protocol can be used to derive keys for fast handovers in IPv4 as well. Keys can be derived for secure IPv4 low latency handoffs LOWLAT [5] based on this protocol. CxTP [6] can also use this protocol to derive keys between the AR and MN to secure the CTAR message. Additionally, keys between an MN and a MAP can be derived using this protocol for HMIPv6 [7] operation. In order for this protocol to be used to create session keys for more than one application (e.g. FMIPv6 and CxTP) between the same {MN, AR} pair, application specific key derivation will be addressed in a future revision of this draft. The document is organized as follows. Section 2 describes the Narayanan, et al. Expires December 30, 2005 [Page 4] Internet-Draft Handover Keys Using AAA June 2005 terminology used in this document. Section 3 provides a general protocol overview. Section 4 details the message formats. Section 5 provides protocol details on mobile node and access router operation. Section 6 describes the security considerations for this protocol. Appendix A provides a method of deriving the handover master key using EAP. Appendices B and C describe the AAA messages and attributes necessary for this protocol in RADIUS [2] and Diameter [3] respectively. Appendix D provides brief descriptions of alternate approaches for handover key derivation along with the disadvantages of those alternatives. 2. Terminology The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in RFC- 2119 RFC2119 [4]. In addition, this document uses the following terms: MN-AAA Handover Master Key (HMK): A key that is shared between the Mobile Node and the AAAH server, hereby referred to simply as the Handover Master Key. Handover Key (HK): Session key used to secure messages between the Mobile Node and Access Router. A given HK between an MN and ARn is termed as HKn. ARn-AAA Key: A key that is shared between an Access Router ARn and the AAA server. In a roaming case, the ARn shares this key with the AAAL server. 3. Protocol Overview This section provides a description of the procedure to obtain the Handover Key (HK). We assume that the MN shares a session key, called Handover Master Key (HMK), with the AAA (AAAH) server. This key, for instance, may be the derived from the EAP key hierarchy. Appendix A describes a method of deriving the HMK and an identity for the MN from the EAP Application Master Session Key (AMSK). This method can be used whenever possible. For the purpose of the protocol itself, the HMK may simply be a handover specific master key pre-shared between the MN and the AAA server. Narayanan, et al. Expires December 30, 2005 [Page 5] Internet-Draft Handover Keys Using AAA June 2005 Figure 1 depicts the high-level protocol interaction. MN AR AAAH Server | HKReq. | | | ---------> | | | | AAA (RADIUS Access Request) | | | ----------------------> | | | AAA (RADIUS Access Accept) | | | <----------------------- | | HKResp. | (Keying material) | | <--------- | | Figure 1: Protocol Operation The MN, upon attaching to an AR (say AR1) in a given administrative domain, sends a Handover Key Request (HKReq) message to the AR. The very first time the MN attaches to the domain, it completes successful Mobile IP registration prior to sending the HKReq message. The MN then creates a HKReq message including a NAI alike identifier (that was derived possibly during the time of HMK derivation), a message ID, a sequence number and a keyed message digest of these fields by using the HMK. AR1 forwards the HKReq message to the AAA Server via the AAA infrastructure. The keyed message digest allows the home AAA server to authenticate the MN and to perform authorization for fast handoffs before deriving unique and fresh session key, the Handover Key (HK1). The keyed message digest is calculated as follows: MN-AAA MAC = PRF(HMK, MN ID | Message ID | Sequence Number), where | indicates concatenation. HK1 will subsequently be used between the MN and the AR1 after a successful protocol execution. The key derivation procedure for the Handover Key is defined as follows: HK1 = PRF(HMK, AAA-MN Nonce | AR1 ID | MN ID, "Handover Key"), where | indicates concatenation The AR1 ID is the IP address of AR1. The MN ID is the NAI of the MN that is sent by the MN in the HKReq message. The AAA-MN Nonce is a nonce generated by the AAA server for the purpose of HK1 derivation. After successful authentication and authorization the AAA Server then sends two different parameters to AR1 - one of the parameters includes the session key HK1 and the lifetime associated with it. The other parameter, to be sent to the MN, includes the AAA-MN Nonce. A keyed message digest computed based on the HMK is included with Narayanan, et al. Expires December 30, 2005 [Page 6] Internet-Draft Handover Keys Using AAA June 2005 this parameter to the MN. The message is protected with the AR1-AAA SA when forwarded to AR1. AR1 sends a Handover Key Response (HKResp) to the MN, including the material (nonce) sent by the AAA server and also the key lifetime it received from the AAA server. Using this keying material, the MN derives HK1. When the MN is ready to send an FBU to AR1 (in accordance with FMIPv6 [1]), it uses HK1 to secure the FBU message. 3.1 Mobile Node Handoff Related Operation The MN may learn about the neighboring ARs while it is attached to AR1. This may be done by exchanging the RtSolPr and PrRtAdv messages as defined in FMIPv6 [1] or via layer 2 mechanisms. As soon as it learns about its neighboring ARs, the MN sends HKReq message to those ARs. Assuming that AR2 is a neighbor of AR1, the MN sends a HKReq to AR2 through AR1, while still attached to AR1. AR2 correspondingly sends the message in a AAA protocol to the AAA server. The AAA server generates HK2 for the MN as a derivative of HMK as shown below: HK2 = PRF (HMK, AAA-MN Nonce | AR2 ID | MN ID, "Handover Key"), where | indicates concatenation. Fresh nonces are generated by the AAA server for every handover key generation and sent to the MN through the AR in every HKResp. The AAA server sends HK2 and the corresponding lifetime to AR2, protected by the AR2-AAA SA. As before, the AAA server also sends the keying material for the MN (AAA-MN Nonce, hashed with HMK). AR2 sends the parameters from the AAA server to the MN via AR1, in a HKResp message. If the MN hands off prior to receiving the HKResp from AR2, it re- sends the HKReq message with the same message ID, to AR2, upon attaching to it. AR2 re-sends the HKResp sent earlier via AR1 to the MN directly in this case. This does not add to the handoff delay, since HK2 is required to authenticate the FBU sent only when the MN is performing a handoff from AR2 to a third AR. The MN sends a new HKReq to any new neighbors it receives information about, while attached to AR2. 4. Message Formats This protocol will run over UDP well known port number . This section presents the description of the HKReq and HKResp messages that this protocol uses. The description Narayanan, et al. Expires December 30, 2005 [Page 7] Internet-Draft Handover Keys Using AAA June 2005 of AAA attributes that are needed for this protocol are described in Appendices B and C. Appendix B provides the attributes for RADIUS and Appendix C describes a Diameter handover application. 4.1 Handover Key Request (HKReq) 0 1 2 3 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Message Type |V| Reserved | Message Length | +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Message Identifier | Message Sequence Number | +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Type=1 | Length | MN ID .......| +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Type=2 | Length | MN-AAA-MAC .......| +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Type=3 | Length | MN-AR-MAC .... | +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Padding... +-+-+-+-+-+-+-+-+ This message is sent from a mobile node to an access router, either directly or via another access router to which the MN is attached. IP Addresses IP Source Address = Care-of-address of MN IP Destination Address = AR IP address HKReq Fields Message Type = 1 v - Verify flag. This is set by the MN to indicate that it may already share a key with MN. Message length = length of message including all the TLVs but excluding padding Message ID - A value that can uniquely identify the message to both the AR and MN Sequence number - MUST be set to 1 for the first transmission and incremented by 1 for every retransmission Narayanan, et al. Expires December 30, 2005 [Page 8] Internet-Draft Handover Keys Using AAA June 2005 MN-ID TLV - The NAI of the MN. This value MUST always be included MN-AAA MAC - TLV of type 2 MUST be present if v=0. This is the hash of the message ID, sequence number and the MN-ID TLV. It MAY be present if v=1 MN-AR MAC - TLV of type 3; this MUST be present if v=1. This is the hash of the message up to this TLV 4.2 Handover Key Response (HKResp) 0 1 2 3 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Message Type |V| Reserved | Message Length | +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Status Code | Lifetime | +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Message Identifier | Message Sequence Number | +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Type=4 | Length | AAA-MN Nonce .......| +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Type=2 | Length | MN-AAA MAC .......| +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Type=3 | Length | MN-AR-MAC .... | +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Padding... +-+-+-+-+-+-+-+-+ This message is sent from an access router to a mobile node, either directly or via another access router to which the MN is attached. IP Addresses IP Source Address = AR IP address IP Destination Address = Care-of-address of MN HKResp Fields Message Type = 2 V - Verified Flag - Set by the AR in response to a HKReq with the V bit set, if it verified the request Narayanan, et al. Expires December 30, 2005 [Page 9] Internet-Draft Handover Keys Using AAA June 2005 Reserved - set to zero Message Length - Length of the full message excluding padding Status Code - Indicates status of the message; the following values are defined: 0 - success 1 - unable to verify 2 - invalid MN-AR MAC 3 - MN-AR MAC TLV needed 4 - MN-AAA MAC TLV needed 5 - Invalid MN-AAA MAC (sent by AAA server) Lifetime - Recommended lifetime from AAA server when received from the AAA server; when AR is verifying a request from MN, this field MUST be set to the remaining lifetime of the handover key maintained by the AR. Message ID - uniquely identifies the message (copied from the corresponding HKReq) Sequence number - MUST be set to 1 for the first transmission and incremented by 1 for every retransmission AAA-MN nonce - TLV of type 4; a random value of at least 128 bits generated by the AAA server to be used to derive the key to be shared between MN and AR MN-AAA MAC - MUST be present if V=0 and Status Code = 0; MUST NOT be present when V=1; This field is the hash of the AAA-MN Nonce, when V=0 MN-AR MAC - MUST be present if V=1 and Status Code = 0; MUST NOT be present when V=0; This is a hash of the message up to this TLV 5. Protocol Details The proposed protocol enables a MN to derive session keys (HKs) with its current AR and with neighboring ARs. This section describes the processing rules for the mobile node and the access router. AAA Narayanan, et al. Expires December 30, 2005 [Page 10] Internet-Draft Handover Keys Using AAA June 2005 server considerations are addressed in Appendices B and C, along with the description of the AAA attributes. 5.1 Mobile Node Considerations After completing MIPv6 signaling the mobile node SHOULD immediately proceed to obtain a session key between itself and its current AR. It does not have to wait for information about any neighbor AR information. If the MN does not receive a response after a configured timeout (HKEY_REQ_TOUT), it SHOULD retransmit the request for a maximum of N HO_KEYTRIES. In each of the retry attempts, the MN MUST use the same message ID. The default value of N_HO_KEYTRIES is 3. When the MN receives information about neighboring routers it SHOULD first determine whether the MN already shares keys with the one or more of the identified access routers. With each neighboring AR with which a MN does not share a key, the MN SHOULD start the process by sending HKReq even when connected to the current AR. If the MN, which had sent a HKReq corresponding to a nAR, hands off before receiving a response, the MN MAY receive the HKResp directly when it gets connected to the nAR (provided the AR still has the response buffered). This response MAY be sent unsolicited, i.e., nAR may forward the HKResp to MN once it realizes the presence of the mobile (e.g., receives the FNA from MN). If the MN does not receive this response it MAY retransmit a HKReq after a configured timeout (UNSOLICITED_HKRSP_TO). As indicated before, the retransmission MUST use the same message id to enable the nAR respond immediately if it has already received a response from AAA for the corresponding HKReq. It is up to the end points (MN/AR) to enforce the key lifetimes. The AAA server does not store or enforce the lifetime. A new session key (HK) should be derived before the lifetime expires on the current key. When a MN attaches an AR with which the MN believes it has a shared key, i.e., the MN has already received a HKResp from the AR, the MN MUST verify that by sending a HKReq with the verify flag set and a hash of the message with the MN-AR key. The MN MUST include this hash in the MN-AR MAC TLV in this case. This procedure serves two purposes. It is used to verify the validity of the key and also bind the key with the MN CoA. In a protocol like FMIPv6, the FBU only contains the CoA of the MN. Hence, when receiving an FBU secured with the handover key, the AR must be able to retrieve the correct key corresponding to the MN, based on the contents of the FBU. This message makes it possible. For this purpose, this message MUST be sourced with the CoA that the MN acquired at the AR. The MN MAY Narayanan, et al. Expires December 30, 2005 [Page 11] Internet-Draft Handover Keys Using AAA June 2005 include its CoA in an Alternate CoA Option (defined in FMIPv6 [1]). This verification procedure is also needed to accommodate cases where an AR rebooted after getting the shared key leading the MN to believe that is shared a key with the AR. In response, the MN may receive a HKResp with verified bit set and a hash of the HKResp message. If the AR did not have the key, the MN will receive a standard HKResp with verified bit set to 0. Note that the message id must be different from the one used to create the previous MN-AR key because this is not a retransmission and if the AR did not have the key this message may simply trigger normal HKReq reception procedure. If the MN receives a HKResp message with the 'V' bit set, but without the MN-AR MAC TLV, it MUST silently discard the message. If the MN receives a HKResp with the 'V' bit set to zero, but without the AAA Auth TLV, it MUST silently discard the message. If the MN receives a HKResp with the 'V' bit set to one and with the MN-AAA MAC TLV, it MUST silently discard the message. If the MN receives the HKResp with the 'V' bit set to zero and with the MN-AR MAC TLV, it SHOULD discard the message. 5.2 Access Router Considerations When an AR receives a HKReq from a MN it MUST first determine if it has the 'V' bit set. If so, the AR MUST use the included MN ID to lookup the MN and obtain the key. If a key is present and the computed keyed message digest matches the values included in the HKReq message, the AR MUST send a response with the verified bit set including the hash of the response. Also, the AR MUST record the CoA of the MN as the IP address associated with the handover key for that MN, in addition to the MN ID (NAI). This is required so that the AR can pull up the correct key upon receiving a message (like the FBU) from the MN with the CoA. If the HKReq message included an Alternate CoA Option (as defined in FMIPv6 [1]), the AR MUST use the IP address in that option as the MN CoA. If not, the AR MUST use the source IP address of the HKReq message as the CoA of the MN. If the MN-AR MAC TLV is not present in the HKReq in this case, the AR MUST drop the message and return a HKResp with the error code set to 3. Also, if the MN-AR MAC TLV was included but the AR was unable to verify the keyed message digest, it MUST drop the message and return a HKResp with the error code set to 2. If the AR does not have the key or if the HKReq does not have the verify bit set, the AR does the following. It MUST first determine if it has already seen the same message request by checking its tables using the message id and the included MN ID as index. If so and if the AR has already received the HKResp, the AR SHOULD retransmit the response to the MN. If the received message has the same message ID and the sequence number as before, Narayanan, et al. Expires December 30, 2005 [Page 12] Internet-Draft Handover Keys Using AAA June 2005 the AR MUST drop the packet. The sequence number alone cannot entirely thwart replay attacks, since a HKReq that does not have the verify bit set, only has a hash with the HMK that the MN shares with the AAA server. Hence, there is no way for the AR to verify the legitimacy of the hash in the message. This could lead to replay attacks going unnoticed at the AR when the attacker increments the sequence number, but replays the message with the same hash. This message will only be dropped at the AAA server. For simple replay protection, the AR MUST drop packets that are sent with the same sequence number for the same message ID. For further protection from replays, the rate of retransmissions of responses to MN MUST not be more than a preconfigured RETRANS_RATE. If the AR already forwarded this message to the home AAA Server but has not yet received a response from AAA server, the AR MUST silently discard the retransmitted request from the MN. Note that the AAA protocol should independently perform its own retransmission. If this is a new request, the AR MUST check to determine if the MN-AAA MAC TLV has been included in this message by the MN. If it has been included, then the AR MUST forward the request to the home AAA Server. If it has not been included, the AR MUST drop the message and return a HKResp to the MN with the error code set to 1. The AR MUST construct a AAA message using the appropriately defined attributes (defined in Appendix B for RADIUS and Appendix C for Diameter). For instance, the AR MUST include the MN ID from the HKReq message in a HK-MN-ID attribute in a RADIUS Access Request message. Also, the MN-AAA MAC TLV MUST be included in the HK-MN-AAA- Authenticator attribute. The AR MUST include the NAS-IP-Address AVP in the AAA message (e.g. RADIUS Access Request) sent to the AAA server. The AR MUST use its IP address as seen by the MN in this AVP. This will be used as the AR ID in deriving the handover key. The domain name in the NAI is used to determine the AAA server to be contacted. Note that if there is a local AAA server that is different from the MNs AAA server, then the AR may send the message via the AAA protocol to the Local AAA server which in turn would forward the request. The AAAL will act as a AAA proxy in this case. If the AR receives a RADIUS Access Accept message from the AAA server, it MUST send the AAA-MN Nonce and the AAA Authenticator from the HK-MN-AAA-SHASH attribute in the RADIUS message in the HKResp message to the MN. It MUST also send the key lifetime sent by the AAA server to the MN in the same message. If the AR receives a RADIUS Access Reject message from the AAA server, the AR MUST send an appropriate error code to the MN in the HKResp message. Narayanan, et al. Expires December 30, 2005 [Page 13] Internet-Draft Handover Keys Using AAA June 2005 When the AR sends a HKResp, it SHOULD determine if the MN is directly connected to it. If so it should forward the packet to the MN directly. If the MN is not attached directly then the AR SHOULD send the packet to the MN via the current AR. In any case the AR SHOULD buffer the packet for a maximum value of HKEY_REQ_TOUT, so that it can be retransmitted if needed. An AR SHOULD maintain the keys such that it could be looked up based on the MN ID, last CoA that the MN has with the AR. It must also maintain the message id that was used to create the key. The MN ID is needed to verify the HK, while the message ID is required to determine retransmitted HKReq messages. The CoA is needed to determine the key to use when the FBU is received. Since the MN ID is not included in the FBU, tracking the key only based on the MN ID is insufficient for using it with FMIPv6. If the MN that returns to a AR and obtain a new CoA, this message should be updated based on HKReq from the MN for verification. If a pAR receives a HKResp destined to a MN that is no longer connected to it, indicating that the MN roamed away from the pAR, it SHOULD silently discard it. 5.3 AAA Server Considerations A description of the actual AAA attributes is included in Appendices B and C. This section provides a brief description of the operation of the AAA server for this protocol. Upon receiving a handover key request, the AAA server MUST verify that the MN-AAA MAC TLV is present in the message. If the MN-AAA MAC TLV is absent, the AAA server MUST silently discard the message. Otherwise, the AAA server MUST verify the keyed message digest included in the MN-AAA MAC TLV. If the MN-AAA MAC TLV is invalid, the AAA server MUST silently discard the message. If the hash is valid, the AAA server must proceed with the handover key generation as follows. If the NAS-IP-Address AVP was not included in the request, the AAA server MUST return an error to the AR, indicating that it is required. The AAA Server calculates the Handover Key for the {MN,AR} pair as follows. HK = PRF(HMK, AAA-MN Nonce | AR ID | MN ID, "Handover Key"), where | indicates concatenation. The AR ID is the IP address of the AR included in the NAS-IP-Address AVP in the request. The MN ID is obtained from the HK-MN-NAI attribute included in the RADIUS Access Request. The AAA-MN Nonce is Narayanan, et al. Expires December 30, 2005 [Page 14] Internet-Draft Handover Keys Using AAA June 2005 generated by the AAA Server. The Handover Master Key (HMK) is shared between the MN and the AAA server. The AAA server MUST send a response back to the AR, including the AAA-MN Nonce as well as the derived HK, encrypted with the AR-AAA SA. The AAA server SHOULD include a lifetime for the HK in the RADIUS Access Accept message. The AAA server is, however, not required to store the key or the lifetime. The MN-AAA MAC TLV MUST be calculated as a hash of the AAA-MN-Nonce using the HMK that the AAA Server shares with the MN and MUST be included in the RADIUS Access Accept message. 6. Security Considerations This document uses a number of building blocks that need to interwork in order to secure the protocol described in this document. The extensions defined for RADIUS and Diameter will be separated from this document in a future version. The following aspects need to be considered from a security point of view: 1. Mechanism to establish a Handover Master Key 2. Authentication and key exchange protocol executed between the MN and the AAA server (via the AR) 3. AAA infrastructure to exchange the necessary parameters and session keys between the AR and the AAA server 4. FMIPv6 protocol (or other signaling protocols) 6.1 Procedure to establish a Handover Master Key Appendix A provides an example for the establishment of the Handover Master Key (HMK) but does not mandate a particular procedure. The aspect of user identity privacy (i.e., the linking between the identity used for network access authentication and the identify used for the MN-HA authentication protocol) needs to be considered to prevent impacting the privacy properties of the underlying EAP-based network access authentication procedure. Furthermore, the lifetime of the established HMK and a new NAI-based identity need to be created to allow proper key naming. Further details are discussed in Appendix A. Narayanan, et al. Expires December 30, 2005 [Page 15] Internet-Draft Handover Keys Using AAA June 2005 6.2 Authentication and key exchange protocol This document defines a shared secret based authentication protocol with the following properties: Authentication: The protocol provides mutual authentication based on a pre-shared secret, the Handover Master Key (HMK). Authentication of the server is provided implicitly since the server's identity is not transmitted. As such, a proof of possession is provided. Freshness of the authentication protocol run is provided with the help of sequence numbers. Loss of synchronization is not yet dealt with. Dictionary Attacks: The HK is a derived key that is not subject of off-line and online dictionary attacks assuming the underlying HMK is resistant to dictionary attacks as well. Even with the HMK key derivation procedure suggested in Appendix A dictionary attacks can be defeated largely because of the requirements placed on EAP methods. Replay Protection: The authentication and key exchange protocol prevents replay attacks by using 16-bit sequence numbers. Sequence numbers must not used twice with the same keying material. Once the sequence number space is exhausted a new HK must be established. Key Derivation and Key Strength: No assumptions are made about the length of the HK. The derived HK is 160 bit due to the usage of the output length of the SHA-1 hash function. The key strength depends on the chosen nonce, which is a variable length input value with at least 128 bits chosen by the AAA server, and the HK. Key Control: Key derivation is controlled by the AAA server. Joint key control is therefore not provided. Key Naming: The HMK is selected based on the NAI provided by the MN. The NAI will most likely be different for the network access Narayanan, et al. Expires December 30, 2005 [Page 16] Internet-Draft Handover Keys Using AAA June 2005 authentication protocol and for the protocol described in this document. As a consequence of successful protocol execution the MN and the AR establish the HK. FMIPv6 does not consider naming keys other than by the IP address of the MN. Hence, the same mechanisms has to be used. If multiple session keys exist then the available keys need to be verified in order to find the suitable one. This aspect requires further coordination with the FMIPv6 authors since their document is work in progress. Lifetime: The Handover Key (HK) is associated with a lifetime. Section 3 discusses the aspects regarding enforcing lifetime of a key. The HMK also has a lifetime parameter associated with it although this document does not discuss this aspect since it is largely out of scope. For generation of the HMK only suggestions are provided in Appendix A. Denial of Service Resistance: The authentication and key exchange protocol itself is resistant to denial of service attacks. Flooding the AAA client with requests might cause problems to the AAA infrastructure since the AAA client cannot verify the validity of the request, needs to perform processing and forwards the message to the backend AAA server. To some extend it might be reasonable to think about a cookie- or puzzle-based approach as done in IKEv2/HIP to thwart this. When the AAA client (AR) thinks it is under attack, it may send a cookie to the source address of the request it received for the MN to send another request including that cookie. This will be included in future revisions of the protocol. Loss of synchronization between the MN, AR and the AAA server will be described in a future version of this document. Session Independence: Each individual protocol run is independent based on the usage of the nonce value chosen by the AAA server and the sequence numbers chosen independently by the two parties. Fragmentation: This protocol does not suffer from fragmentation due to its conservative usage of symmetric cryptography. Narayanan, et al. Expires December 30, 2005 [Page 17] Internet-Draft Handover Keys Using AAA June 2005 Channel Binding: Channel binding is not provided by this protocol. Fast Reconnect: This protocol does not provide a concept of session resumption or fast reconnects. This is, however, not necessary since a single roundtrip protocol is already a highly optimized authentication protocol. Furthermore, it is worth mentioning that the established HK at the AR (with a given lifetime) also prevents the need to perform the interaction with the AAA server frequently. Identity Protection: This protocol does not provide active or passive user identity confidentiality. The assumptions is made that the identity used during network access authentication is NOT used as part of this protocol exchange and a new identity is created periodically as part of the HK bootstrapping procedure. Protected Ciphersuite Negotiation: This protocol does not provide ciphersuite negotiation. Confidentiality: Confidentiality protection of individual payloads exchanged with the authentication protocol is not provided. Cryptographic Binding: The concept of crytographic bindings is not applicable to this document. Perfect Forward Secrecy: Perfect forward secrecy is not provided by this protocol. Key confirmation: Key confirmation of the established HK is not provided as part of the protocol exchange. However, implicit key confirmation is offered when the session key is established for protection of the FMIP protocol. An attempt to formally verify the protocol is shown in Appendix E. Narayanan, et al. Expires December 30, 2005 [Page 18] Internet-Draft Handover Keys Using AAA June 2005 6.3 AAA infrastructure This document aims to reuse the existing AAA infrastructure. As such, additional RADIUS attributes and/or a Diameter application needs to be defined to exchange the necessary parameters. The security of RADIUS and Diameter is outside the scope of this document. The standard security mechanisms available for these protocols will be utilized. 6.4 FMIPv6 The main goal of this document is to establish session keys and security parameters in order to secure FMIPv6. Although other protocols can also be benefit from the approach suggested by this document, the focus is on FMIPv6. The security threats and the need for securing FMIPv6 signaling messages is investigated in [1]. 7. IANA Considerations TBD: Details will be provided in a future draft version. 8. Acknowledgments The authors would like to thank Madjid Nakhjiri of Motorola Labs for his helpful discussions during the early stages of development of this protocol. The authors would also like to acknowledge Mike Korus and George Popovich of Motorola for their reviews and comments on this document. 9. References 9.1 Normative References [1] Koodli, R., "Fast Handovers for Mobile IPv6", draft-ietf-mipshop-fast-mipv6-03 (work in progress), October 2004. [2] Rigney, C., "Remote Authentication Dial-In User Service (RADIUS)", RFC 2865, June 2000. [3] Calhoun, P., "Diameter Base Protocol", RFC 3588, September 2003. [4] Bradner, S., "Key words for use in RFCs to Indicate Requirement Levels", BCP 14, RFC 2119, March 1997. Narayanan, et al. Expires December 30, 2005 [Page 19] Internet-Draft Handover Keys Using AAA June 2005 9.2 Informative References [5] El Malki, K., "Low Latency Handoffs in Mobile IPv4", draft-ietf-mobileip-lowlatency-handoffs-v4-09 (work in progress), June 2004. [6] Loughney, J., "Context Transfer Protocol", draft-ietf-seamoby-ctp-11 (work in progress), August 2004. [7] Soliman, H., "Hierarchical Mobile IPv6 Mobility Management (HMIPv6)", draft-ietf-mipshop-hmipv6-04 (work in progress), December 2004. [8] Aboba, B., "Extensible Authentication Protocol (EAP) Key Management Framework", draft-ietf-eap-keying-06 (work in progress), April 2005. [9] Housley, R. and B. Aboba, "AAA Key Management", draft-housley-aaa-key-mgmt-00 (work in progress), June 2005. [10] "Automated Validation of Internet Security Protocols and Applications Webpage, http://www.avispa-project.org/", http://www.avispa-project.org/, June 2005. [11] Johnson, D., Perkins, C., and J. Arkko, "Mobility for IPv6", RFC 3775, June 2004. Authors' Addresses Vidya Narayanan Motorola 1301 E. Algonquin Road Schaumburg, IL 60196 US Email: vidya@motorola.com Narayanan Venkitaraman Motorola Labs 1301 E. Algonquin Road Schaumburg, IL 60196 US Email: narayanan.venkitaraman@motorola.com Narayanan, et al. Expires December 30, 2005 [Page 20] Internet-Draft Handover Keys Using AAA June 2005 Hannes Tschofenig Siemens Otto-Hahn-Ring 6 Munich, Bavaria 81739 Germany Email: Hannes.Tschofenig@siemens.com Gerardo Giaretta TILab via G. Reiss Romoli, 274 TORINO 10148 Italy Email: gerardo.giaretta@telecomitalia.it Julien Bournelle GET/INT 9 rue Charles Fourier Evry 91011 France Email: julien.bournelle@int-evry.fr Appendix A. Deriving the Handover Master Key A Handover Master Key (HMK) between the MN and AAAH server is required for this protocol to be able to derive handover keys between the MN and AR. As mentioned earlier in the document, the exact method of derivation of this HMK is outside the scope of this document. One method of HMK derivation is presented in this Appendix and it is based on the Application Master Session Key (AMSK) defined in EAP EAPKEY [8]. The basic idea is that during the authentication for network access, the MN and the AAA server derive an AMSK and subsequently an HMK from the EAP method derived keying material. The procedure requires that the authentication for network access is based on an EAP method capable of exporting session keys. Deriving the Handover Master Key (HMK) involves requires the following steps: 1. The MN and the AAA server of the home domain undertake the EAP exchange for network access authentication. 2. At the end of the EAP exchange the EAP peers derive the Master Session Key (MSK) and the Extended Master Session Key (EMSK). As such, the EAP method MUST be capable of deriving these session Narayanan, et al. Expires December 30, 2005 [Page 21] Internet-Draft Handover Keys Using AAA June 2005 keys. 3. The MN and the AAA server derive an AMSK from the EMSK to be used as HMK. The key derivation function is described below. The lifetime of the HMK is managed as a system parameter and must not be higher than the lifetime of the EMSK (as stated in EAPKEY [8]). As a default choice the two lifetimes should be equal. Figure 4 shows how the AMSK and the HMK-AMSK is derived. EAP Peer EAP Server (MN) (AAA Server) +--------------------------------+ /-------------------------\ / EAP \ MSK \ exchange / MSK \-------------------------/ +------+ +------+ | EMSK | | EMSK | +------+ +------+ +------------+ +------------+ | HMK-AMSK | | HMK-AMSK | +------------+ +------------+ Figure 4: Key Hierarchy The HMK is derived through the key derivation function specified for AMSK in EAPKEY [8] and shown below for the sake of clarity. KDF (K,L,D,O) = T1 | T2 | T3 | T4 | ... where: T1 = prf (K, S | 0x01) T2 = prf (K, T1 | S | 0x02) T3 = prf (K, T2 | S | 0x03) T4 = prf (K, T3 | S | 0x04) prf = HMAC-SHA1 Narayanan, et al. Expires December 30, 2005 [Page 22] Internet-Draft Handover Keys Using AAA June 2005 K = EMSK L = key label D = application data O = OutputLength (2 bytes) S = L | " " | D | O The application specific parameters are set as follows: o key label = "Handover Master Key" o application data = o output length = 128 bits A.1 Identity Derivation for the Mobile Node Based on the protocol defined in this document, the MN provides its identity in the HKReq message. As this message is not encrypted, the identity used by the MN in this exchange can be seen by other, possible malicious, nodes. This should be avoided since it exposes the identity of the MN implying identity privacy concerns. To solve this issue, several EAP methods provide user identity confidentiality. Thus, an exchange of HKReq/HKResp messages that carries the MN identity in clear, will destroy the security properties of the EAP method used for network authentication. One possible approach to solve this issue is to use in the HKReq/HKResp exchange a derived identity based on a pseudonym - during the EAP method used for network access authentication and based on the cryptographic material exported by the EAP method itself, the AAA server can send to the MN an identity that the MN can use for subsequent HKReq/HKResp exchanges. Moreover, different MN identities can be derived so that the MN can use different entities in different exchanges of the protocol, in order that malicious nodes are unable to trace its movements based on the same pseudonym. Alternatively, the capability of certain EAP to establish an encrypted channel to securely exchange parameters can be exploited to secure provisioning a temporal identity. Appendix B. RADIUS Handover Key Attributes This section provides an overview of the protocol interaction between the access router and the RADIUS server to request a key for FMIPv6. The proposal assumes that the AAA exchange is authenticated, replay Narayanan, et al. Expires December 30, 2005 [Page 23] Internet-Draft Handover Keys Using AAA June 2005 protected, integrity protected and encrypted. For RADIUS, the usage of IPsec between the AR and the AAAH server is recommended. The AR acts as a AAA client in order to get a Handover Key in order to secure FMIPv6 signaling messages. A more detailed version of this section will be provided in the near future. MN AR AAAH Server | HKReq. | | | ---------> | | | | Access Request | | | ----------------------> | | | Access Accept (key mtrl)| | | <----------------------- | | HKResp. | | | <--------- | | Figure 5: RADIUS Messages As shown in Figure 5 the MN sends a HKReq to the AR. This message contains an NAI of the Mobile node and the MN-AAA Authenticator. This authenticator is the keyed message digest computed with the HMK (see Appendix A). The access router extracts the necessary information to from the attributes to be included in a RADIUS Access Request messages. This message is sent to the AAA infrastructure. The AR includes at least the IP address used with the MN in the NAS-IP attributes. The message is the following: RADIUS-Access-Request { HK-MN-MSGID-SEQ (Message ID | Sequence number from HKReq) HK-MN-NAI NAS-IP (IP Address of the AR) HK-MN-AAA Authenticator Message Authenticator(80)} The home RADIUS server receives the message and checks the validity of the HK-MN-AAA Authenticator. This authenticator value is calculated on the HK-MN-MSGID-SEQ and HK-MN-NAI. The RADIUS server Narayanan, et al. Expires December 30, 2005 [Page 24] Internet-Draft Handover Keys Using AAA June 2005 generates a Nonce of at least 128 bits (AAA-MN Nonce) and computes the Handover Key (HK1) as follows: HK1 = PRF(HMK, AAA-MN Nonce, AR1 ID, MN ID, "Handover Key") where, AR1 ID is extracted from the NAS-IP Attribute, MN ID is extracted from the NAI, and the HMK is the shared key between MN and its RADIUS server. The RADIUS server answers to the AR by sending a RADIUS-Access- Accept message. RADIUS-Access-Accept{ HK-MN-AR-Key (HK1) HK-MN-AR-Key-Lifetime (HK1's lifetime) HK-AAA-MN-Nonce (Nonce generated by AAAH) HK-MN-AAA-SHASH (PRF(HMK, Nonce || Lifetime HK1) Message Authenticator(80)} If the authentication failed (wrong MN-AAA MAC), the AAAH generates a RADIUS Access-Reject message. The AR receives the message, extracts the HK1 and its associated lifetime and creates the HKResp containing the Nonce AAA-MN, the HK1's lifetime and the signed hash. Thus, this proposal needs the following attributes to be defined: o HK-MN-NAI o HK-MN-MSGID-SEQ o HK-MN-AAA Authenticator o HK-MN-AR-Key (HK1) o HK-MN-AR-Key-Lifetime (HK1's lifetime) o HK-AAA-MN-Nonce (Nonce generated by AAAH) o HK-MN-AR-SHASH (PRF(HMK, Nonce || Lifetime HK1) It may be possible to reuse some attributes defined for Mobile IPv4 Narayanan, et al. Expires December 30, 2005 [Page 25] Internet-Draft Handover Keys Using AAA June 2005 here - such as the MIP-MN-NAI or the MIP-MN-AAA-Authenticator attribute - this possibility will be explored in later revisions of this document. Appendix C. Diameter Handover Key Application To support this proposal a new Diameter application must be defined. The intent of this section is to provide an overview of what is needed to support the proposal. Note that the proposal assumes that AAA exchanges between AR and the AAAH server is protected. Use of IPsec or TLS is recommended for this purpose. In this section, we describe needed Diameter messages and AVPs. A more detailed version of this section will be provided in the near future. C.1 New Messages As for RADIUS, the AR will act as a AAA client and thus as a Diameter client. However, new Diameter command could be defined for this proposal: o HK-Mobile-Node-Request (HMR) - Command Code (TBD) and 'R' bit set in Command Flags field. This message is sent by AR acting as a Diameter client to a AAAH in order to request the handover key for the mobile node. The AR uses the information provided in the HKreq to construct the needed AVPs. o HK-Mobile-Node-Answer (HMA) - The HK-Mobile-Node-Answer (HMA) indicated by the Command-Code field set to TBD and 'R' bit cleared in Command Flags field is sent by the AAAH in response to a HMR message. C.2 AVPs For backward compatibility, attributes defined for RADIUS can be reused within this new Diameter Application. C.3 Diameter Flow of Messages The AAA exchanges between AR and its home AAA server is basically the same as for RADIUS. However, the Diameter application will benefit from all of the advantages that Diameter provides. Narayanan, et al. Expires December 30, 2005 [Page 26] Internet-Draft Handover Keys Using AAA June 2005 MN AR AAAH Server | HKReq. | | | ---------> | | | | HMR | | | ----------------------> | | | HMA | | | <----------------------- | | HKResp. | | | <--------- | | Figure 6: Diameter Handover Key Messaging Appendix D. Alternate Approaches Several alternative approaches are available for AAA-assisted handover key derivation between the MN and the AR. In this section, brief details about these alternatives are provided. One alternate approach to preserve air interface bandwidth could be for the MN to send a single HKReq to AR1, including a list of ARs, requesting handover keys to be derived for each AR. AR1 may then forward the request to the appropriate ARs (via say, a Handover Key Notify (HKNot) message). The ARs should then send the AAA request for handover key generation as described in the previous section. Hence, the difference in this approach is that the MN, instead of individually sending a HKReq message to every neighboring AR, allows the AR to distribute the request to the other ARs. While this approach saves some bytes over the air, it adds complexity to the signaling. A second approach will be for AR1 to send the first HKReq from the MN to the AAA server along with a list of neighboring ARs. The AAA Server may derive handover keys for each AR in the list and send all the HKs back in a AAA message to AR1. AR1 will then use the HKNot message to transfer the key to the corresponding AR. This approach adds some complexity as follows: o In order to satisfy the criteria described in AAAKEY [9], the compromise of one AR must not lead to the compromise of any other AR. Hence, this means that each HK must be encrypted with the corresponding AR-AAA SA. In the presence of a AAAL, each AR will only share an SA with the AAAL. Hence, this will require the AAAL to receive the keys via its SA with the AAAH and then individually encrypt each attribute separately with the correct AR SA. This deviates from the model of having the AAAL as simply a proxy. Narayanan, et al. Expires December 30, 2005 [Page 27] Internet-Draft Handover Keys Using AAA June 2005 o It may be possible if the AAA protocol allows unsolicited messages to the AAA client - in that case, the AAA server may derive a set of HKs and send each one separately to the corresponding AR directly. However, this is not feasible, since RADIUS is strictly a request-response style protocol. o There are obvious vulnerabilities in letting one AR see the keys of the other ARs in the clear - hence, this option must not be considered. It is also possible for the AR itself to generate keys for the MN to share with neighboring ARs - however, it suffers from some of the same disadvantages outlined above. A third approach is to use an approach similar to the one described in irtf-aaaarch-handoff - the AAA server in this case can derive HKs for multiple neighboring ARs and notify the ARs about the availability of this key. This, however, requires support for unsolicited AAA messaging, which is absent at the present time. Other approaches where the AAAL performs handover key derivation are also feasible. This requires the AAAL to be more than just a proxy and hence introduces complexity in the AAAL. Hence, given the shortcomings of these alternate approaches, the protocol is simplest and most efficient as described in section 5. Appendix E. Formal Analysis This section aims to provide a formal analysis of the MN-AAAH authentication protocol described in this document. We used the tool OFMC (On-the-Fly Model-Checker), from the AVISPA project [10] (Automated Validation of Internet Security Protocols and Applications), which uses a rich specification language for formalizing protocols, security goals, and threat models of industrial complexity. This HIPSL file is then translated into an Intermediate format using another tool named HLPSL2IF, which is a translator, which maps security protocol specifications into rewriting systems. This intermediate format can be executed to analyze the threats of the protocol. The verified protocol has the structure shown in Figure 7 and is a simplified version of the protocol discussed in this document. The analysis considers only two parties and some attributes are omitted. Narayanan, et al. Expires December 30, 2005 [Page 28] Internet-Draft Handover Keys Using AAA June 2005 [NAI, Sequence number N1]HMK ---------------------------> Handover Key Response (HKResp) [Sequence Number N2, nonce]HMK <--------------------------- Figure 7: Modeled Protocol [x]key respresents the keyed message digest computed over the field 'x'. HMK is the long-term key shared between the MN and the AAA server. Sequence numbers N1 and N2 are independent from each other and non-repeating numbers. The nonce value is primarily used for key derivation. This is the HLPSL format of the authentication protocol executed between the MN and the AAA server. A web-based tool is available at http://www.avispa-project.org/web-interface/ %%HLPSL: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% role mobile(M,S:agent, Snd, Rec: channel(dy), HMK: symmetric_key, NAI: text, Seq: text ) played_by M def= local State :nat, Seq1 :text, Nonce :text(fresh) const r1,r2 : protocol_id, add : function init State := 1 transition 1. State = 1 /\ Rec(start) =|> State'= 2 /\ Snd({NAI.Seq}_HMK) 2. State = 2 /\ Rec({seq1.Nonce'}_HMK) =|> Narayanan, et al. Expires December 30, 2005 [Page 29] Internet-Draft Handover Keys Using AAA June 2005 State'= 3 /\ Seq1' := add(Seq1,1) % /\ Secret(Nonce',S) end role %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% role server(S,M : agent, Snd, Rec: channel(dy), HMK: symmetric_key, Seq1 : text ) played_by S def= local State : nat, NAI : text, Nonce :text(fresh), Seq :text const r1,r2 : protocol_id, add : function init State := 1 transition 1. State = 1 /\ Rec({NAI.Seq}_HMK) =|> State' := 2 /\ Snd({seq1.Nonce'}_HMK) /\ Seq' := add(Seq',1) %/\ secret(Nonce',M) end role %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% role session(M,S: agent, HMK: symmetric_key, Seq,Seq1: text, NAI:text, SA,RA,SB,RB: channel(dy)) def= composition mobile(M,S,SA,RA,HMK,NAI,Seq) Narayanan, et al. Expires December 30, 2005 [Page 30] Internet-Draft Handover Keys Using AAA June 2005 /\ server(S,M,SB,RB,HMK,Seq1) end role %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% role environment() def= local Sa1,Ra1,Ss1,Rs1 : channel (dy) const r1, r2 : protocol_id, a, i, s : agent, k_as, k_is, kai : symmetric_key, nai : text, seq_as, seq_is, seq_ai : text intruder_knowledge={a,s,i} composition session(a,s,k_as,seq_as,seq_ai,nai,Sa1,Ra1,Ss1,Rs1) end role %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% goal secrecy_of seq,seq1 %Mobile weakly authenticates Server on r1 % the nonce R authentication_on r1 %Server weakly authenticates Mobile on r2 % the nonce R authentication_on r2 end goal %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% environment() Our preliminary analysis did not show vulnerabilities. Narayanan, et al. Expires December 30, 2005 [Page 31] Internet-Draft Handover Keys Using AAA June 2005 Intellectual Property Statement The IETF takes no position regarding the validity or scope of any Intellectual Property Rights or other rights that might be claimed to pertain to the implementation or use of the technology described in this document or the extent to which any license under such rights might or might not be available; nor does it represent that it has made any independent effort to identify any such rights. Information on the procedures with respect to rights in RFC documents can be found in BCP 78 and BCP 79. Copies of IPR disclosures made to the IETF Secretariat and any assurances of licenses to be made available, or the result of an attempt made to obtain a general license or permission for the use of such proprietary rights by implementers or users of this specification can be obtained from the IETF on-line IPR repository at http://www.ietf.org/ipr. The IETF invites any interested party to bring to its attention any copyrights, patents or patent applications, or other proprietary rights that may cover technology that may be required to implement this standard. Please address the information to the IETF at ietf-ipr@ietf.org. Disclaimer of Validity This document and the information contained herein are provided on an "AS IS" basis and THE CONTRIBUTOR, THE ORGANIZATION HE/SHE REPRESENTS OR IS SPONSORED BY (IF ANY), THE INTERNET SOCIETY AND THE INTERNET ENGINEERING TASK FORCE DISCLAIM ALL WARRANTIES, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTY THAT THE USE OF THE INFORMATION HEREIN WILL NOT INFRINGE ANY RIGHTS OR ANY IMPLIED WARRANTIES OF MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE. Copyright Statement Copyright (C) The Internet Society (2005). This document is subject to the rights, licenses and restrictions contained in BCP 78, and except as set forth therein, the authors retain all their rights. Acknowledgment Funding for the RFC Editor function is currently provided by the Internet Society. Narayanan, et al. Expires December 30, 2005 [Page 32]