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.