IP Security Protocol (IPSEC) Working Group of the Internet Engineering Task Force
(IETF) developed the Internet Key Exchange protocol (IKE) [1], a key exchange
protocol. The main purpose of its development is to provide the security support for
client protocols of the Internet Protocol. It is being designed to do much more than
just distribute keys, it can also be used to establish Security Associations that specify
such things as the protocol format used, the cryptographic and hashing algorithms
used, and other necessary features for secure communication. For incorporating flexibility,
it supports a number of different types of key exchange options, including
digital signatures, public key encryption, and conventional encryption using shared
keys. The Diffie-Hellman algorithm is used to generate shared key material.
The IKE protocol has evolved from ISAKMP [2] and Oakley [3]. It can be
thought of as combination of these two protocols. ISAKMP provides a framework for
establishing security associations and cryptographic keys, but does not prescribe any
particular authentication mechanism. Indeed, ISAKMP is supposed to integrate with a
number of security protocols. Oakley, on the other hand, is a suite of key agreement
protocols in which two parties generate a key jointly.
A typical key establishment protocol proceeds in one phase, in which two parties
use master keys to establish shared keying material. IKE, however, proceeds in two
such phases. In the first phase, two entities use master keys to agree, not only on
keying material, but on the various mechanisms (e.g. cryptographic algorithms, hash
functions, etc.), that they will use in the second phase. The keying material and set of
mechanisms thus agreed upon is called a security association. In the second phase, the
keys and mechanisms produced in the first phase are used to agree upon new keys
and mechanisms (that is, new security associations) that will be used to protect and
authenticate further communications. The security association established in Phase
One is bidirectional, so the initiator in the first phase can be either initiator or responder
in the second phase. Like Oakley, IKE can also be used in multiple modes,
aggressive mode and main mode.
The paper step by step analyzes the threat perception and measures taken to address
them, when we build IKE protocol from the scratch. We have used Murf tool,
to check the possibilities of attack on the strip down versions of IKE protocol in Public
signature, Pre-Shared secret and Public Encryption mode. For removing the threats
we added some more steps, which finally lead us to the original IKE protocols.
Now we need to have some understanding of the Formal methods, its importance
and also the difficulties in modeling the protocols. Formal verification of a protocol
proceeds by describing the protocol in some language and then comparing the behavior
of this description with a specification of the desired behavior. A verifier generates
states from the description, comparing them with the specification as it goes. If
the verifier detects an inconsistency, this fact is reported, along with an example sequence
of states that illustrates how the problem can occur, that aid in diagnosis.
The main challenges that arise while using finite state verification tool for analyzing
security-related protocols are:
- State-space explosion
- Subtleties involving formalization of the adversary and
- Subtleties involving the properties of the encryption primitives, which may
be modeled as completely secure black-box primitives, or primitives with
other algebraic properties.
Outline of the methodology
The Murf verification system
Murf is a protocol verification tool that has been successfully applied to several industrial
protocols, especially in the domains of multiprocessor cache coherence protocols
and multiprocessor memory models. Previously this tool has been successfully
used to model and verify SSL 3.0 [10], Needham-Schroeder public key protocol Kerberos
and the TMN cellular telephone protocol.
To use Murf for verification, one has to model the protocol in the Murf language
and augment this model with a specification of the desired properties [8]. The
Murf system automatically checks, by explicit state enumeration, if all reachable
states of the model satisfy the give specification. For the state enumeration, either
breadth-first or depth-first search can be selected.
The state of the model consists of the values of all global variables. In a startstate,
initial values are assigned to global variables. The transition from one state to
another is performed by rules. Each rule has a Boolean condition and an action,
which is a program segment that is executed atomically. The action may be executed
if the condition is true (i.e. the rule is enabled) and may change global variables.
The desired properties of a protocol can be specified in Murf by invariants,
which are Boolean conditions that have to be true in every reachable state. If a state is
reached in which some invariant is violate, Murf prints an error trace – a sequence of
states from the start state to the state exhibiting the problem.
The methodology
We have analyzed the protocols using the following sequence of steps:
- Formulate the protocol. This involves simplifying the protocol by identifying the
key steps and primitives. However, the Murf formulation of a protocol is more detailed
than the high level description found in the literature. The most significant
issue is to decide exactly which messages will be accepted by each participant in the
protocol.
- Add an adversary to the system. We generally assume that the adversary is a participant
in the system capable of initiating communication with an honest participant.
We also assume that the network is under the control of the adversary and allow the
adversary the following actions:
- Overhear every message, remember all parts of each message, and decrypt ciphertext
when it has the key.
- Intercept (delete) messages.
- Generate messages using any combination of initial knowledge about the system
and parts of overheard messages.
- State the desired correctness condition.
- Run the protocol for some specific choice of system size parameters.
- Experiment with alternate formulations and repeat.
Murf compiler and verifier
The Murf compiler takes a Murf source description and generates a C++ program,
which is compiled together with code for a verifier which checks for invariant violations,
error statements and deadlocks.
The intruder model
The intruder model has the following limitations.
- No cryptanalysis Here the intruder ignores both computational and numbertheoretic
properties of cryptographic functions. As a result it cannot perform any
cryptanalysis whatsoever.
- No probabilities Murf has no notion of probability. Therefore, we do not model
“propagation” of attack probabilities through the finite state system. We also ignore
that the intruder may learn some probabilistic information about the participants’ keys
by observing the multiple runs of the protocol.
- No partial information Keys, nonces, etc. are treated as atomic entities. Intruder
cannot break such data into separate bits. It cannot perform an attack that results in
the partial recovery of a secret.
Modeling IKE
In this paper we have modeled only the main mode protocols. In main mode there are
six messages. In the first pair of messages, “A” sends a cookie and requested cryptographic
algorithms, and “B” responds with his cookie and the cryptographic algorithms
he will agree to. Messages 3 and 4 are a Diffie-Hellman exchange. Messages 5
and 6 are encrypted with the Diffie-Hellman value agreed upon in messages 3 and 4.
In messages 5 and 6, each side reveals its identity and proves it knows the relevant
secret.
In general it is assumed that encryption is opaque, however intruder can store the
encrypted messages for replaying them later. Signatures are taken to be unforgeable
and there exists a Certification Authority which is trusted by both the communicators.
Another thing to note here is that we have not modeled the first phase, which includes
mutual agreement on the protocols and algorithms
Notation
*( ..) denotes the comments
* p,g are publicly known
* a,b are secret random values chosen by A and B resp.
Public signature key main mode:
Protocol A
To begin with, we start be the most basic 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 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.
Protocol B
To prevent the man in the middle attack, we have now added two more steps to the
existing protocol A. Here both A and B after exchanging the Diffie-Hellman Values
also exchange encrypted signed messages containing all the previous messages sent.
Now without knowing the value K, intruder cannot generate correct messages for
steps 5 and 6. Thus preventing man in the middle attack.
1. A -> B : Crypto offered
2. B -> A : Crypto selected
3. A -> B : ga mod p , A
4. B -> A : gb mod p , B
5. A -> B : K{sign on previous messages by A, A}
6. B -> A : K {sign on previous messages by B, B }
K=gab mod p is the session key
Attack on B
Replay attack is possible on protocol B but here the man in the middle attack is prevented.
Man in the middle attack is prevented as the intruder cannot sign messages.
When the initiator or responder signs all the previous messages the intruder cannot
modify it and the two parties come to know about the Man in the Middle attack by
comparing the message they received previously and the messages signed. Replay
attack is now possible as the intruder can save the messages and can replay them
later. There is no nonce hence replay attack is successful.
Protocol C
To prevent the replay attack, one can add an ephemeral value (nonce) to one of the
messages so that the encrypted signed messages would change each time. So replay
attack would not be possible.
1. A -> B : Crypto offered
2. B -> A : Crypto selected
3. A -> B : ga mod p , A
4. B -> A : gb mod p , B , nonce(B)
5. A -> B : K{sign of previous messages by A , A}
6. B -> A : K{sign of previous messages by B, B}
K=f(gab mod p, nonce(B)) is the session key
Attack on C
Here the replay attack is prevented due to the nonce sent by B. But murf pointed out
that the intruder can still impersonate B through replay attack as there is no nonce
sent by A.
Protocol D (final)
To prevent the attack found in the previous protocol, we have added one more
ephemeral quantity. This time A would generate it. Now intruder can not replay any
previous messages since both A and B would issue different nonce when initiating a
fresh communication.
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{sign of previous messages by A , A}
6. B -> A : K{sign of previous messages by B, B}
K=f(gab mod p, nonce(B), nonce(A)) is the session key
Attack on D
Here A sends a nonce to prevent the replay attack on the previous protocol C. Till
now there is no attack found on protocol D.
E-Mail Link
Your IP address will be sent with this e-mail
