Abstract. The IP security protocols (IPsec) may be used via security gateways that apply cryptographic operations to provide security servi- ces 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 achie- ving, 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. Authentica- tion 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.
