these

Informations

• Publié par: Anjoi
• Nombre de lectures: 60
• Langue: English

Extrait

THÈSE
présentée à l’École Normale Supérieure de Cachan
pour obtenir le grade de
Docteur de l’École Normale Supérieure de Cachan
par : Kumar Neeraj VERMA
Spécialité : INFORMATIQUE
Automates d’arbres bidirectionnels modulo
théories équationnelles
Soutenue le 30 septembre 2003 devant un jury composé de :
Rémi GILLERON examinateur
Jean GOUBAULT-LARRECQ directeur de thèse
Denis LUGIEZ rapporteur
Dale MILLER président du jury
Michaël RUSINOWITCH rapporteur
Helmut SEIDL examinateur2Remerciements
First of all I am extremely grateful to Jean Goubault-Larrecq for having supervised my thesis
and trained me as a researcher. With him I also had my introduction to research during internships
at Dyade and INRIA. His interest in and knowledge of wide variety of subjects in computer science
and mathematics has always surprised me and inspired me. Also his enthusiasm for speaking on these
subjects, as well as various non-academic subjects have helped me learn a lot. I thank him for his
patience and availability to help me and to answer my questions.
I thank Dale Miller for being president of my PhD jury. I thank Denis Lugiez for accepting to
referee this thesis, as well as for discussions and for giving me new ideas through his work. I thank
Michäel Rusinowitch for accepting to referee this thesis. Also thanks to Rémi Gilleron and Helmut
Seidl for accepting to take part in my PhD jury.
Thanks to Hubert Comon for numerous discussions, ideas, and his enthusiasm for working on
problems. I also acknowledge discussions with and feedback from Stéphane Demri, Alain Finkel,
Laurent Fribourg, Jerôme Leroux, Slawek Lasota, Hitoshi Ohsaki, Ralf Treinen, and many others
whose names don’t appear here.
I thank all the members of LSV for providing a wonderful environment for work, for their jokes,
discussions and for supporting me in various ways. Especially, I thank the PhD students and interns
for an enjoyable stay at LSV. I also thank the administrative staff, Brigitte Van-Elsen and Catherine
Forestier, for their patience with my numerous problems.
Finally I thank my parents and family for always supporting me in every way.
345
Automates d’arbres bidirectionnels modulo théories équationnelles
Résumé
Les automates d’arbres bidirectionnels étendent les automates classiques, en ce sens que les tran-
sitions peuvent non seulement construire mais aussi détruire des termes. Récemment des variantes
équationnelles des automates d’arbres ont été proposés qui acceptent des termes modulo une théorie
équationnelle. Dans cette thèse on étudie des automates d’arbres bidirectionnels des théories
équationnelles. On étudie les théories AC (associativité, commutativité de +), ACU (avec unité 0),
ACUI (avec idempotence x + x = x), ACUX (avec annulation x + x = 0) et ACUM (groupes abé-
liens). Ces automates sont importants pour la vérification des protocoles cryptographiques qui utilisent
des primitives cryptographiques non parfaites.
On étudie la décidabilité et la clôture par opérations booléennes de ces automates. On commence
par des résultats négatifs : le vide est indécidable pour les automates bidirectionnels, ou unidirection-
nels alternants, modulo les théories AC, ACU, ACUM.
On montre que les automates unidirectionnels modulo toutes ces théories sont clos par intersec-
tion, et que le vide est décidable. La clôture par union est triviale. A l’opposé, alors que les automates
unidirectionnels modulo AC, ACU sont clos par complémentation, ceux modulo ACUX, ACUM et
ACUI ne le sont pas. Les propriétés de clôture et de décidabilité s’étendent au cas bidirectionnel, pour
chaque théorie sauf ACUI, si on restreint le format des clauses push. On montre cela en réduisant les
automates bidirectionnels aux automates unidirectionnels. (Le cas ACUI est ouvert.) Pour traiter cer-
taines clauses ayant le symbole + dans le corps, on développe une extension des systèmes d’addition
de vecteurs avec états (VASS), appelés VASS étendus. On montre que la construction des arbres de
Karp et Miller pour VASS peut être étendue pour les VASS étendus.
Ces résultats diffèrent nettement du cas des automates non équationnels qui ont toutes les proprié-
tés de clôture et de décidabilité.67
Two-Way Equational Tree Automata
Abstract
Two-way tree automata extend classical tree automata by allowing transitions that can destruct
terms besides constructing them. Recently equational variants of tree automata have been proposed
which accept terms modulo an equational theory. In this thesis we study two-way equational tree auto-
mata. We study the theories AC (associativity, commutativity of +), ACU (with unit 0), ACUI (with
idempotence x + x = x), ACUX (with cancellation x + x = 0) and ACUM (Abelian groups). These
automata are useful in verification of cryptographic protocols which use non-perfect cryptographic
primitives.
We study the properties of decidability and closure under Boolean operations of these automata.
We start with negative results : emptiness is undecidable for alternating one-way automata, as well as
for general two-way automata modulo the theories AC, ACU, ACUM.
We show that the one-way automata modulo all these theories are closed under intersection, and
emptiness is decidable. Closure under union is trivial. On the other hand, while the one-way automata
modulo AC, ACU are closed under complementation, those modulo ACUX, ACUM and ACUI are
not. These closure and decidability properties extend to the two-way case, for each theory except
ACUI, if we restrict the format of push clauses. We show this by reducing the two-way automata to
one-way automata. (The ACUI case is open.) In order to deal with certain push clauses which have
the + symbol in the body, we develop an extension of Vector Addition Systems with States (VASS),
called Extended VASS, in which transitions can add configurations. We show that the construction of
Karp and Miller trees for VASS can be extended for Extended VASS.
Our results on one-way and two-way equational tree automata are strikingly different from the
case of non-equational automata which have all the good closure and decidability properties.8Table des matières
1 Introduction 13
1.1 Cryptographic Protocols and Tree Automata . . . . . . . . . . . . . . . . . . . . . . 16
1.2 Tree Automata and its Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.2.1 Two-Way Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.2.2 Equational Tree Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.3 Contributions of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.4 Plan of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
I Automates d’arbres équationnels et une application aux protocoles cryptogra-
phiques 23
2 Logique du premier ordre 25
2.1 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.2 First Order Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.3 Rewriting Systems and Equational Theories . . . . . . . . . . . . . . . . . . . . . . 28
2.4 Tree Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.4.1 Tree Automata and First Order Logic . . . . . . . . . . . . . . . . . . . . . 31
2.4.2 General Two-Way Tree Automata . . . . . . . . . . . . . . . . . . . . . . . 32
2.5 Logic with Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3 Automates d’arbres bidirectionnels équationnels 37
3.1 Equational Tree Automata as Logic Programs modulo Equational Theories . . . . . 38
3.2 Associative-Commutative Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.2.1 Properties of Terms Modulo AC Theories . . . . . . . . . . . . . . . . . . . 41
3.3 Tree Automata Clauses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
3.3.1 Clauses of One-Way Equational Tree Automata . . . . . . . . . . . . . . . . 44
3.3.2 of Alternating Automata . . . . . . . . . . . . . . . . . . . . . . . . 45
3.3.3 Clauses of Two-Way . . . . . . . . . . . . . . . . . . . . . . . . 45
3.4 Other Formalisms of Equational Tree Automata . . . . . . . . . . . . . . . . . . . . 47
4 Automates d’arbres modulo les théories A et C 51
4.1 C Tree Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
4.2 A Tree . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
910 TABLE DES MATIÈRES
5 Une application des automates d’arbres équationnelles 57
5.1 Group Diffie-Hellman Protocols . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
II Résultats d’indécidabilité 63
6 Résultats 65
6.1 ACU Case . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
6.1.1 With General +-Push Clauses . . . . . . . . . . . . .