next up previous
Next: Description of the Attacks Up: Analysis Using the Analyzer Previous: Queries for Finding Known

Analysis of the IP Encapsulating Security Protocol

  In this section we describe the current state of our analysis of an early version of the IP Encapsulating Security Protocol or ESP [1,8]. ESP is the protocol of the Internet security architecture for securing IP [2]. It describes formats and transforms for encryption and decryption of data. We selected ESP because its use of CBC mode caused Bellovin to notice a number of possible attacks when it was used under certain system configurations [1,8].

As we mentioned in the last section, our specification of the protocol has an error in it. However, we describe it here both because even with the error we were able to reproduce a number of Bellovin's attacks, and also because we wish to document the process by which the discovery of the error led us to revise our formal definitions of chosen pairs.