Formal characterization and automated analysis of known-pair and chosen-text attacks

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 pairs and chosen text using the NRL Protocol Analyzer. We give a formal characterization of known and chosen pairs, and translate it to necessary and sufficiency conditions in the NRL Protocol Analyzer model. It is the first work the authors are aware of automatically discovering known-pair and chosen-text attacks. We describe the use of the analyzer to rediscover attacks, to find new variants of attacks on an early version of the ESP protocol, and to 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.