next up previous
Next: Authentication Up: Formalizing Security Services Previous: Formalizing Security Services


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 $H_K(x)=z$, on receipt of xyz , B can verify the integrity of x and z combined by computing $H_K(x)=z$. 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