An area of current interest is the addition of security to transactions over the network layer of the Internet. Inserting security mechanisms is possible at several different points, all the way from the application level to the hardware level. A natural location is at the IP level of the protocol stack. This particular idea is receiving much attention and several mechanisms for achieving this result have been proposed for possible standardization [2,5,6,7]. There is also a natural combination of IP layer security mechanisms and mobile networking to create secure mobile networks (secure Mobile-IP). In this case, mobility within a network refers to the ability of a network entity, a mobile node, to send and receive datagrams using an IP address that is not recognized as local by the subnet in which the node is connected. This requires that there are additional entities that act as agents on behalf of a mobile node. In this context, a mobile node's IP address is used to indicate the identity of the node with respect to a home network (where its IP address is local). Datagrams destined for the mobile node continue to be sent to the mobile node's home network and are then forwarded on to the mobile node's actual (registered) location. Both the application of security mechanisms to the Internet and the development of mobile networks are evolving areas.
We have modeled several of the proposed IPSEC security extensions to determine the soundness of these propositions. Specifically, we examine the services that should be provided by the addition to an IP packet of the authentication header, AH, and the privacy header, ESP (encapsulation security payload). Through formal methods, we show where protocols using ``secure packets'' succeed in providing the service for which they are intended and where they fall short.
In the context of Mobile-IP, we are investigating the use of belief logics to examine IP layer security mechanisms. There are several security mechanisms needed for a reasonable implementation of a secure mobile network. Initially, mobile registration requires the use of an untrusted route to establish a secure tunnel. We model the registration services that are provided via a routing daemon using a UDP port.
Several logics for analyzing cryptographic protocols and authentication schemes have been proposed (see for example [1,3,4,13,14]). Belief logics are designed to consider what conclusions individual parties (principals) in a communication dialogue can deduce based on messages received and a set of initial assumptions or beliefs. Belief analysis attempts to show that only desired properties are guaranteed by the communication (data confidentiality, message authorship, non-repudiation, no replayed transactions, etc). Note that proofs about idealized protocols are not a guarantee that the concrete protocols are correct. There are many implementation assumptions that if invalid, would cause a secure, idealized protocol to actually be insecure. For example, these logics all assume that the cryptoalgorithm is secure.
Our logic for IP layer security mechanisms closely follows the logic used for analyzing protocols that was developed by Syverson and vanOorschot [13]. Syverson and vanOorschot's logic was chosen as it encompasses many of the desirable features from earlier developed logics in an integrated approach. Using our mechanization of SVO, we formally demonstrate the danger of preserving backward compatibility of the ESP header.