Dolev-Yao Theory with Associative Blindpair Operators

  • A. BaskarEmail author
  • R. Ramanujam
  • S. P. Suresh
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11601)


In the context of modeling cryptographic tools like blind signatures and homomorphic encryption, the Dolev-Yao model is typically extended with an operator over which encryption is distributive. The intruder deduction problem has a non-elementary upper bound when the extended operator is an Abelian group operator. Here we show that the intruder deduction problem is DEXPTIME-complete when we restrict the operator to satisfy only the associative property. We propose an automata-based analysis for the upper bound and use the reachability problem for alternating pushdown systems to show the lower bound.


  1. 1.
    Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 367(1–2), 2–32 (2006). Scholar
  2. 2.
    Avanesov, T., Chevalier, Y., Rusinowitch, M., Turuani, M.: Satisfiability of general intruder constraints with and without a set constructor. J. Symbolic Comput. 80, 27–61 (2017). Scholar
  3. 3.
    Baskar, A.: Decidability results for extended Dolev-Yao theories. Ph.D. thesis, Chennai Mathematical Institute (2011)Google Scholar
  4. 4.
    Baskar, A., Ramanujam, R., Suresh, S.: Dolev-Yao theory with associative blindpair operators, Technical report (2019).
  5. 5.
    Baskar, A., Ramanujam, R., Suresh, S.P.: Knowledge-based modelling of voting protocols. In: Samet, D. (ed.) TARK 2007, pp. 62–71 (2007).
  6. 6.
    Baskar, A., Ramanujam, R., Suresh, S.P.: A dexptime-complete Dolev-Yao theory with distributive encryption. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 102–113. Springer, Heidelberg (2010). Scholar
  7. 7.
    Ciobâca, S., Delaune, S., Kremer, S.: Computing knowledge in security protocols under convergent equational theories. J. Autom. Reason. 48(2), 219–262 (2012). Scholar
  8. 8.
    Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: LICS 2003, pp. 271–280. IEEE Computer Society (2003).
  9. 9.
    Cortier, V., Delaune, S.: Decidability and combination results for two notions of knowledge in security protocols. J. Autom. Reason. 48(4), 441–487 (2012). Scholar
  10. 10.
    Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur. 14(1), 1–43 (2006). Scholar
  11. 11.
    Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Trans. Inf. Theory 29(2), 198–207 (1983). Scholar
  12. 12.
    Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for the equational theory of Abelian groups with distributive encryption. Inf. Comput. 205(4), 581–623 (2007). Scholar
  13. 13.
    Rusinowitch, M., Turuani, M.: Protocol insecurity with a finite number of sessions and composed keys is NP-complete. Theor. Comput. Sci. 299(1–3), 451–475 (2003). Scholar
  14. 14.
    Suwimonteerabuth, D., Schwoon, S., Esparza, J.: Efficient algorithms for alternating pushdown systems with an application to the computation of certificate chains. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 141–153. Springer, Heidelberg (2006). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.BITS Pilani, K K Birla Goa CampusGoaIndia
  2. 2.Institute of Mathematical SciencesChennaiIndia
  3. 3.CMI and CNRS UMI 2000 ReLaXChennaiIndia

Personalised recommendations