Faster Basic Syntactic Mutation with Sorts for Some Separable Equational Theories

  • Christopher Lynch
  • Barbara Morawska
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


Sorting information arises naturally in E-unification problems. This information is used to rule out invalid solutions. We show how to use sorting information to make E-unification procedures more efficient. We illustrate our ideas using Basic Syntactic Mutation. We give classes of problems where E-unification becomes polynomial. We show how E-unification can be separated into a polynomial part and a more complicated part using a specialized algorithm. Our approach is motivated by a real problem arising from Cryptographic Protocol Verification.


Polynomial Time Inference Rule Function Symbol Equational Theory Normal Term 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baader, F., Snyder, W.: Unification Theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 447–533. Elsevier Science Publishers, Amsterdam (2001)Google Scholar
  2. 2.
    Comon, H.: Intruder Theories (Ongoing Work). In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 1–4. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    Goguen, J.A., Meseguer, J.: Order-Sorted algebra I: equational deduction for multiple inheritance, overload, exceptions and partial operations. Theoretical Computer Science 105, 217–273 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Hintermeier, C., Kirchner, C., Kirchner, H.: Dynamically-Typed Computations for Order-Sorted Equational Presentations. In: Shamir, E., Abiteboul, S. (eds.) ICALP 1994. LNCS, vol. 820, pp. 450–461. Springer, Heidelberg (1994)Google Scholar
  5. 5.
    Jouannaud, J.P., Kirchner, C.: Solving Equations in Abstract Algebras: A Rule- Based Survey of Unification. In: Lassez, J., Plotkin, G. (eds.) Computational Logic, Essays in Honor of Alan Robinson, vol. ch. 8, pp. 257–321. MIT Press, Cambridge (1991)Google Scholar
  6. 6.
    Lynch, C., Meadows, C.: Sound Approximations to Diffie-Hellman Using Rewrite Rules. In: Proceedings of the Sixth International Conference on Information and Communications Security, Malaga, Spain (October 2004)Google Scholar
  7. 7.
    Lynch, C., Morawska, B.: Basic Syntactic Mutation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 471–485. Springer, Heidelberg (2002)Google Scholar
  8. 8.
    Meadows, C.: Analysis of the Internet Key Exchange Protocol Using the NRL Protocol Analyzer. In: Proceedings of the 1999 IEEE Symposium on Security and Privacy, May 1999, IEEE Computer Society Press, Los Alamitos (1999)Google Scholar
  9. 9.
    Meadows, C.: Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends. IEEE Journal on Selected Areas in Communication 21(1), 44–54 (2003)CrossRefGoogle Scholar
  10. 10.
    Nieuwenhuis, R.: Decidability and Complexity Analysis by Basic Paramodulation. Information and Computation 147, 1–21 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Smolka, G., Nutt, W., Goguen, J.A., Meseguer, J.: Order-Sorted Equational Computation. In: Ait-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures. Rewriting Techniques, vol. 2, ch. 10, pp. 267–297. Academic Press, London (1989)Google Scholar
  12. 12.
    Wallner, D., Harder, E., Agee, R.C.: Key Management for Multicast: Issues and Architectures. RFC 2627 (June 1999)Google Scholar
  13. 13.
    Weidenbach, C.: Sorted Unification and Tree Automata. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction – A Basis for Applications. Applied Logic, vol. 1, ch. 9, pp. 291–320. Kluwer, Dordrecht (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Christopher Lynch
    • 1
  • Barbara Morawska
    • 2
  1. 1.Department of Computer ScienceClarkson UniversityPotsdamUSA
  2. 2.Chair for Automata Theory, Institute for Theoretical Computer ScienceDresden University of TechnologyGermany

Personalised recommendations