CS259 - Project Report Faisal Memon (fmemon) Erik Weathers (erikdw) MOBIKE - IKEv2 Mobility and Multihoming Protocol MOBIKE allows the IKE endpoints to change IP addresses while retaining the existing IKE and IPSec SAs, no reauthentication or rekey is required. The primary usage scenario is mobility, not multihoming, so that is what we have analyzed. I. Protocol Summary The IKEv2 initial exchange is completely unchanged by MOBIKE. However, during the subsequent authentication exchange, each side must declare support for MOBIKE by including a MOBIKE notification in the payload. Initiator Responder ----------- ----------- 1) (IP_I1:500 -> IP_R1:500) HDR, SAi1, KEi, Ni, N(NAT_DETECTION_SOURCE_IP), N(NAT_DETECTION_DESTINATION_IP) --> <-- (IP_R1:500 -> IP_I1:500) HDR, SAr1, KEr, Nr, N(NAT_DETECTION_SOURCE_IP), N(NAT_DETECTION_DESTINATION_IP) 2) (IP_I1:4500 -> IP_R1:4500) HDR, SK { IDi, CERT, AUTH, CP(CFG_REQUEST), SAi2, TSi, TSr, N(MOBIKE_SUPPORTED) } --> <-- (IP_R1:4500 -> IP_I1:4500) HDR, SK { IDr, CERT, AUTH, CP(CFG_REPLY), SAr2, TSi, TSr, N(MOBIKE_SUPPORTED) } The IKE_SA_INIT exchange is represented in 1). It exchanges the Diffie-Hellman values (KE[ir]) used for encryption and integrity checking of all future exchanges on this IKE SA. IKE_SA_INIT includes cryptographically essential fields such as the nonces (N[ir]) and a message ID (inside the HDR). These two fields are needed to prevent replay attacks. The nat detection notifications include the original outer IP addresses of the packet so that each side can detect any NATs on the path and enable NAT traversal if desired. NAT traversal encapsulates the ESP packets inside UDP packets to allow them to be multiplexed by the NAT device. The SA[ir]1 is not relevant to our analysis. The IKE_SA_AUTH exchange is represented in 2). Each side is authenticated by inclusion of an identification payload (ID[ir]), authentication payload (AUTH), and optionally a certificate. AUTH contains the entire first message transmitted by this participant, to prevent a man-in-the-middle attack (MITM). It also contains the ID', which is essentially the ID payload minus the header, to certify our identity, and it includes the nonce from the peer, to prevent replay attacks. Then the combined values are HMACed using either a predefined shared secret, or the sender's private key if using certificates. Other fields such as SA[ir]2, TS[ir], and CP(CFG_REQUEST) are not relevant to this treatment of the protocol and as such will be ignored. (Initiator gets information from lower layers that its attachment point and address have changed.) 3) (IP_I2:4500 -> IP_R1:4500) HDR, SK { N(UPDATE_SA_ADDRESSES), N(NAT_DETECTION_SOURCE_IP), N(NAT_DETECTION_DESTINATION_IP) } --> <-- (IP_R1:4500 -> IP_I2:4500) HDR, SK { N(NAT_DETECTION_SOURCE_IP), N(NAT_DETECTION_DESTINATION_IP) } (Responder verifies that the initiator has given it a correct IP address.) 4) <-- (IP_R1:4500 -> IP_I2:4500) HDR, SK { N(COOKIE2) } (IP_I2:4500 -> IP_R1:4500) HDR, SK { N(COOKIE2) } --> The purpose of 3) is to perform the address change. It is an IKE notification across the IKE SA that tells the peer we are changing addresses to the IP in the outer IP header. If NATs have been explicitly disallowed then each side will include the original source and destination IP addresses in the payload in a NO_NATS_ALLOWED notification. This completely obviates any MOBIKE specific attacks and reduces the attacker to the same set of attacks he can use against general IKEv2. However, if NATs are allowed, as will typically be the case for MOBIKE, then an attacker is granted more power to negatively affect the state of each peer. More on this later. The final exchange we discuss is the optional return routability exchange, initiated by the responder after receipt of an address change request. The responder issues this return routability request to verify that the sender of the address change is at a routable address, and is a valid participant in this exchange. The responder includes a randomly chosen cookie value which must be echoed back by the address change initiator. The responder can delay updating of the SA database to the newly declared address until this return routablity exchange completes. The responder can also choose to periodically issue return routability requests throughout the lifetime of the IKE SA. II. Protocol Modeling with Murphi Eight step protocol is modeled in murphi by transitioning initiators and responders thru 8 states. Each participant is referred to by an AgentID, which is a union of 4 different entity types: initiators, initiator-primes (post address change agent), responders, and intruders. A session database is maintained on each virtual peer that allows the actual agent to be separated from the session state. This session database is indexed by the SPI ID (security parameter index), much like the SA database in a standard IKE implementation. We in fact call the session the "SPI". It includes many items that need to be known throughout the session, including for each peer the KEs, SPIs, nonces, message IDs, and the cookie. It also includes a randomly generated exponent for the DH exchange, the final IKE SA session key, and a variable indicating the current state of this peer. Diffie-Hellman -------------- The Diffie-Hellman is implemented as closely as we dared to reality, with each side choosing a random exponent, raising a generator to that exponent, and taking the modulus with a large prime. We couldn't use a standard DH group since the prime number is so enormous, so instead we chose a small prime of 7919. The generator is 2, as are all of the DH groups' generators. Messages -------- The IKEv2 message is implemented as an amalgam of all possible messages, with an entry for each possible message field, only some of which will be populated for any given message. Invariants and Correctness Checks --------------------------------- We created three invariants to test the protocol: a) if the initiator-prime is connected to a responder, then that responder had better be connected to this initiator and not some other agent. b) reached protocol completed state in both initiator and responder. c) verify that the session keys match. We implemented a 1 message wide window, so we only accept messages if the msgid is the next ID value expected from this peer. The AUTH payload is checked to ensure no MITM attack has occured with the first two messages. If NATs are disallowed (a globally configurable flag) then we verify that the source and destination values stored in the protected payload match the source and destination values of the packet. The responder checks that the cookie sent in the return routability exchange is returned unmodified. Intruder -------- Runs at a higher priority than other agents, and so is able to steal all packets off of the network prior to their arrival at their intended destination. Then forges the source and destination parameters sending to all possible agents from all possible agents. To avoid the intruder circularly sending and receiving its own packets we introduced a flag to indicate whether the packet was from the Rintruder or not. III. Attacks Standard Attacks (MITM, general replay) --------------------------------------- Standard attacks such as man in the middle and replay are thwarted by the AUTH payload of the third and fourth messages, mentioned in the first section. A typical man in the middle attack would involve the attacker replacing the Diffie-Hellman values in each of the first two messages with his own, seemingly stealing the session key, or so he thinks. Upon receiving the IKE_SA_AUTH message from the initiator, the responder will immediately be able to tell that something is amiss. Specifically the AUTH payload from the initiator is computed using the entire first message sent out by the initiator (along with other data as mentioned in section 1). When the responder calculates what he expects the AUTH payload to be based on the first message he received from the initiator, which was modified by the intruder, they will not match and the IKE negotitation will be stopped immediately. The same check is also done on the initiator side. Replay attacks are also prevented by the same AUTH payload. The AUTH payload from a host (initiator or responder) will contain the peer's nonce sent out as part of its IKE_SA_INIT message. So if an attacker decides to replay messages from a previous IKE negotiation, the AUTH payload will again give it away as the nonces used in this replayed session will differ from those used in the previous session. Address Change Attacks and Prevention ------------------------------------- MOBIKE retains all of the benefits of IKE when no nats are allowed. However a slight loosening of the requirements is necessary to support the common scenario of clients residing behind NAT devices. In this case the address to be changed to cannot be cryptographically protected since it is modified by the NAT device and the client cannot know a priori what the modified address will be. Since the third party NAT device cannot participate in the encrypted and authenticated exchanges there is no way to determine whether the device changing the outer IP is a friendly NAT device or a fiendish attacker. When NATs are allowed, as should be the standard case with MOBIKE, the address change exchange seems to be vulnerable to attack, since the responder changes its SAs based on the unprotected outer IP in the UPDATE_SA_ADDRESS notification message. At first blush without taking IKEv2's protections into account, the attacker seems to be able to execute a replay attack by recording a previous address change request from the initiator and then replaying that later with a different IP address. However, IKEv2 effectively prevents this attack by using the message ID in the protected IKE header, since a replayed packet would have the old message ID which should be outside of the responder's message window. So the attacker must intercept and modify the initial address change request message in order to mount any attack against MOBIKE. If the attacker intercepts and forges the outer IP he could cause the responder to update his SAs to the wrong IP address. MOBIKE attempts to combat this with the return routability exchange, which is a cookie sent from the responder to the source IP claimed in the address change request. The attacker cannot reply to this request himself, since he does not have the ability to properly craft the IKEv2 response message. That is, he doesn't have the session keys that would allow him to encrypt and MAC the IKE message, so although he can copy the cookie verbatim out of the return rouability request, he cannot increment the initiator's message ID. However, it is within the responder's power to forward this return routability request on behalf of the initiator, patching the IP addresses in order to carry out this attack. For instance the initiator tries to update the address from I1 to I2, and the attacker intercepts this message and replaces the source address with A, an address the attacker can receive packets on. Then the responder sends the return routability request to A, which the attacker forwards to I2 by patching the destination address to I2. So long as the attacker can intercept the outbound request from the responder, he can carry out this attack. The one advantage it has is to force the attacker to be able to respond to requests to the claimed source address A, preventing a pure spoofed address change request. So a DoS has been allowed by design in MOBIKE, by allowing this "relay attack" just mentioned above. There does not seem to be a way to overcome this without enlisting the NAT device into the protected exchange, which is not feasible given the usage scenario for NAT transparency; i.e., the IKE peers have no control over the NAT device. IV. Conclusions and Recommendations IKEv2 is a well designed security protocol, preventing common attacks such as MITM and replay attacks, while also retaining the flexibility to be used with preshared keys or certificates. The difficult to address DoS problem is also somewhat mitigated by an optional initial cookie exchange to prevent spoofing attacks from causing unnecessary and expensive exponentiations on the responder. MOBIKE, in the common scenario of traversing third party NATs, has a known DoS allowed by design that seems to be have no realistic solution. It is recommended that return routability always be enabled when NATs are allowed, and that no changeover of SAs occurs until after the return routability exchange has completed successfully. V. References Design of the MOBIKE Protocol http://www.ietf.org/internet-drafts/draft-ietf-mobike-design-08.txt IKEv2 Mobility and Multihoming Protocol (MOBIKE) http://www.ietf.org/internet-drafts/draft-ietf-mobike-protocol-08.txt Internet Key Exchange (IKEv2) Protocol http://www.ietf.org/rfc/rfc4306.txt?number=4306