The Finite Variant Property: How to Get Rid of Some Algebraic Properties

  • Hubert Comon-Lundh
  • Stéphanie Delaune
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


We consider the following problem: Given a term t, a rewrite system \(\cal R\), a finite set of equations E′ such that \(\cal R\) is E′-convergent, compute finitely many instances of t: t 1,...,t n such that, for every substitution σ, there is an index i and a substitution θ such that \(t\sigma\mathord\downarrow =_{E'} t_i\theta\) (where \(t\sigma\mathord\downarrow\) is the normal form of w.r.t. \(\to_{E'\mathord{\setminus}\mathcal R}\)).

The goal of this paper is to give equivalent (resp. sufficient) conditions for the finite variant property and to systematically investigate this property for equational theories, which are relevant to security protocols verification. For instance, we prove that the finite variant property holds for Abelian Groups, and a theory of modular exponentiation and does not hold for the theory ACUNh (Associativity, Commutativity, Unit, Nilpotence, homomorphism).


Abelian Group Normal Form Variant Property Equational Theory Security Protocol 
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.
    Comon, H.: Complete axiomatizations of some quotient term algebras. Theoretical Computer Science 118(2), 167–191 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Comon-Lundh, H.: Intruder theories (ongoing work). In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 1–4. Springer, Heidelberg (2004), Invited talk, slides available at CrossRefGoogle Scholar
  3. 3.
    Comon-Lundh, H., Cortier, V.: New decidability results for fragments of firstorder logic and application to cryptographic protocols. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 148–164. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  4. 4.
    Comon-Lundh, H., Delaune, S.: The finite variant property: How to get rid of some algebraic properties. Research Report LSV-04-17, Laboratoire Spécification et Vérification, ENS Cachan, France, 21 pages (2004)Google Scholar
  5. 5.
    Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: Proc. of 18th Annual IEEE Symposium on Logic in Computer Science (LICS 2003), Ottawa, Canada, pp. 271–280. IEEE Comp. Soc. Press, Los Alamitos (2003)CrossRefGoogle Scholar
  6. 6.
    Delaune, S., Jacquemard, F.: A decision procedure for the verification of security protocols with explicit destructors. In: Proc. 11th ACM Conference on Computer and Communications Security (CCS 2004), Washington, USA, pp. 278–287. ACM, New York (2004)CrossRefGoogle Scholar
  7. 7.
    Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, ch. 6, Elsevier and MIT Press (1990)Google Scholar
  8. 8.
    Hullot, J.-M.: Canonical forms and unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol. 87, pp. 318–324. Springer, Heidelberg (1980)Google Scholar
  9. 9.
    Hullot, J.-M.: A catalogue of canonical term rewriting systems. Technical Report CSL-114, Computer Science Laboratory, SRI, CA, USA (1980)Google Scholar
  10. 10.
    Kapur, D., Narendran, P., Wang, L.: An E-unification algorithm for analyzing protocols that use modular exponentiation. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 165–179. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    Kirchner, C.: Méthodes et Outils de Conception Systématique d’Algorithmes d’Unification dans les Théories Équationnelles. PhD thesis, Université de Nancy I (1985)Google Scholar
  12. 12.
    Meadows, C., Narendran, P.: A unification algorithm for the group Diffie-Hellman protocol. In: Proc. of the Workshop on Issues in the Theory of Security (WITS 2002), Portland, USA (2002)Google Scholar
  13. 13.
    Narendran, P., Guo, Q., Wolfram, D.: Unification and matching modulo nilpotence. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 261–274. Springer, Heidelberg (1996)Google Scholar
  14. 14.
    Narendran, P., Pfenning, F., Statman, R.: On the unification problem for cartesian closed categories. Journal of Symbolic Logic 62(2), 636–647 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Paulson, L.: Mechanized proofs for a recursive authentication protocol. In: Proc. 10th Computer Security Foundations Workshop (CSFW 1997), Rockport, USA, pp. 84–95. IEEE Comp. Soc. Press, Los Alamitos (1997)CrossRefGoogle Scholar
  16. 16.
    Rackoff, C.: On the complexity of the theories of weak direct products (preliminary report). In: Proc. of the 6th Annual ACM Symposium on Theory of Computing, pp. 149–160. ACM Press, New York (1974)CrossRefGoogle Scholar
  17. 17.
    Ryan, P.Y.A., Schneider, S.A.: An attack on a recursive authentication protocol: A cautionary tale. Information Processing Letters 65(1), 7–10 (1998)CrossRefGoogle Scholar
  18. 18.
    Treinen, R.: A new method for undecidability proofs of first order theories. Journal of Symbolic Computation 14(5), 437–457 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Viola, E.: E-unifiability via narrowing. In: Restivo, A., Ronchi Della Rocca, S., Roversi, L. (eds.) ICTCS 2001. LNCS, vol. 2202, pp. 426–438. Springer, Heidelberg (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Hubert Comon-Lundh
    • 2
  • Stéphanie Delaune
    • 1
    • 2
  1. 1.France Télécom R& D 
  2. 2.Laboratoire Spécification & VérificationENS de Cachan & CNRS UMR 8643Cachan CedexFrance

Personalised recommendations