Intruder Deduction for AC-Like Equational Theories with Homomorphisms

  • Pascal Lafourcade
  • Denis Lugiez
  • Ralf Treinen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


Cryptographic protocols are small programs which involve a high level of concurrency and which are difficult to analyze by hand. The most successful methods to verify such protocols rely on rewriting techniques and automated deduction in order to implement or mimic the process calculus describing the protocol execution.

We focus on the intruder deduction problem, that is the vulnerability to passive attacks, in presence of several variants of AC-like axioms (from AC to Abelian groups, including the theory of exclusive or) and homomorphism which are the most frequent axioms arising in cryptographic protocols. Solutions are known for the cases of exclusive or, of Abelian groups, and of homomorphism alone. In this paper we address the combination of these AC-like theories with the law of homomorphism which leads to much more complex decision problems.

We prove decidability of the intruder deduction problem in all cases considered. Our decision procedure is in EXPTIME, except for a restricted case in which we have been able to get a PTIME decision procedure using a property of one-counter and pushdown automata.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148(1), 1–70 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    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
  3. 3.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)Google Scholar
  4. 4.
    Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. In: Proc. of 18th Annual IEEE Symposium on Logic in Computer Science (LICS 2003), Ottawa, Canada, pp. 261–270. IEEE Comp. Soc. Press, Los Alamitos (2003)CrossRefGoogle Scholar
  5. 5.
    Clark, J., Jacob, J.: A survey of authentication protocol literature (1997),
  6. 6.
    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
  7. 7.
    Comon-Lundh, H., Treinen, R.: Easy intruder deductions. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 225–242. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. Research Report LSV-04-15, LSV, ENS de Cachan (September 2004), Available at
  9. 9.
    Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, vol. B, ch. 6, pp. 243–320. Elsevier Science Publishers and The MIT Press (1990)Google Scholar
  10. 10.
    Dolev, D., Yao, A.: On the security of public-key protocols. In: Transactions on Information Theory, vol. 29, pp. 198–208. IEEE Comp. Soc. Press, Los Alamitos (1983)Google Scholar
  11. 11.
    Jacquemard, F.: Security protocols open repository, Available at
  12. 12.
    Kaltofen, E., Krishnamoorthy, M.S., Saunders, B.D.: Fast parallel computation of hermite and smith forms of polynomial matrices. SIAM J. Algebraic Discrete Methods 8(4), 683–690 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for ac-like equational theories with homomorphisms. Research Report LSV-04-16, LSV, ENS de Cachan (November 2004), Available at
  14. 14.
    Lowe, G.: An attack on the Needham-Schroeder public key authentication protocol. Information Processing Letters 56(3), 131–133 (1995)zbMATHCrossRefGoogle Scholar
  15. 15.
    McAllester, D.A.: Automatic recognition of tractability in inference relations. JACM 40(2), 284–303 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Narendran, P.: Solving linear equations over polynomial semirings. In: Proc. of 11th Annual Symposium on Logic in Computer Science (LICS), July 1996, pp. 466–472 (1996)Google Scholar
  17. 17.
    Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)zbMATHGoogle Scholar
  18. 18.
    Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1986)zbMATHGoogle Scholar
  19. 19.
    Turuani, M.: Personal communication (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Pascal Lafourcade
    • 1
    • 2
  • Denis Lugiez
    • 2
  • Ralf Treinen
    • 1
  1. 1.LSVENS de Cachan & CNRS UMR 8643 & INRIA Futurs project SECSICachanFrance
  2. 2.LIFUniversité Aix-Marseille 1 & CNRS UMR 6166Marseille Cedex 13France

Personalised recommendations