Next: Description of the Attacks
Up: Analysis Using the Analyzer
Previous: Queries for Finding Known
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.