Formal Analysis of IP Layer Security

Sarah Mocas and Tom Schubert
{sarah,schubert}@cs.pdx.edu
Department of Computer Science
Portland State University

Abstract:

The use of formal methods during the development of a security protocol permits the designer to identify subtle assumptions that can lead to security flaws. Automated support for using formal methods can greatly assist this process, however, for many applications, correct formal modeling of a protocol and identification of its underlying assumptions is initially of greater importance than automated proofs. With this in mind, we model several different security mechanisms and protocols that are currently being developed for use at the IP network layer. Specifically we model the proposed IPSEC security extensions, AH and ESP, to determine the soundness of these propositions. In the context of Mobile-IP, we investigate the use of formal logics to examine IP layer security mechanisms but especially mobile node registration.