A primary use of a cryptographic hash function is to provide
an integrity check over data.
Informally, if A and B share a secret key, K , for use with a
cryptographic hash function, H , then if A creates a message xyz
where 
, on receipt of xyz , B can verify the integrity
of x and z combined by computing . If either of
these where
changed then, assuming a cryptographically strong keyed hash function,
B will detect the change. Using the abstract IP packet described above,
the integrity of the hash-data, hash-value, IP source address and SPI
can be verified as a unit. Since the source IP address and SPI are
used to index the security association information and
determine what key is used with the hash function, then
if any of these fields were modified, it follows that
the computation of the hash-value will be incorrect.
This notion is mechanized HOL using two auxiliary definitions that
validate the datagram AH hash with respect to a security association table
and that the relevant field is covered by the hash.
aPrincipal RECEIVED datagram datagram HASH_OK security_association_table message_field INDEXED_BY (hash-list datagram) --------------------------------------------- INTEGRITY message_field security_association_table aPrincipal