Formal characterization and automated analysis of known-pair and chosen-text attacks
- 1 April 2000
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Journal on Selected Areas in Communications
- Vol. 18 (4) , 571-581
- https://doi.org/10.1109/49.839933
Abstract
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.Keywords
This publication has 9 references indexed in Scilit:
- Analysis of the Internet Key Exchange protocol using the NRL Protocol AnalyzerPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- On message integrity in cryptographic protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Protocol design for integrity protectionPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A system for the specification and analysis of key management protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Formal characterization and automated analysis of known-pair and chosen-text attacksIEEE Journal on Selected Areas in Communications, 2000
- The NRL Protocol Analyzer: An OverviewThe Journal of Logic Programming, 1996
- IP Encapsulating Security Payload (ESP)Published by RFC Editor ,1995
- Security Architecture for the Internet ProtocolPublished by RFC Editor ,1995
- Security Mechanisms in High-Level Network ProtocolsACM Computing Surveys, 1983