Stuart G. Stubblebine
AT&T Labs-Research - Catherine A. Meadows
Naval Research Laboratory
Formal methods have been successfully applied to exceedingly abstract system specifications to verify high level security properties such as authentication, key exchange, and fail-safe revocation. Furthermore, considerable research exists on evaluating particular ciphers and secure hash functions used to implement high level security properties. However, verifying that less abstract system specifications satisfy low level security properties has been largely impractical. This is evidenced by innumerable system vulnerabilities where high level properties are not attained due to failed assumptions of low level properties. This paper presents ongoing work on investigating known and chosen ciphertext pairs using the NRL Protocol Analyzer. We give a formal characterization of known and chosen pairs, and map it to the NRL Protocol Analyzer model. We also describe the use of the Analyzer to rediscover attacks on an early version of the ESP protocol, and show how our experience in using it has led us to refine our model. This was the first use of the Analyzer to model protocols at such a low level of abstraction.