The IP security protocols (IPsec) may be used via security gateways that apply cryptographic operations to provide security services to datagrams, and this mode of use is supported by an increasing number of commercial products.
Authentication and Confidentiality via Ipsec
Download Resources
PDF Accessibility
One or more of the PDF files on this page fall under E202.2 Legacy Exceptions and may not be completely accessible. You may request an accessible version of a PDF using the form on the Contact Us page.
The IP security protocols (IPsec) may be used via security gateways that apply cryptographic operations to provide security services to datagrams, and this mode of use is supported by an increasing number of commercial products. In this paper, we formalize the types of authentication and confidentiality goal that IPsec is capable of achieving, and we provide criteria that entail that a network with particular IPsec processing achieves its security goals. This requires us to formalize the structure of networks using IPsec, and the state of packets relevant to IPsec processing. We can then prove confidentiality goals as invariants of the formalized systems. Authentication goals are formalized in the manner of [9], and a simple proof method using "unwinding sets" is introduced. We end the paper by explaining the network threats that are prevented by correct IPsec processing.