|
Authentication and Confidentiality via IPsec
May 2000
Joshua D. Guttman, The MITRE Corporation
Amy L. Herzog, The MITRE Corporation
F. Javier Thayer, The MITRE Corporation
ABSTRACT
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.
Additional Search Keywords
N/A
|
