Finite State Analysis of IKE

{LANG_NAVORIGIN} Encryption
Udayan Kumar, Y.Narendra, and Rakesh Upadhyay 05/31/2005

IKE using public encryption key (main mode)

Protocol A
Basic step for both Public signature and encryption mode can be the same, since in starting protocol neither signatures nor public encryption are used. We start with Diffie-Hellman Key exchange. This step requires the communicators to send over just the Diffie-Hellman values with the identity of the sender.

1. A -> B : Crypto offered
2. B -> A : Crypto selected
3. A -> B : ga mod p , A
4. B -> A : gb mod p , B
K=gab mod p is the session key

Attack on A
There can be a man in the middle attack possible on protocol A. The intruder just changes the Diffie-Hellman exponent but the source of the message remains the same. The responder reacts to this exponent by sending own Diffie-Hellman exponent. The intruder intercepts this message and again replaces the Diffie-Hellman exponent of responder by its exponent. Hence the intruder generates two different session keys with initiator and responder where initiator and responder think that the key they hold is with the intended party.

Unknown Key Share attack is also possible as the intruder just modifies the source field of the message. The responder thinks the session key is shared between him and the intruder. The intruder replays the unmodified message sent by the responder to the initiator so that the initiator thinks it shares the session key with the responder. Now when an encrypted message comes from the initiator the responder thinks it came from the intruder.

Protocol B
To prevent man in the middle attack, we have a different strategy than what we used in Public signature mode. Here both the parties send an ephemeral value (nonce) encrypted by other party’s public key. This alone does not solve the problem. Intruder can also generate encrypted nonce. Therefore the session key is made in combination with the nonce send by the initiator. Now intruder make successfully complete the protocol but will not be able to communicate successfully.

1. A -> B : Crypto offered
2. B -> A : Crypto selected
3. A -> B : ga mod p , { A }B, {nonce(A) }B
4. B -> A : gb mod p , { B }A , { nonce(B) }A
K=f(gab mod p, nonce(A)) is the session key

Attack on B
Here the man in the middle attack is prevented because of the nonce used to generate the key. But replay attack and Unknown Key Share attack both are possible on the above protocol B. Intruder may save all the communication happening between the legitimate parties. And later replay them imposing himself has the initiating party. Even in an on going communication, intruder can capture all the messages send by one party and forward them to the other party, making it believe that intruder has send the messages.

Protocol C (final)
In the previous protocol, both replay and Unknown Key share attack were working since only one of the nonces was used to generate the session key and after transfer of Diffie-Hellman values no proof was asked whether the parties were still the same with whom communication was started. In an attempt to remove replay attack now nonces of both the parties would be used to generate the key. And for removing Unknown Key share attack, two more steps have been added to the protocol. These steps are used to prove that communication is going on between the parties which started it.

1. A -> B : Crypto offered
2. B -> A : Crypto selected
3. A -> B : ga mod p , { A }B, { nonce(A) }B
4. B -> A : gb mod p , { B }A, { nonce(B) }A
5. A -> B : K{proof I’m A}
6. B -> A : K{proof I’m B}
K=f(gab mod p, nonce(A), nonce(B)) is the session key

Attack on C
Replay attack is not possible here due to the 5th and 6th messages. UKS is also not possible as the intruder can not generate any of the proofs. We could not find any other attack possible on this protocol, using Murf. Moreover this protocol C is similar to the corresponding mode in IKE.

Pre-shared Key Main Mode

* A and B have a pre-shared secret J in protocols to follow

Protocol A
A and B share a common secret J. So they can communicate with J as their session key.

Attack on A
The intruder would be able to decrypt the previous conversations if he gets the preshared secret. Hence this protocol doesn’t guarantee perfect forward secrecy.

Protocol B
Perfect Forward Secrecy can be obtained if we use different session keys on session. That means we need to create some other value using session key, which could be used as session key. For this purpose we can again use Diffie-Hellman key exchange protocol. And use the key thus obtained in combination with Shared secret to create a session key. Now the session key would be different for each key. Thus Perfect Forward Secrecy is achieved.

1. A -> B : Crypto offered
2. B -> A : Crypto selected
3. A -> B : ga mod p , A
4. B -> A : gb mod p , B
K=f(gab mod p, J) is the session key

Attack on B
Replay attack is possible on the above protocol B. Unknown Key Share attack is not possible due to the secret J that only the initiator and responder know. Hence the key generated will be different as responder will use the shared secret with the intruder whereas the initiator will use the shared secret with the responder hence two different keys.

Protocol C
We can use an ephemeral value (nonce) in conjunction with the existing protocol to prevent the replay attack.

1. A -> B : Crypto offered
2. B -> A : Crypto selected
3. A -> B : ga mod p , A , nonce(A)
4. B -> A : gb mod p , B, nonce(B)
K=f (gab mod p, J, nonce (A)) is the session key

Attack on C
Replay attack is still not prevented in the above protocol C. As we have used nonce only form one party. Unknown Key Share attack is also possible.

Protocol D (final)
To prevent both Replay and Unknown Key share attack. We added two more steps and one more nonce in the generation of session key. This addition leads us to the final protocol.

1. A -> B : Crypto offered
2. B -> A : Crypto selected
3. A -> B : ga mod p , A , nonce(A)
4. B -> A : gb mod p , B , nonce(B)
5. A -> B : K{proof I’m A,”A”}
6. B -> A : K{proof I’m B,”B”}
K=f(gab mod p, J, nonce (A), nonce (B)) is the session key

Attack on D
Our Murf modeling did not found any other kind of attack possible.

Public Encryption Key, main mode, revised Protocol and encryption of Diffie- hellman values

This protocol functionally is similar to the final protocol reached in Public Encryption Key method, but it is more economic in the sense of computation. This protocol avoids heavy public key encryptions and private key decryption being needed in step 3 and 4 of the original. For this saving it requires generation of secret key using the nonces and all further encryption is done using that secret key.

1. A -> B : Crypto offered
2. B -> A : Crypto selected
3. A -> B : KA{ga mod p} , KA{“A”} , KA{nonce(A)}, KA{Alice’s cert}
4. B -> A : KB {gb mod p} , KB {“B”} , KB {nonce(B)}
5. A -> B : K{proof I’m A}
6. B -> A : K{proof I’m B}
KA= hash(nonce(A), cookie(A))
KB= hash(nonce(B), cookie(B))
K = f(gab mod p, nonce (A), nonce (B), cookie(A), cookie(B))
cookie(A) and cookie(B) are exchanged in step 1 and 2 respectively

When we modeled this revised version, we made a small but significant change while modeling it. We ignored the encryption KA{ga mod p} and KB {gb mod p}, still we found that it was not susceptible to any attack. Now we again modeled it, exactly as it is. Comparing both we found that there is absolutely no difference in both the models considering the security aspect. On the basis of this result we claim that this secret key encryption can be dispensed with, without affecting the security. This reduction would further lower down the computational requirements of the protocol.

Conclusions

Our study of IKE using formal methods is not a new technique; it has already been done by the using NRL [9], though here we have done it using Murf. However we have tried to bring out the need of the various steps of IKE. This technique of adding more functionality or steps when faced by certain attacks can be used to improve and build protocols.

Here we would like to re-iterate our analysis which points towards the unnecessary encryption of Diffie-Hellman values in the revised Main mode protocol of the Public Key Encryption.

References

1. Charlie Kaufman (edt.): Internet Key Exchange (IKEv2) Protocol. draft-ietfipsec- ikev2-17.txt
2. D. Maughan, M. Schertler, M. Schneider, and J. Turner: Internet security association and key management protocol (ISAKMP), version 1 draft-ietfipsec- isakmp-10.txt (1998).
3. H. Orman: The Oakley key determination protocol, version 2. draft-ietfipsec- oakley-02.txt (1996).
4. D. L. Dill and A. J. Drexler and A. J. Hu and C. H. Yang: Protocol verification as a hardware design aid
5. D. L. Dill: The Murf verifcation system. In Computer Aided Verifcation. 8th Interntional Conference, pages 390-3 (1996)
6. Charlie Kaufman, Radia Perlman, Mike Speciner: Network Security. Pearson Education . (2004) pages 441-460
7. John C. Mitchell Mark Mitchell Ulrich Stern: Automated analysis of cryptographic protocols using Murf
8. User Manual, tutorial and other examples provided with the free distribution of Murf.
9. Catherine Meadows: Analysis of the Internet Key Exchange Protocol Using the NRL Protocol Analyzer, IEEE, (1999)
10. John C Mitchell, Vitaly Shmatikov, Ulrich Stern: Finite state analysis of SSL 3.0, 7th USENIX Security Symposium, pages 201-15, (1998)
11. Vitaly Shmatikov and U. Stern: Efficient Finite-State Analysis for Large Security Protocols. 11th IEEE Computer Security Foundations Workshop, pages 106-15, (1998)

Your IP address will be sent with this e-mail

From e-mail to e-mail