Abstract
Equational tree automata accept terms modulo equational theories, and have been used to model algebraic properties of cryptographic primitives in security protocols. A serious limitation is posed by the fact that alternation leads to undecidability in case of theories like ACU and that of Abelian groups, whereas for other theories like XOR, the decidability question has remained open. In this paper, we give a positive answer to this open question by giving effective reductions of alternating general two-way XOR automata to equivalent one-way XOR automata in 3EXPTIME, which also means that they are closed under intersection but not under complementation. We also show that emptiness of these automata, which is needed for deciding secrecy, can be decided directly in 2EXPTIME, without translating them to one-way automata. A key technique we use is the study of Branching Vector Plus-Minimum Systems (BVPMS), which are a variant of VASS (Vector Addition Systems with States), and for which we prove a pumping lemma allowing us to compute their coverability set in EXPTIME.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: Deciding the security of protocols with diffie-hellman exponentiation and products in exponents. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 124–135. Springer, Heidelberg (2003)
Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. In: LICS 2003, pp. 261–270 (2003)
Comon, H., Cortier, V.: Tree automata with one memory, set constraints and cryptographic protocols. Theoretical Computer Science (2004) (to appear)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (1997), http://www.grappa.univ-lille3.fr/tata
Comon-Lundh, H., Cortier, V.: New decidability results for fragments of first-order logic and application to cryptographic protocols. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 148–164. Springer, Heidelberg (2003)
Cortier, V.: Vérification Automatique des Protocoles Cryptographiques. Ph.D. thesis, ENS Cachan, France (2003)
Gécseg, F., Steinby, M.: Tree languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, ch. 1, vol. 3, pp. 1–68. Springer, Heidelberg (1997)
Goubault-Larrecq, J.: A method for automatic cryptographic protocol verification. In: Rolim, J.D.P. (ed.) IPDPS-WS 2000. LNCS, vol. 1800, pp. 977–984. Springer, Heidelberg (2000)
Goubault-Larrecq, J.: Une fois qu’on n’a pas trouvé de preuve, comment le faire comprendre à un assistant de preuve? In: Ménissier-Morain, V. (ed.) Actes des 12èmes Journées Francophones des Langages Applicatifs (JFLA 2004), INRIA, collection didactique (2004)
Goubault-Larrecq, J., Roger, M., Verma, K.N.: Abstraction and resolution modulo AC: How to verify Diffie-Hellman-like protocols automatically. Journal of Logic and Algebraic Programming (2004) (to Appear); Available as Research Report LSV-04-7, LSV, ENS Cachan
Hopcroft, J., Pansiot, J.J.: On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science 8, 135–159 (1979)
Karp, R.M., Miller, R.E.: Parallel program schemata. J. Computer and System Sciences 3(2), 147–195 (1969)
Lugiez, D.: Counting and equality constraints for multitree automata. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 328–342. Springer, Heidelberg (2003)
Monniaux, D.: Abstracting cryptographic protocols with tree automata. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 149–163. Springer, Heidelberg (1999)
Ohsaki, H.: Beyond regularity: Equational tree automata for associative and commutative theories. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 539–553. Springer, Heidelberg (2001)
Paulson, L.C.: Mechanized proofs for a recursive authentication protocol. In: CSFW 1997, pp. 84–95. IEEE Computer Society Press, Los Alamitos (1997)
Ryan, P., Schneider, S.: An attack on a recursive authentication protocol: A cautionary tale. Information Processing Letters 65(1), 7–10 (1998)
Slutzki, G.: Alternating tree automata. Theoretical Computer science 41, 305–318 (1985)
Steiner, M., Tsudik, G., Waidner, M.: Key agreement in dynamic peer groups. IEEE Transactions on Parallel and Distributed Systems 11(8), 769–780 (2000)
Verma, K.N.: Automates d’arbres bidirectionnels modulo théories équationnelles. Ph.D. thesis, ENS Cachan (2003)
Verma, K.N.: On closure under complementation of equational tree automata for theories extending AC. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS, vol. 2850, pp. 183–197. Springer, Heidelberg (2003)
Verma, K.N.: Two-way equational tree automata for AC-like theories: Decidability and closure properties. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 180–196. Springer, Heidelberg (2003)
Verma, K.N., Goubault-Larrecq, J.: Karp-Miller trees for a branching extension of VASS. Research Report LSV-04-3, LSV, ENS Cachan, France (January 2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Verma, K.N. (2004). Alternation in Equational Tree Automata Modulo XOR. In: Lodaya, K., Mahajan, M. (eds) FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2004. Lecture Notes in Computer Science, vol 3328. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30538-5_43
Download citation
DOI: https://doi.org/10.1007/978-3-540-30538-5_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24058-7
Online ISBN: 978-3-540-30538-5
eBook Packages: Computer ScienceComputer Science (R0)