Abstract
Guessing, or dictionary, attacks arise when an intruder exploits the fact that certain data like passwords may have low entropy, i.e. stem from a small set of values. In the case of off-line guessing, in particular, the intruder may employ guessed values to analyze the messages he has observed. Previous attempts at formalizing off-line guessing consist of extending a Dolev-Yao-style intruder model with inference rules to capture the additional capabilities of the intruder concerning guessable messages. While it is easy to convince oneself that the proposed rules are correct, in the sense that an intruder can actually perform such “guessing steps”, it is difficult to see whether such a system of inference rules is complete in the sense that it captures all the kinds of attacks that we would intuitively call “guessing attacks”. Moreover, the proposed systems are specialized to particular sets of cryptographic primitives and intruder capabilities. As a consequence, these systems are helpful to discover some off-line guessing attacks but are not fully appropriate for formalizing what off-line guessing precisely means and verifying that a given protocol is not vulnerable to such guessing attacks.
In this paper, we give a formalization of off-line guessing by defining a deduction system that is uniform and general in that it is independent of the overall protocol model and of the details of the considered intruder model, i.e. cryptographic primitives, algebraic properties, and intruder capabilities.
This work was partially supported by the FET Open Project IST-2001-39252 and the BBW Project 02.0431, “AVISPA: Automated Validation of Internet Security Protocols and Applications”.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 46–58. Springer, Heidelberg (2004)
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. POPL 2001, ACM Press, New York (2004)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Basin, D., Mödersheim, S., Viganò, L.: An On-The-Fly Model-Checker for Security Protocol Analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 253–270. Springer, Heidelberg (2003)
Basin, D., Mödersheim, S., Viganò, L.: Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols. In: Proc. CCS 2003, ACM Press, New York (2003)
Basin, D., Mödersheim, S., Viganò, L.: OFMC: A Symbolic Model-Checker for Security Protocols. International Journal of Information Security (2004)
Bellare, M., Pointcheval, D., Rogaway, P.: Authenticated key exchange secure against dictionary attacks. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, p. 139. Springer, Heidelberg (2000)
Bellovin, S.M., Merritt, M.: Encrypted key exchange: Password-based protocols secure against dictionary attacks. In: Proc. IEEE Symposium on Security and Privacy 1992, IEEE Computer Society Press, Los Alamitos (1992)
Bresson, E., Chevassut, O., Pointcheval, D.: Security proofs for an efficient password-based key exchange. In: Proc. CCS 2003, ACM Press, New York (2003)
Cohen, E.: Proving cryptographic protocols safe from guessing attacks. In: Proc. Foundations of Computer Security 2002 (2002)
Corin, R., Doumen, J., Etalle, S.: Analysing password protocol security against off-line dictionary attacks. In: Proc. WISP 2004. Electronic Notes in Theoretical Computer Science (2004)
Corin, R., Malladi, S., Alves-Foss, J., Etalle, S.: Guess what? Here is a new tool that finds some new guessing attacks (extended abstract). In: Proc. WITS 2003, Dip. Scienze dell’Informazione, Università di Bologna, Italy (2003)
Delaune, S., Jacquemard, F.: A theory of guessing attacks and its complexity. Research Report LSV-04-1, Lab. Specification and Verification, ENS de Cachan, France (2004)
Dolev, D., Yao, A.: On the Security of Public-Key Protocols. IEEE Transactions on Information Theory 2(29) (1983)
Gong, L., Lomas, T.M.A., Needham, R.M., Saltzer, J.H.: Protecting poorly chosen secrets from guessing attacks. IEEE Journal on Selected Areas in Communications 11(5), 648–656 (1993)
Hamzeh, K., Pall, G., Verthein, W., Taarud, J., Little, W., Zorn, G.: RFC 2637: Point-to-Point Tunneling Protocol (July 1999) Status: Informational
Lowe, G.: Analysing Protocols Subject to Guessing Attacks. In: Proc. WITS 2002 (2002)
Lowe, G.: Analysing Protocols Subject to Guessing Attacks. Journal of Computer Security 12(1) (2004)
Morris, R., Thompson, K.: Password security: A case history. Communications of the ACM 22(11), 594 (1979)
Schneier, B., Mudge, Wagner, D.: Cryptanalysis of Microsoft’s PPTP authentication extensions (MS-CHAPv2). In: Baumgart, R. (ed.) CQRE 1999. LNCS, vol. 1740, p. 192. Springer, Heidelberg (1999)
Zorn, G.: RFC 2759: Microsoft PPP CHAP Extensions, Version 2 (January 2000) Status: Informational
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Drielsma, P.H., Mödersheim, S., Viganò, L. (2005). A Formalization of Off-Line Guessing for Security Protocol Analysis. In: Baader, F., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2005. Lecture Notes in Computer Science(), vol 3452. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32275-7_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-32275-7_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25236-8
Online ISBN: 978-3-540-32275-7
eBook Packages: Computer ScienceComputer Science (R0)