A chosen text attack is characterized by an adversary causing another principal to encrypt or decrypt chosen text using a secret key unknown to the adversary. A known text attack is characterized by an adversary learning encrypted or decrypted text not necessarily chosen by the adversary. Chosen- and known- text in cryptographically protected systems is an important area of study since its presence can lead to vulnerabilities. Chosen- ciphertext can enable the adversary to read confidential messages. Chosen- plaintext can enable the adversary to create messages that may be accepted as legitimate. It can also be used by the adversary to conduct a dictionary attack in an attempt to learn secrets. The problem is compounded when the same key is used for different protocols. Guidance on how to avoid chosen- and known- text attacks has been in the literature for many years [11]. However, attacks based on chosen- and known- text continue to be a problem even in security protocols designed and reviewed by teams of security experts. In spite of this, little work has been done on developing formal theories and techniques for detection and prevention of chosen and known text attacks. This is mainly because the degree of abstraction at which the problem occurs is at a somewhat lower level than that usually handled by most of the existing applications of formal methods of cryptographic protocols. However, as the work of Stubblebine and Gligor [9,10] has shown us, it is possible to apply formal techniques even at the level at which splicing and message decomposition occur and obtain meaningful results.
Analysis of chosen- and known- text is difficult since analysis is tedious and complex. There are many details to consider including numerous message and protocol options. Another factor making analysis difficult is the size of the search space and the fact that system entities can send anything that is known to it.
In this paper we give a formal characterization of chosen and known text. We also give a theory and method for system specification and analysis for chosen and known text. We present some automated techniques using and available tool, the NRL Protocol Analyzer [6]. We discuss the relationship between these techniques and the theory. Finally, we give some examples using our technique to re-discover known attacks.