Formalizing Security Services

In our model, an IP packet is abstractly defined as a (type, hash-data, encrypted-data, data-list) tupple, where type is either NoProtection, ESP, or AH; data-list is a list of all of the fields in the IP packet; hash-data is a list of indices into data-list that indicate the data in the IP packet that is covered by a hash function; and encryption-data indicate the data in the IP packet that is covered by an encryption function. Note that the value of a hash (hash-value), which results from hashing the data referenced by hash-data, is usually contained in the data-list. Likewise, for mobile registration, UDP packets are abstracted in the same fashion where the type is Mobile. Whether or not the UDP packet payload is a registration request or reply is determined by information in the payload. The intention is to prove that certain security services are provided based on what data is covered by a hash or encryption.

A security association is abstractly modeled as a table where the entries are a principle, which is considered to be an address; a SPI; a type, which is either ESP, AH or Mobile; and a key-list, which is an ordered list of keys. In each case discussed, a packet will include a source IP address and SPI which can be used to index the security association table so that the correct secret key can be retrieved.