Abstract
The indistinguishability of two pieces of data (or two lists of pieces of data) can be represented formally in terms of a relation called static equivalence. Static equivalence depends on an underlying equational theory. The choice of an inappropriate equational theory can lead to overly pessimistic or overly optimistic notions of indistinguishability, and in turn to security criteria that require protection against impossible attacks or—worse yet—that ignore feasible ones. In this paper, we define and justify an equational theory for standard, fundamental cryptographic operations. This equational theory yields a notion of static equivalence that implies computational indistinguishability. Static equivalence remains liberal enough for use in applications. In particular, we develop and analyze a principled formal account of guessing attacks in terms of static equivalence.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Baudet, M., Warinschi, B.: Guessing attack and the computational soundness of static equivalence (extended version) (manuscript 2006)
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., Cortier, V.: Deciding knowledge in security protocols under (many more) equational theories. In: Proc. 18th IEEE Computer Security Foundations Workshop (CSFW 2005), pp. 62–76 (2005)
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. 28th ACM Symposium on Principles of Programming Languages (POPL 2001), pp. 104–115 (2001)
Abadi, M., Gordon, A.D.: A bisimulation method for cryptographic protocols. Nordic Journal of Computing 5(4), 267–303 (1998)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (The computational soundness of formal encryption). Journal of Cryptology 15(2), 103–127 (2002)
Abadi, M., Warinschi, B.: Password-based encryption analyzed. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 664–676. Springer, Heidelberg (2005)
Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: Proc. 10th ACM Conference on Computer and Communications Security (CCS 2003), pp. 220–330 (2003)
Bana, G.: Soundness and completeness of formal logics of symmetric encryption. PhD thesis, University of Pensilvania (2004)
Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proc. 12th ACM Conference on Computer and Communications Security (CCS 2005), Alexandria, Virginia, USA, November 2005, pp. 16–25 (2005)
Baudet, M., Cortier, V., Kremer, S.: Computationally sound implementations of equational theories against passive adversaries. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 652–663. Springer, Heidelberg (2005)
Bellare, M., Pointcheval, D., Rogaway, P.: Authenticated key exchange secure against dictionary attacks. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 139–155. Springer, Heidelberg (2000)
Bellovin, S.M., Merritt, M.: Encrypted key exchange: Password-based protocols secure against dictionary attacks. In: Proc. 1992 IEEE Symposium on Security and Privacy (SSP 1992), pp. 72–84 (1992)
Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: Proc. 20th IEEE Symposium on Logic in Computer Science (LICS 2005), pp. 331–340 (2005)
Boreale, M., De Nicola, R., Pugliese, R.: Proof techniques for cryptographic processes. In: Proc. 14th IEEE Symposium on Logic in Computer Science (LICS 1999), pp. 157–166 (1999)
Boyko, V., MacKenzie, P., Patel, S.: Provably secure password-authenticated key exchange using Diffie-Hellman. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 156–171. Springer, Heidelberg (2000)
Corin, R., Doumen, J.M., Etalle, S.: Analysing password protocol security against off-line dictionary attacks. Technical report TR-CTIT-03-52, Centre for Telematics and Information Technology, Univ. of Twente, The Netherlands (2003)
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: IFIP WG 1.7 and ACM SIGPLAN Workshop on Issues in the Theory of Security (WITS 2003), pp. 62–71 (2003)
Delaune, S., Jacquemard, F.: A theory of dictionary attacks and its complexity. In: Proc. 17th IEEE Computer Security Foundations Workshop (CSFW 2004), pp. 2–15 (2004)
Fournet, C.: Private communication (2002)
Gennaro, R., Lindell, Y.: A framework for password-based authenticated key exchange. In: Biham, E. (ed.) EUROCRYPT 2003. LNCS, vol. 2656, pp. 524–543. Springer, Heidelberg (2003)
Goldreich, O., Lindell, Y.: Session key generation using human passwords only. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol. 2139, pp. 403–432. Springer, Heidelberg (2001)
Gong, L.: Verifiable-text attacks in cryptographic protocols. In: Proc. 9th IEEE Conference on Computer Communications (INFOCOM 1990), pp. 686–693 (1990)
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)
Katz, J., Ostrovsky, R., Yung, M.: Practical password-authenticated key exchange provably secure under standard assumptions. In: Pfitzmann, B. (ed.) EUROCRYPT 2001. LNCS, vol. 2045, pp. 475–494. Springer, Heidelberg (2001)
Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: Proc. 2004 IEEE Symposium on Security and Privacy (SSP 2004), pp. 71–85 (2004)
Lowe, G.: Analysing protocols subject to guessing attacks. Journal of Computer Security 12(1), 83–98 (2004)
Micciancio, D., Warinschi, B.: Completeness theorems for the Abadi-Rogaway logic of encrypted expressions. Journal of Computer Security 12(1), 99–129 (2004)
Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 133–151. Springer, Heidelberg (2004)
Phan, D.H., Pointcheval, D.: About the security of ciphers (semantic security and pseudo-random permutations). In: Handschuh, H., Hasan, M.A. (eds.) SAC 2004. LNCS, vol. 3357, pp. 185–200. Springer, Heidelberg (2004)
Steiner, M., Tsudik, G., Waidner, M.: Refinement and extension of encrypted key exchange. ACM SIGOPS Oper. Syst. Rev. 29(3), 22–30 (1995)
Tsudik, G., Herreweghen, E.V.: Some remarks on protecting weak secrets and poorly-chosen keys from guessing attacks. In: Proc. 12th IEEE Symposium on Reliable Distributed Systems (SRDS 1993) (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abadi, M., Baudet, M., Warinschi, B. (2006). Guessing Attacks and the Computational Soundness of Static Equivalence. In: Aceto, L., Ingólfsdóttir, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2006. Lecture Notes in Computer Science, vol 3921. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11690634_27
Download citation
DOI: https://doi.org/10.1007/11690634_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33045-5
Online ISBN: 978-3-540-33046-2
eBook Packages: Computer ScienceComputer Science (R0)