Keywords: IPSec, Security Associations, Security Policies, Formal Specification
Suppose a wireless client needs to securely communicate with a server. Existing wireless security mechanisms often look something like this. A layer 2 protocol such as WEP provides some degree of security between the client and the NAS. End-to-end security between the client and the server is provided at the application layer by SSL. Although this may seem adequate, there are several problems. First, all of the layer 2 security mechanisms have known vulnerabilities. Secondly, SSL is vulnerable to DOS attacks. Instead of combineing security mechanisms from different layers we decided to receive all our protection at layer 3 from IPSec.We call the protocol that sets up the IPSec security associations the Layer 3 Accounting Protocol (L3A).
Let us consider the following configuration. A wireless client that needs to securely communicate with a server. The client gains access to the Internet via a Network Access Server (NAS) that belongs to a vendor that charges the client based on the volume of data going over the link. We can assume that the client must authenticate itself to both the NAS and the server. Our protocol sets up a collection of IPSec security associations (SA) and polices that provide the necessary protections.
The first question we ask in designing such a protocol is what security associations are needed to protect the user. An SA is clearly needed between the client and the server. This SA should provide both encryption and authentication protection. Although this protection may seem sufficient at first glance, recall that the client needs to authenticate to both the NAS and the server. This indicates the need for an SA that authenticates the client to the NAS. So it seems that protocol should first set up an SA from the client to the NAS and then set up an SA between the client and the server. Note the SA between the client and server tunnels through the SA from the client to the NAS. Unfortunately, this configuration still leaves the user exposed to an attack since an attacker may be able to push bogus traffic back through the NAS resulting in charges for services that the user never requested. This indicates the need for a second authentication tunnel from the server to the NAS to authenticate incoming traffic. When the authentication SA from the client is established, the client presents a credential to the NAS for authentication purposes. The NAS will need to present a credential to the server on behalf of the client as part of establishing the SA from the server to the NAS.
Our efforts have been guided by the philosophy that all traffic should travel in DOS resistant SAs and that the protocols that establish these SAs should be DOS resistant.
A brief reminder of some facts about IPSec. IPSec is a Security Architecture for the Internet Protocol specified in RFC 2401 ipsec-rfc that provides authentication and encryption for IP packets. Loosely speaking, IPSec is implemented between network and transport layers of the protocol stack, but the detailed interaction with the IP stack is slightly more complex. The operation of IPSec critically depends on the existence and maintenance of security associations, that is virtual secure channels, and policies, governing the use of these channels. IPSec does not provide a mechanism to set up these entities, but instead relies on external protocols like IKE, IKEv2, or JFK. The existing implementations IKE and JFK did not totally support our needs and introduce complexities orthogonal to our project's goals. In particular, implementations of IKE and JFK don't support nested tunnels. Thus we implemented a simple key exchange protocol for L3A that supports nesting of tunnels.
In the context of the CONTESSA project we have developed an executable formal specification of the L3A protocol and performed some preliminary analysis. This analysis revealed several problems with our design. The design was modified and the process repeated. We shall present four iterations of this design where the final version gives us a correct solution.
Relevant References:
The files of all versions of the formal specification in Maude 2.0 (
available
here) can be found
here.
Many of the files provide the necessary infrastructure to perform
tasks such as public key cryptography, model addresses, message
formats, model security policies and security associations. For the
first version of the protocol we provide a list of files critical to
understanding the model. We shall only list those files that change
when presenting the revised versions.
Before continuing with our description of the first version of the L3A
protocol we we shall give a brief description of the key exchange
protocol, Simplified Internet Key Exchange (SIKE), associated with
this system. The key exchange establishes a single SA. This SA does
not necessarily flow from the initiator to the responder. As a
consequence the initiator must provide the direction as a parameter
when invoking the protocol. The protocol also allows information to be
sent from the initiator to the responder via a payload field. In
practice, the payload field is used by an L3A client to pass to the
NAS the server address and the credential that the NAS must present to
the server. The following diagram shows the exchanges involved in the
protocol.
The initiator A generates a nonce and a SPI for a B->A tunnel. Upon receiving msg1, the responder B generates a nonce and a SPI for a A->B tunnel. The responder also forms a cookie. The responder forms msg 2 and sends it to the initiator. The initiator A forms the third message that includes B's IP address, A's certificate, the direction of the SA that is being established, payload, and signature among other items. The responder then generates the shared key K and sends it back in msg4 along with some other information. Note that there is only one update to the SADB and SPDB at each node since only one SA gets set up by this key exchange.
Existing implementations of IKE, IKEV2, and JFK do not support nested tunnels. There are many issues as to why this is the case, but the reason of most concern to us is the complexity of possible configurations makes it difficult to know what to do when creating an SA that may or may not tunnel through an existing SA. L3A has a rather simple configuration. As a consequence we designed SIKE to support the following nesting strategy. Whenever an SA is being created from A-->C and there is an existing SA A-->B we just tunnel through. Due to the configuration of SAs in L3A we don't have to worry about improper nesting of SAs. This solution works fine for this protocol. It would be possible to check for improper nesting if necessary. This policy adapted here would not work cases where you may not want such nesting to always occur. The more general case may require a great deal more complexity.
We now turn our attention to the L3A protocol itself. In the first
action of the protocol, the client invokes SIKE to establish an SA
from the client to the NAS. The payload field contains the address of
the server as well a credential that the NAS must present to the
server on behalf of the client. NAS then invokes the SIKE exchange to
establish an SA from the server to the NAS. Note that the direction
field indicates that the resulting SA flows from the server to the
NAS. The credential contained in the payload field of the previous
SIKE exchange is then passed along to the server in the payload field
of this SIKE exchange. The server then invokes SIKE to establish
the SA from the server to the client. Once the client has set up this
SA, it invokes SIKE to establish the SA from the client to the server.
The protocol is illustrated in the following figure:
The relevant files are listed below.
Looking at the results of running a search of all possible executions analysis: we see that there are three solutions.
We were somewhat perplexed over the first error so we decided to address it first. Analysis reveled that our model of IP and IPSec was too weak. The actual semantics for a send message is that the send function doesn't return until the message is out on the wire. We checked the code! The model of IP and IPSec used in version 1A didn't behave this way. This weaker model allowed the caller of the send message to continue precessing as soon as the send call was made while the message was processed concurrently. The key exchange sends message 4 and then updates the security policy database to create the SA from the responder to the initiator. Due to the concurrency mentioned above, there are cases where the SAs are set up on the responder before message 4 is actually out the door.
The relevant files are listed below.
Looking at the results of running a search of all possible executions analysis: we see that there are now four solutions. It seems that things may be getting worse now that we have a correct model of IP and IPSec, but closer inspection shows that things may be improving.
As a result our analysis of version 1B we decided to make a small
modification to see if the problems could be resolved. In version 2a
we seek to eliminate the problem of packets going into the partially
set up tunnel from S to the NAS by having the NAS send an
acknowledgment to S after it is finished the S-->NAS set up. The
new protocol is illustrated by the following figure:
The new files are listed below.
Looking at the results of running a search of all possible executions analysis: we see that there is now one solution. Although it may seem like we have solved all our prpblems, the ACK from the NAS to the server is not traveling in an SA. It became clear that maintenance traffic flowing from the NAS to the client needed to be in an authentication tunnel. Similarly for maintenance traffic flowing from the NAS to the server. This means that the key exchange needed to be reworked to establish SAs in both directions. Note that IKE and JFK establish SAs in both directions. Our analysis uncovered the need for more acknowledgments. Before describing this revision of the protocol we shall give a brief description of the new version of SIKE.
The revised version of the key exchange protocol is given the the
following figure:
There are only minimal changes to the messages. The direction field is no longer needed since SIKE establishes bi-directional tunnels. The payload field has also been dropped in favor of sending this information in acknowledgment messages. The point of interest in this protocol is where the SADBs and SPDBs get written. The responder writes the information to establish the A-->B SA before sending msg4. Upon receipt of msg4, the initiator can be assured that the responder has set up the A-->B tunnel. The responder must wait until after msg4 is sent to write the information for the B-->A SA. Otherwise, msg4 would have the SA applied to it before the recipient of that message is able to set up the SA on its end. The initiator postpones all writing to the DBs until after msg4 is received. Upon termination of SIKE, the initiator knows that both sides have established the A-->B SA. The responder only know it has set up the SAs on its side and knows nothing about the state of the SAs at the initiator.
Version 2A of the L3A protocol is illustrated in the following figure:
The client begins the protocol by initiating a SIKE exchange to establish the C<-->NAS authentication SAs. The client then sends an Init message to the NAS containing the address of the server as well as the credential that the NAS must present to the server. This message informs that NAS that the client has set up the C<--> NAS SAs on its end. Upon receiving the Init message, the NAS begins a key exchange with the server to establish the NAS<-->S authentication SAs. The NAS then sends an Ack message containing the credential. The Ack message also lets the server know that the NAS<-->S SAs are set up on the NAS. Upon receipt of the Init message, the server checks the credential in order to authenticate the client. If this succeeds, the server begins a key exchange with the client to establish the C<-->S SAs. Finally, the server sends a FIN message to the client indicating that it has set up both C<-->S on its end.
The relevant files are listed below.