Next: The ESP Header Up: Formal Analysis of IP Previous: Confidentiality

The AH Header

The AH header consists of the following fields:

and is preceded by an IP header and followed by the data [5]. The Authentication Data field is the hash-value. In transport mode an AH packet is:

$IP Header \vert Next Header \vert Payload Len \vert Reserved \vert SPI \vert Seq No$
$\vert Authentication Data \vert Data$

In our abstract packet format this is:

$(AH, data\!-\!list, (IP Header, Next Header, Payload Len, Reserved, SPI,$
$Seq No, Authentication Data , Data), ())$
where data-list is the entire packet.

Since all fields in a packet using the AH header are included in the hash-data, it is easy to prove that integrity and authentication are provided over the entire packet. AH may also be used in tunnel mode (see [5]) but again since all fields are covered by an authenticator, such as a hash, it is easy to show that both integrity and authentication are provided for the packet.