Limits of the Cryptographic Realization of Dolev-Yao-Style XOR

  • Michael Backes
  • Birgit Pfitzmann
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3679)


The abstraction of cryptographic operations by term algebras, called Dolev-Yao models, is essential in almost all tool-supported methods for proving security protocols. Recently significant progress was made in proving that Dolev-Yao models can be sound with respect to actual cryptographic realizations and security definitions. The strongest results show this in the sense of reactive simulatability/UC, a notion that essentially means the preservation of arbitrary security properties under arbitrary active attacks and in arbitrary protocol environments, with only small changes to both Dolev-Yao models and natural implementations.

However, these results are so far restricted to cryptographic systems like encryption and signatures which essentially only have constructors and destructors, but no further algebraic properties. Typical modern tools and complexity results around Dolev-Yao models also allow more algebraic operations. The first such operation considered is typically XOR because of its clear structure and cryptographic usefulness. We show that it is impossible to extend the strong soundness results to XOR, at least not with remotely the same generality and naturalness as for the core cryptographic systems. On the positive side, we show the soundness of a rather general Dolev-Yao model with XOR and its realization under passive attacks.


Cryptographic Protocol Payload Data Cryptographic Operation Cryptographic System Reactive Simulatability 
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.


  1. 1.
    Abadi, M., Blanchet, B., Fournet, C.: Just fast keying in the pi calculus. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 340–354. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Abadi, M., Jürjens, J.: Formal eavesdropping and its computational interpretation. In: Proc. 4th International Symposium on Theoretical Aspects of Computer Software (TACS), pp. 82–94 (2001)Google Scholar
  4. 4.
    Abadi, M., Rogaway, P.: Reconciling two views of cryptography: The computational soundness of formal encryption. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 3–22. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  5. 5.
    Backes, M.: A cryptographically sound dolev-yao style security proof of the otway-rees protocol. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol. 3193, pp. 89–108. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  6. 6.
    Backes, M., Pfitzmann, B.: A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol. IEEE Journal on Selected Areas in Communications 22(10), 2075–2086 (2004)CrossRefGoogle Scholar
  7. 7.
    Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In: Proc. 17th IEEE Computer Security Foundations Workshop (CSFW) Full version in IACR Cryptology ePrint Archive 2004/059 (Febrauary 2004),
  8. 8.
    Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations (extended abstract). In: Proc. 10th ACM Conference on Computer and Communications Security, pp. 220–230 (2003); Full version in IACR Cryptology ePrint Archive 2003/015, January 2003, Scholar
  9. 9.
    Backes, M., Pfitzmann, B., Waidner, M.: Symmetric authentication within a simulatable cryptographic library. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 271–290. Springer, Heidelberg (2003); Extended version in IACR Cryptology ePrint Archive 2003/145, July 2003,
  10. 10.
    Basin, D., Mödersheim, S., Viganò, L.: OFMC: A symbolic model checker for security protocols. International Journal of Information Security (2004)Google Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    Beaver, D.: Secure multiparty protocols and zero knowledge proof systems tolerating a faulty minority. Journal of Cryptology 4(2), 75–122 (1991)CrossRefzbMATHGoogle Scholar
  13. 13.
    Bellare, M., Guérin, R., Rogaway, P.: XOR mACs: New methods for message authentication using finite pseudorandom functions. In: Coppersmith, D. (ed.) CRYPTO 1995. LNCS, vol. 963, pp. 15–28. Springer, Heidelberg (1995)Google Scholar
  14. 14.
    Canetti, R.: Security and composition of multiparty cryptographic protocols. Journal of Cryptology 3(1), 143–202 (2000)CrossRefMathSciNetGoogle Scholar
  15. 15.
    Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: Proc. 42nd IEEE Symposium on Foundations of Computer Science (FOCS), pp. 136–145 (2001) Extended version in Cryptology ePrint Archive, Report 2000/67,
  16. 16.
    Canetti, R., Herzog, J.: Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange). Cryptology ePrint Archive, Report 2004/334 (2004),
  17. 17.
    Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. In: Proc. 23rd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pp. 124–135 (2003)Google Scholar
  18. 18.
    Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. In: Proc. 18th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 261–270 (2003)Google Scholar
  19. 19.
    Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: Proc. 18th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 271–280 (2003)Google Scholar
  20. 20.
    Comon-Lundh, H., Treinen, R.: Easy intruder deductions. Research Report LSV-03-8, Laboratoire Spécification et Vérification, ENS Cachan, France (April 2003)Google Scholar
  21. 21.
    Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system for security protocols and its logical formalization. In: Proc. 16th IEEE Computer Security Foundations Workshop (CSFW), pp. 109–125 (2003)Google Scholar
  22. 22.
    Delaune, S., Jacquemard, F.: Narrowing-based constraint solving for the verification of security protocols. Research Report LSV-04-8, Laboratoire Spécification et Vérification, ENS Cachan, France (April 2004)Google Scholar
  23. 23.
    Denning, D.: Cryptography and Data Security. Addison-Wesley, Reading (1982)zbMATHGoogle Scholar
  24. 24.
    Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)CrossRefMathSciNetzbMATHGoogle Scholar
  25. 25.
    Goldreich, O., Micali, S., Wigderson, A.: How to play any mental game – or – a completeness theorem for protocols with honest majority. In: Proc. 19th Annual ACM Symposium on Theory of Computing (STOC), pp. 218–229 (1987)Google Scholar
  26. 26.
    Goldwasser, S., Levin, L.: Fair computation of general functions in presence of immoral majority. In: Menezes, A., Vanstone, S.A. (eds.) CRYPTO 1990. LNCS, vol. 537, pp. 77–93. Springer, Heidelberg (1991)Google Scholar
  27. 27.
    Kapur, D., Narendran, P., Wang, L.: An e-unification algorithm for analyzing protocols that use modular exponentiation. In: Proc. 14th International Conference on Rewriting Techniques and Applications (RTA), pp. 165–179 (2003)Google Scholar
  28. 28.
    Krawczyk, H.: LFSR-based hashing and authentication. In: Desmedt, Y.G. (ed.) CRYPTO 1994. LNCS, vol. 839, pp. 129–139. Springer, Heidelberg (1994)Google Scholar
  29. 29.
    Laud, P.: Semantics and program analysis of computationally secure information flow. In: Proc. 10th European Symposium on Programming (ESOP), pp. 77–91 (2001)Google Scholar
  30. 30.
    Laud, P.: Computationally Secure Information Flow. PhD thesis, Universität des Saarlandes (2002),
  31. 31.
    Laud, P.: Pseudorandom permutations and equivalence of formal expressions (abstract). In: 14th Nordic Workshop on Programming Theory, pp. 63–65 (2002)Google Scholar
  32. 32.
    Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: Proc. 25th IEEE Symposium on Security & Privacy, pp. 71–85 (2004)Google Scholar
  33. 33.
    Lincoln, P., Mitchell, J., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: Proc. 5th ACM Conference on Computer and Communications Security, pp. 112–121 (1998)Google Scholar
  34. 34.
    Meadows, C.: Using narrowing in the analysis of key management protocols. In: Proc. 10th IEEE Symposium on Security & Privacy, pp. 138–147 (1989)Google Scholar
  35. 35.
    Meadows, C.: A model of computation for the NRL protocol analyzer. In: Proc. 7th IEEE Computer Security Foundations Workshop (CSFW), pp. 84–89 (1994)Google Scholar
  36. 36.
    Meadows, C., Narendran, P.: A unification algorithm for the group Diffie-Hellman protocol. In: Proc. WITS (2002)Google Scholar
  37. 37.
    Micali, S., Rogaway, P.: Secure computation. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 392–404. Springer, Heidelberg (1992)Google Scholar
  38. 38.
    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)CrossRefGoogle Scholar
  39. 39.
    Millen, J.: The Interrogator model. In: Proc. 16th IEEE Symposium on Security & Privacy, pp. 251–260 (1995)Google Scholar
  40. 40.
    Millen, J.: CAPSL: Common Authentication Protocol Specification Language. Technical Report MP 97B48, The MITRE Corporation (1997)Google Scholar
  41. 41.
    Millen, J., Shmatikov, V.: Symbolic protocol analysis with products and Diffie-Hellman exponentiation. In: Proc. 16th IEEE Computer Security Foundations Workshop (CSFW), pp. 47–61 (2003)Google Scholar
  42. 42.
    Paulson, L.: The inductive approach to verifying cryptographic protocols. Journal of Cryptology 6(1), 85–128 (1998)Google Scholar
  43. 43.
    Pfitzmann, B., Waidner, M.: Composition and integrity preservation of secure reactive systems. In: Proc. 7th ACM Conference on Computer and Communications Security, pp. 245–254 (May 2000); Extended version (with Matthias Schunter) IBM Research Report RZ 3206 (May 2000),
  44. 44.
    Pfitzmann, B., Waidner, M.: A model for asynchronous reactive systems and its application to secure message transmission. In: Proc. 22nd IEEE Symposium on Security & Privacy, pp. 184–200 (2001); Extended version of the model (with Michael Backes) IACR Cryptology ePrint Archive 2004/082,
  45. 45.
    Sherman, A.T., McGrew, D.A.: Key establishment in large dynamic groups using one-way function trees. IEEE Transactions on Software Engineering 29(5), 444–458 (2003)CrossRefGoogle Scholar
  46. 46.
    Shmatikov, V.: Decidable analysis of cryptographic protocols with products and modular exponentiation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 355–369. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  47. 47.
    Yao, A.C.: Theory and applications of trapdoor functions. In: Proc. 23rd IEEE Symposium on Foundations of Computer Science (FOCS), pp. 80–91 (1982)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Michael Backes
    • 1
  • Birgit Pfitzmann
    • 1
  1. 1.IBM Zurich Research Lab 

Personalised recommendations