In this paper, we have described proposed IPSEC security mechanisms (AH/ESP) and their use to provide integrity, authentication, and confidentiality use in securing mobile computing. By formalizing definitions of integrity, authentication, and confidentiality, we have shown under what contexts these properties are and are not preserved based on what data is covered by a hash or encryption. In the context of Mobile-IP, we have developed a mechanization of the mobile registration protocol that uses an untrusted route to establish a secure tunnel.
Using the HOL90 system, these definitions have been mechanized and correctness proofs constructed using a belief logic. Future work will focus on automating the decision procedures and mechanise our paper-and-pencil analysis of secure tunnels for use with Mobile IP.