@techreport{tica-report, author = {Schnoebelen, {\relax Ph}ilippe and Lugiez, Denis and Comon, Hubert}, title = {A Semantics for Polymorphic Subtypes in Computer Algebra}, type = {Research Report}, number = {711}, year = {1988}, month = mar, institution = {Laboratoire d'Informatique Fondamentale et d'Intelligence Artificielle, Grenoble, France} }

@article{CL-jsc89, publisher = {Elsevier Science Publishers}, journal = {Journal of Symbolic Computation}, author = {Comon, Hubert and Lescanne, Pierre}, title = {Equational problems and disunification}, volume = 7, number = {3-4}, year = 1989, month = mar # {-} # apr, pages = {371-425}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CL-jsc89.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CL-jsc89.pdf}, abstract = {Roughly speaking, an equational problem is a first order formula whose only predicate symbol is~\(=\). We propose some rules for the transformation of equational problems and study their correctness in various models. Then, we give completeness results with respect to some {"}simple{"} problems called solved forms. Such completeness results still hold when adding some control which moreover ensures termination. The termination proofs are given for a {"}weak{"} control and thus hold for the (large) class of algorithms obtained by restricting the scope of the rules. Finally, it must be noted that a by-product of our method is a decision procedure for the validity in the Herbrand Universe of any first order formula with the only predicate symbol~\(=\). } }

@inproceedings{comon-rta89, address = {Chapel Hill, North Carolina, USA}, month = apr, year = 1989, volume = 355, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Dershowitz, Nachum}, acronym = {{RTA}'89}, booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference on {R}ewriting {T}echniques and {A}pplications ({RTA}'89)}, author = {Comon, Hubert}, title = {Inductive proofs by specifications transformation}, pages = {76-91}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/comon-rta89.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/comon-rta89.pdf} }

@inproceedings{comon-icalp90, address = {Warwick, UK}, month = jul, year = 1990, volume = 443, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Paterson, Mike}, acronym = {{ICALP}'90}, booktitle = {{P}roceedings of the 17th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'90)}, author = {Comon, Hubert}, title = {Equational formulas in order-sorted algebras}, pages = {674-688} }

@inproceedings{comon-lics90, address = {Philadelphia, Pennsylvania, USA}, month = jun, year = 1990, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'90}, booktitle = {{P}roceedings of the 5th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'90)}, author = {Comon, Hubert}, title = {Solving inequations in term algebras}, pages = {62-69} }

@article{comon-ijfcs90, publisher = {World Scientific}, journal = {International Journal of Foundations of Computer Science}, author = {Comon, Hubert}, title = {Solving symbolic ordering constraints}, volume = 1, number = 4, pages = {387-411}, year = 1990, month = dec, url = {comon-ijfcs90.ps}, ps = {comon-ijfcs90.ps}, abstract = {We show how to solve boolean combinations of inequations~\(s>t\) in the Herbrand Universe, assuming that \(\geq\)~is interpreted as a \emph{lexicographic path ordering} extending a total precedence. In~other words, we~prove that the existential fragment of the theory of a lexicographic path ordering which extends a total precedence is decidable.} }

@article{comon91, publisher = {Elsevier Science Publishers}, journal = {Journal of Symbolic Computation}, author = {Comon, Hubert and Lugiez, Denis and Schnoebelen, {\relax Ph}ilippe}, title = {A Rewrite-Based Type Discipline for a Subset of Computer Algebra}, volume = {11}, number = {4}, pages = {349-368}, year = {1991}, month = apr }

@inproceedings{comon-icalp91, address = {Madrid, Spain}, month = jul, year = 1991, volume = 510, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Leach Albert, Javier and Monien, Burkhard and Rodriguez-Artalejo, Mario}, acronym = {{ICALP}'91}, booktitle = {{P}roceedings of the 18th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'91)}, author = {Comon, Hubert}, title = {Complete axiomatizations of some quotient term algebras}, pages = {469-480}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/comon-icalp91.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/comon-icalp91.pdf} }

@incollection{comon-robinson91, year = 1991, publisher = {MIT Press}, editor = {Lassez, Jean-Louis and Plotkin, Gordon}, booktitle = {Computational Logic~-- Essays in Honor of Alan Robinson}, author = {Comon, Hubert}, title = {Disunification: a~survey}, pages = {322-359}, url = {comon-robinson91.ps}, ps = {comon-robinson91.ps}, abstract = {Solving an equation in an algebra of terms is known as unification. Solving more complex formulas combining equations and involving in particular negation is called disunification. With such a broad definition, many works fall into the scope of disunification. The goal of this paper is to survey these works and bring them together in a same framework.} }

@techreport{comon-lri698, author = {Comon, Hubert}, title = {Ground normal forms and inductive proofs. Part~I: Complement problems}, type = {Research Report}, number = {698}, institution = {Laboratoire de Recherche en Informatique, Orsay, France}, year = 1991 }

@article{comon92aila, publisher = {Universit{\`a} di Siena, Italy}, journal = {Atti Degli Incontri Di Logica Matematica}, author = {Comon, Hubert}, title = {Constraints in Term Algebras. {A}pplication to Rewrite Systems}, volume = {8}, pages = {5-17}, year = {1992}, missingmonth = {}, missingnmonth = {} }

@phdthesis{comon92habil, author = {Comon, Hubert}, title = {R{\'e}solution de contraintes dans des alg{\`e}bres de termes}, howpublished = {Technical Report LRI-751}, year = {1992}, month = apr, type = {M{\'e}moire d'habilitation}, school = {Laboratoire de Recherche en Informatique, Orsay, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-habilitation.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-habilitation.ps} }

@inproceedings{comon92icalp, address = {Vienna, Austria}, month = jul, year = 1992, volume = 623, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Kuich, Werner}, acronym = {{ICALP}'92}, booktitle = {{P}roceedings of the 19th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'92)}, author = {Comon, Hubert}, title = {Completion of Rewrite Systems with Membership Constraints}, pages = {392-403} }

@inproceedings{comon92lics, address = {Santa Cruz, California, USA}, month = jun, year = 1992, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'92}, booktitle = {{P}roceedings of the 7th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'92)}, author = {Comon, Hubert and Haberstrau, Marianne and Jouannaud, Jean-Pierre}, title = {Decidable Problems in Shallow Equational Theories}, pages = {255-262} }

@inproceedings{comon92mfcs, address = {Prague, Czechoslovakia}, month = aug, year = 1992, volume = 629, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Havel, Ivan M. and Koubek, V{\'a}clav}, acronym = {{MFCS}'92}, booktitle = {{P}roceedings of the 17th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'92)}, author = {Comon, Hubert and Fern{\'a}ndez, Maribel}, title = {Negation Elimination in Equational Formulae}, pages = {191-199} }

@inproceedings{boudet93caap, address = {Orsay, France}, month = apr, year = 1993, volume = 668, series = {Lecture Notes in Computer Science}, nmpublisher = {Springer-Verlag}, publisher = {Springer}, editor = {Gaudel, Marie-Claude and Jouannaud, Jean-Pierre}, acronym = {{TAPSOFT}'93}, booktitle = {{P}roceedings of the 5th {I}nternational {J}oint {C}onference {CAAP}/{FASE} on {T}heory and {P}ractice of {S}oftware {D}evelopment ({TAPSOFT}'93)}, author = {Boudet, Alexandre and Comon, Hubert}, title = {About the Theory of Tree Embedding}, pages = {376-390}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BouCom-tapsoft93.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BouCom-tapsoft93.ps} }

@inproceedings{comon93amast, address = {Twente, The Netherlands}, year = 1994, series = {Workshops in Computing}, publisher = {Springer-Verlag}, editor = {Nivat, Maurice and Rattray, Charles and Rus, Teodor and Scollo, Giuseppe}, acronym = {{AMAST}'93}, booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference on {A}lgebraic {M}ethodology and {S}oftware {T}echnology ({AMAST}'93)}, author = {Comon, Hubert}, title = {Constraints in Term Algebras (Short Survey)}, pages = {145-152}, note = {Invited paper}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-amast93.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-amast93.ps} }

@article{comon93tcs, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Comon, Hubert}, title = {Complete Axiomatizations of Some Quotient Term Algebras}, volume = {118}, number = {2}, pages = {167-191}, year = {1993}, month = sep, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-TCS93.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-TCS93.ps} }

@inproceedings{caron94icalp, address = {Jerusalem, Israel}, month = jul, year = 1994, volume = 820, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Abiteboul, Serge and Shamir, Ali}, acronym = {{ICALP}'94}, booktitle = {{P}roceedings of the 21th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'94)}, author = {Caron, Anne-C{\'e}cile and Comon, Hubert and Coquid{\'e}, Jean-Luc and Dauchet, Max and Jacquemard, Florent}, title = {Pumping, Cleaning and Symbolic Constraints Solving}, pages = {436-449} }

@misc{cerrito94notes, author = {Cerrito, Sernella and Comon, Hubert and Cr{\'e}peau, Claude}, title = {Calculabilit{\'e} et Complexit{\'e}.}, year = {1994}, howpublished = {Notes du cours de C3, Ma\^itrise d'Informatique de Universit{\'e} Paris-Sud~11, Orsay, France} }

@inproceedings{comon94caap, address = {Edinburgh, Scotland, UK}, month = apr, year = 1994, volume = 787, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Tison, Sophie}, acronym = {{CAAP}'94}, booktitle = {{P}roceedings of the 19th {I}nternational {C}olloquium on {T}rees in {A}lgebra and {P}rogramming ({CAAP}'94)}, author = {Comon, Hubert and Treinen, Ralf}, title = {Ordering Constraints on Trees}, pages = {1-14}, note = {Invited paper}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-caap94.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-caap94.ps} }

@inproceedings{comon94ecole, address = {Universit{\'e} de Savoie, Chamb{\'e}ry, France}, month = jul, year = 1994, optaddress = {Chamb{\'e}ry, France}, optpublisher = {Universit{\'e} de Savoie}, editor = {David, Ren{\'e}}, booktitle = {{L}ecture {N}otes of the 2nd {I}nternational {C}onference in {L}ogic for {C}omputer {S}cience: {A}utomated {D}eduction}, author = {Comon, Hubert}, title = {Inductionless Induction}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-cours-chambery-94.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ Com-cours-chambery-94.ps} }

@article{comon94ic, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Comon, Hubert and Haberstrau, Marianne and Jouannaud, Jean-Pierre}, title = {Syntacticness, Cycle-Syntacticness and Shallow Theories}, volume = {111}, number = {1}, pages = {154-191}, year = {1994}, month = may, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CHJ-IC94.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CHJ-IC94.ps} }

@article{comon94osa, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Comon, Hubert and Delor, Catherine}, title = {Equational Formulae with Membership Constraints}, volume = {112}, number = {2}, pages = {167-216}, year = {1994}, month = aug, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComDel-IC94.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComDel-IC94.ps} }

@inproceedings{comon94stacs, address = {Caen, France}, month = feb, year = 1994, volume = 775, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Enjalbert, Patrice and Mayr, Ernst W. and Wagner, Klaus W.}, acronym = {{STACS}'94}, booktitle = {{P}roceedings of the 11th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'94)}, author = {Comon, Hubert and Jacquemard, Florent}, title = {Ground Reducibility and Automata with Disequality Constraints}, pages = {151-162} }

@misc{boudet95notes, author = {Boudet, Alexandre and Comon, Hubert}, title = {R{\'e}solution de contraintes symboliques}, year = {1995}, missingnmonth = {}, missingmonth = {}, howpublished = {Notes du cours de DEA d'Informatique de Paris Universit{\'e} Paris-Sud~11, Orsay, France} }

@inproceedings{comon95kyoto, address = {Kyoto, Japan}, month = aug, year = 1995, optaddress = {Kyoto University, Japan}, publisher = {Research Institute for Mathematical Sciences}, editor = {Toyama, Yoshihito}, booktitle = {{T}heory of {R}ewriting {S}ystems and {I}ts {A}pplications}, author = {Comon, Hubert}, title = {Sequentiality, Second-Order Monadic Logic and Tree Automata}, note = {Invited talk} }

@inproceedings{comon95licsa, address = {San Diego, California, USA}, month = jun, year = 1995, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'95}, booktitle = {{P}roceedings of the 10th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'95)}, author = {Comon, Hubert and Nieuwenhuis, Robert and Rubio, Albert}, title = {Orderings, {AC}-Theories and Symbolic Constraint Solving}, pages = {375-385}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CNR-lics95.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CNR-lics95.ps} }

@inproceedings{comon95licsb, address = {San Diego, California, USA}, month = jun, year = 1995, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'95}, booktitle = {{P}roceedings of the 10th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'95)}, author = {Comon, Hubert}, title = {Sequentiality, Second-Order Monadic Logic and Tree Automata}, pages = {508-517}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-lics95.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-lics95.ps} }

@article{comon95mst, publisher = {Springer}, journal = {Mathematical Systems Theory}, author = {Comon, Hubert}, title = {On Unification of Terms with Integer Exponents}, volume = {28}, number = {1}, pages = {67-88}, year = {1995}, month = feb, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-MST95.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-MST95.ps} }

@misc{comon95notes, author = {Comon, Hubert and Jouannaud, Jean-Pierre}, title = {Les termes en logique et en programmation}, year = {1995}, howpublished = {Notes du cours de DEA S{\'e}mantique, preuves et programmation}, missingmonth = {}, missingnmonth = {} }

@inproceedings{boudet96caap, address = {Link{\"o}ping, Sweden}, month = apr, year = 1996, volume = 1059, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Kirchner, H{\'e}l{\`e}ne}, acronym = {{CAAP}'96}, booktitle = {{P}roceedings of the 21st {I}nternational {C}olloquium on {T}rees in {A}lgebra and {P}rogramming ({CAAP}'96)}, author = {Boudet, Alexandre and Comon, Hubert}, title = {Diophantine Equations, {P}resburger Arithmetic and Finite Automata}, pages = {30-43} }

@book{JCB-HC-CK-DK-MM-JMM-AP-YR-livre96, author = {Bajard, Jean-Claude and Comon, Hubert and Kenyon, Claire and Krob, Daniel and Morvan, Michel and Muller, Jean-Michel and Petit, Antoine and Robert, Yves}, title = {Exercices d'algorithmique (oraux d'{ENS})}, year = {1997}, publisher = {Vuibert}, month = jan, pages = {272}, isbn = {2-84180-105-5}, lsv-lang = {FR} }

@inproceedings{comon97lics, address = {Warsaw, Poland}, month = jul, year = 1997, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'97}, booktitle = {{P}roceedings of the 12th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'97)}, author = {Comon, Hubert and Jacquemard, Florent}, title = {Ground Reducibility is {EXPTIME}-Complete}, pages = {26-34}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ComJac-lics97.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComJac-lics97.ps}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ComJac-lics97.pdf} }

@misc{comon97licsb, author = {Comon, Hubert}, title = {Applications of Tree Automata in Rewriting and Lambda-Calculus}, year = 1997, month = jul, howpublished = {Invited lecture, 12th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'97), Warsaw, Poland} }

@article{comon97tcs, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Comon, Hubert and Treinen, Ralf}, title = {The First-Order Theory of Lexicographic Path Orderings is Undecidable}, volume = {176}, number = {1-2}, pages = {67-87}, year = {1997}, month = apr, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ComTre-TCS97.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComTre-TCS97.ps}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ComTre-TCS97.pdf} }

@misc{edf-comon-97, author = {Comon, Hubert}, title = {Une approche logique des contr{\^o}les logiques}, year = {1997}, month = jun, howpublished = {Rapport de contrat EDF/DER/MOS--LSV}, lsv-lang = {FR} }

@inproceedings{cj-csl97, address = {{\AA}rhus, Denmark}, year = 1998, volume = 1414, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Nielsen, Mogens and Thomas, Wolfgang}, acronym = {{CSL}'97}, booktitle = {{S}elected {P}apers from the 11th {I}nternational {W}orkshop on {C}omputer {S}cience {L}ogic ({CSL}'97)}, author = {Comon, Hubert and Jurski, Yan}, title = {Higher-Order Matching and Tree Automata}, pages = {157-176}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CJ-csl97.pdf}, ps = {CJ-csl97.ps}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CJ-csl97.pdf} }

@techreport{alcatel-ComPad-98a, author = {Comon, Hubert and Padovani, Vincent}, title = {Specifications Consistency Verification. {I}ntermediate Report}, year = {1998}, month = sep, type = {Contract Report}, number = {MAR/UAO/C/98/0051} }

@techreport{alcatel-ComPad-98b, author = {Comon, Hubert and Padovani, Vincent}, title = {Specifications Consistency Verification. {F}inal Report}, year = {1998}, month = dec, type = {Contract Report}, number = {MAR/UAO/C/98/0080}, note = {280 pages} }

@inproceedings{comon97csl, address = {{\AA}rhus, Denmark}, year = 1998, volume = 1414, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Nielsen, Mogens and Thomas, Wolfgang}, acronym = {{CSL}'97}, booktitle = {{S}elected {P}apers from the 11th {I}nternational {W}orkshop on {C}omputer {S}cience {L}ogic ({CSL}'97)}, author = {Comon, Hubert and Jurski, Yan}, title = {Higher-order matching and tree automata}, pages = {157-176}, note = {Invited lecture}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComJur-csl97.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComJur-csl97.ps} }

@article{comon97jsc1, publisher = {Elsevier Science Publishers}, journal = {Journal of Symbolic Computation}, author = {Comon, Hubert}, title = {Completion of Rewrite Systems with Membership Constraints. {P}art~{I}: {D}eduction Rules}, volume = {25}, number = {4}, pages = {397-420}, year = {1998}, month = apr, optnote = {This is a first part of a paper whose abstract appeared in Proc.\ {ICALP '92}, Vienna.}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-cirs1.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-cirs1.ps} }

@article{comon97jsc2, publisher = {Elsevier Science Publishers}, journal = {Journal of Symbolic Computation}, author = {Comon, Hubert}, title = {Completion of Rewrite Systems with Membership Constraints. {P}art~{II}: {C}onstraint Solving}, volume = {25}, number = {4}, pages = {421-454}, year = {1998}, month = apr, optnote = {This is the second part of a paper whose abstract appeared in Proc.\ {ICALP '92}, Vienna.}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-cirs2.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-cirs2.ps} }

@inproceedings{comon98cav, address = {Vancouver, British Columbia, Canada}, month = jun, year = 1998, volume = 1427, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Hu, Alan J. and Vardi, Moshe Y.}, acronym = {{CAV}'98}, booktitle = {{P}roceedings of the 10th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'98)}, author = {Comon, Hubert and Jurski, Yan}, title = {Multiple Counters Automata, Safety Analysis and {P}resburger Arithmetic}, pages = {268-279}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComJur-cav98.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComJur-cav98.ps} }

@inproceedings{comon98lics, address = {Indianapolis, Indiana, USA}, month = jun, year = 1998, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'98}, booktitle = {{P}roceedings of the 13th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'98)}, author = {Comon, Hubert and Narendran, Paliath and Nieuwenhuis, Robert and Rusinowitch, Micha{\"e}l}, title = {Decision Problems in Ordered Rewriting}, pages = {276-286}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CNNR-lics98.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CNNR-lics98.ps} }

@inproceedings{comon98rta, address = {Tsukuba, Japan}, month = mar, year = 1998, volume = 1379, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Nipkow, Tobias}, acronym = {{RTA}'98}, booktitle = {{P}roceedings of the 9th {I}nternational {C}onference on {R}ewriting {T}echniques and {A}pplications ({RTA}'98)}, author = {Comon, Hubert}, title = {About proofs by consistency}, pages = {136-137}, note = {Invited lecture} }

@techreport{LSV:99:5, author = {Padovani, Vincent and Comon, Hubert and Leneutre, J. and Tingaud, R.}, missingauthor = {}, title = {A Formal Verification of Telephone Supplementary Service Interactions}, type = {Research Report}, number = {LSV-99-5}, year = {1999}, month = may, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-1999-5.rr.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-1999-5.rr.ps} }

@techreport{alcatel-ComPad-99a, author = {Comon, Hubert and Padovani, Vincent}, title = {Report on Specification Validation in Telecommunication Services}, year = {1999}, month = jun, type = {Contract Report}, missinginstitution = {} }

@article{comon97cacm, publisher = {Kluwer Academic Publishers}, journal = {Constraints}, author = {Comon, Hubert and Dincbas, Mehmet and Jouannaud, Jean-Pierre and Kirchner, Claude}, title = {A Methodological View of Constraint Solving}, volume = {4}, number = {4}, pages = {337-361}, year = {1999}, month = dec, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-constraints.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-constraints.ps} }

@inproceedings{comon99, address = {Eindhoven, The Netherlands}, month = aug, year = 1999, volume = 1664, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Baeten, Jos C. M. and Mauw, Sjouke}, acronym = {{CONCUR}'99}, booktitle = {{P}roceedings of the 10th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'99)}, author = {Comon, Hubert and Jurski, Yan}, title = {Timed Automata and the Theory of Real Numbers}, pages = {242-257}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComJur-concur99.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComJur-concur99.ps} }

@article{comon00ic2, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Comon, Hubert and Nieuwenhuis, Robert}, title = {Inductive Proofs = {I}-Axiomatization + First-Order Consistency}, volume = {159}, number = {1-2}, pages = {151-186}, year = {2000}, month = may # {-} # jun, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-1998-9.rr.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-1998-9.rr.ps} }

@inproceedings{comon2000csl, address = {Fischbachau, Germany}, month = aug, year = 2000, volume = 1862, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Clote, Peter and Schwichtenberg, Helmut}, acronym = {{CSL} 2000}, booktitle = {{P}roceedings of the 14th {I}nternational {W}orkshop on {C}omputer {S}cience {L}ogic ({CSL} 2000)}, author = {Comon, Hubert and Cortier, V{\'e}ronique}, title = {Flatness is not a Weakness}, pages = {262-276}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComCor-csl2000.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComCor-csl2000.ps} }

@article{comon97ic, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Comon, Hubert}, title = {Sequentiality, Monadic Second Order Logic and Tree Automata}, volume = {157}, number = {1-2}, pages = {25-51}, year = {2000}, month = feb # {-} # mar, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-sequentiality-ic.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ Com-sequentiality-ic.ps} }

@techreport{LSV:01:13, author = {Comon, Hubert and Cortier, V{\'e}ronique}, title = {Tree Automata with One Memory, Set Constraints and Cryptographic Protocols}, type = {Research Report}, number = {LSV-01-13}, year = {2001}, month = dec, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, note = {98 pages}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2001-13.rr.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2001-13.rr.ps} }

@inproceedings{ccm-icalp2001, address = {Heraklion, Crete, Grece}, month = jul, year = 2001, volume = 2076, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Orejas, Fernando and Spirakis, Paul G. and van Leeuwen, Jan}, acronym = {{ICALP}'01}, booktitle = {{P}roceedings of the 28th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'01)}, author = {Comon, Hubert and Cortier, V{\'e}ronique and Mitchell, John}, title = {Tree Automata with One Memory, Set Constraints and Ping-Pong Protocols}, pages = {682-693}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CCM-icalp2001.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CCM-icalp2001.ps} }

@inproceedings{cgn-focs2001, address = {Las Vegas, Nevada, USA}, month = oct, year = 2001, publisher = {{IEEE} Computer Society Press}, acronym = {{FOCS}'01}, booktitle = {{P}roceedings of the 42nd {S}ymposium on {F}oundations of {C}omputer {S}cience ({FOCS}'01)}, author = {Comon, Hubert and Godoy, Guillem and Nieuwenhuis, Robert}, title = {The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time}, pages = {298-307}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CGN-focs2001.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CGN-focs2001.ps} }

@inproceedings{comon01ccl, address = {Gif-sur-Yvette, France}, year = 2001, volume = 2002, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Comon, Hubert and March{\'e}, {\relax Cl}aude and Treinen, Ralf}, acronym = {{CCL}'99}, booktitle = {{R}evised {L}ectures of the {I}nternational {S}ummer {S}chool on {C}onstraints in {C}omputational {L}ogics ({CCL}'99)}, author = {Comon, Hubert and Kirchner, Claude}, title = {Constraint Solving on Terms}, pages = {47-103} }

@incollection{comon99hb, author = {Comon, Hubert}, title = {Inductionless Induction}, editor = {Robinson, Alan and Voronkov, Andrei}, booktitle = {Handbook of Automated Reasoning}, volume = {1}, chapter = {14}, pages = {913-962}, year = {2001}, missingmonth = {}, missingnmonth = {}, publisher = {Elsevier Science Publishers}, isbn = {0-444-82949-0}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HC-hb.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HC-hb.ps} }

@article{comon02jtit, address = {Warsaw, Poland}, publisher = {Instytut {\L}{\k a}csno{\'s}ci}, journal = {Journal of Telecommunications and Information Technology}, author = {Comon, Hubert and Shmatikov, Vitaly}, title = {Is it Possible to Decide whether a Cryptographic Protocol is Secure or not?}, volume = {4/2002}, year = {2002}, pages = {5-15}, missingmonth = {}, missingnmonth = {}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JTIT-CS.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JTIT-CS.pdf} }

@article{CNNR-tocl03, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Comon, Hubert and Narendran, Paliath and Nieuwenhuis, Robert and Rusinowitch, Micha{\"e}l}, title = {Deciding the Confluence of Ordered Term Rewrite Systems}, volume = {4}, number = {1}, pages = {33-55}, year = {2003}, month = jan }

@inproceedings{ComCor-esop2003, address = {Warsaw, Poland}, month = apr, year = 2003, volume = 2618, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Degano, Pierpaolo}, acronym = {{ESOP}'03}, booktitle = {{P}roceedings of the 12th {E}uropean {S}ymposium on {P}rogramming ({ESOP}'03)}, author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique}, title = {Security properties: two agents are sufficient}, pages = {99-113}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortierESOP03.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortierESOP03.ps} }

@inproceedings{ComCor-rta2003, address = {Valencia, Spain}, month = jun, year = 2003, volume = 2706, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Nieuwenhuis, Robert}, acronym = {{RTA}'03}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {R}ewriting {T}echniques and {A}pplications ({RTA}'03)}, author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique}, title = {New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protocols}, pages = {148-164}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2003-2.rr.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2003-2.rr.ps} }

@article{ComJac-IC2003, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Comon, Hubert and Jacquemard, Florent}, title = {Ground Reducibility is {EXPTIME}-complete}, volume = {187}, number = {1}, pages = {123-153}, year = {2003}, month = nov, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJ-icomp.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJ-icomp.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CJ-icomp.ps} }

@inproceedings{ComTre-mann03, month = feb, year = 2003, volume = 2772, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Dershowitz, Nachum}, acronym = {{V}erification: {T}heory and {P}ractice}, booktitle = {{V}erification: {T}heory and {P}ractice, {E}ssays {D}edicated to {Z}ohar {M}anna on the {O}ccasion of {H}is 64th {B}irthday}, author = {Comon{-}Lundh, Hubert and Treinen, Ralf}, title = {Easy Intruder Deductions}, pages = {225-242}, note = {Invited paper}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CT-manna.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CT-manna.ps} }

@techreport{LSV:03:1, author = {Comon{-}Lundh, Hubert and Shmatikov, Vitaly}, title = {Constraint Solving, Exclusive Or and the Decision of Confidentiality for Security Protocols Assuming a Bounded Number of Sessions}, type = {Research Report}, number = {LSV-03-1}, year = {2003}, month = jan, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, note = {17~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2003-1.rr.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2003-1.rr.ps} }

@inproceedings{comon03lics, address = {Ottawa, Canada}, month = jun, year = 2003, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'03}, booktitle = {{P}roceedings of the 18th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'03)}, author = {Comon{-}Lundh, Hubert and Shmatikov, Vitaly}, title = {Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive Or}, pages = {271-280} }

@article{ComonCortier-TCS1, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Comon, Hubert and Cortier, V{\'e}ronique}, title = {Tree Automata with One Memory, Set Constraints and Cryptographic Protocols}, year = {2005}, volume = 331, number = 1, pages = {143-214}, month = feb, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortierTCS1.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortierTCS1.ps}, doi = {10.1016/j.tcs.2004.09.036} }

@article{ComonCortier04scp, publisher = {Elsevier Science Publishers}, journal = {Science of Computer Programming}, author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique}, title = {Security Properties: {T}wo Agents are Sufficient}, volume = {50}, number = {1-3}, pages = {51-71}, year = {2004}, month = mar, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortier-step2.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortier-step2.ps} }

@techreport{Prouve:rap4, author = {Bernat, Vincent and Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie and Jacquemard, Florent and Lafourcade, Pascal and Lakhnech, Yassine and Mazar{\'e}, Laurent}, title = {Sufficient conditions on properties for an automated verification: theoretical report on the verification of protocols for an extended model of the intruder }, year = {2004}, month = dec, type = {Technical Report}, number = 4, institution = {projet RNTL PROUV{\'E}}, oldhowpublished = {Rapport Technique 4 du projet RNTL PROUV\'E}, note = {33~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap4.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap4.ps}, abstract = {Cryptographic protocols are successfully analyzed using formal methods. However, formal approaches usually consider the encryption schemes as black boxes and assume that an adversary cannot learn anything from an encrypted message except if he has the key. Such an assumption is too strong in general since some attacks exploit in a clever way the interaction between protocol rules and properties of cryptographic operators. Moreover, the executability of some protocols relies explicitly on some algebraic properties of cryptographic primitives such as commutative encryption. We first give an overview of the existing methods in formal approaches for analyzing cryptographic protocols. Then we describe more precisely the results obtained by the partners of the RNTL project PROUV\'E.} }

@inproceedings{comon04fossacs, address = {Barcelona, Spain}, month = mar, year = 2004, volume = 2987, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Walukiewicz, Igor}, acronym = {{FoSSaCS}'04}, booktitle = {{P}roceedings of the 7th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'04)}, author = {Comon{-}Lundh, Hubert }, title = {Intruder Theories (Ongoing Work)}, pages = {1-4}, note = {Invited talk} }

@inproceedings{ComDel-rta2005, address = {Nara, Japan}, month = apr, year = 2005, volume = 3467, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Giesl, J{\"u}rgen}, acronym = {{RTA}'05}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {R}ewriting {T}echniques and {A}pplications ({RTA}'05)}, author = {Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie}, title = {The finite variant property: {H}ow to get rid of some algebraic properties}, pages = {294-307}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-CD.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/rta05-CD.ps}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-CD.pdf}, doi = {10.1007/b135673}, abstract = {We consider the following problem: Given a term \(t\), a rewrite system \(\mathcal{R}\), a finite set of equations \(E'\) such that \(\mathcal{R}\) is convergent modulo~\(E'\), compute finitely many instances of~\(t\): \(t_1,\ldots,t_n\) such that, for every substitution~\(\sigma\), there is an index \(i\) and a substitution~\(\theta\) such that \( t\sigma\mathord{\downarrow}=_{E'} t_i\theta\) (where \(t\sigma\mathord{\downarrow}\) is the normal form of \(t\sigma\) w.r.t.~\(\mathcal{R}/E'\)). \par 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~\textit{ACUNh} (Associativity, Commutativity, Unit, Nilpotence, homomorphism).} }

@inproceedings{BC-asian06, address = {Tokyo, Japan}, month = jan, year = 2008, volume = 4435, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Okada, Mitsu and Satoh, Ichiro}, acronym = {{ASIAN}'06}, booktitle = {{R}evised {S}elected {P}apers of the 11th {A}sian {C}omputing {S}cience {C}onference ({ASIAN}'06)}, author = {Bernat, Vincent and Comon{-}Lundh, Hubert}, title = {Normal proofs in intruder theories}, pages = {151-166}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-asian06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-asian06.pdf}, doi = {10.1007/978-3-540-77505-8_12}, abstract = {Given an arbitrary intruder deduction capability, modeled as an inference system~\(\mathcal{S}\) and a protocol, we show how to compute an inference system~\(\widehat{\mathcal{S}}\) such that the security problem for an unbounded number of sessions is equivalent to the deducibility of some message in~\(\widehat{\mathcal{S}}\). Then, assuming that \(\mathcal{S}\)~has some subformula property, we lift such a property to~\(\widehat{\mathcal{S}}\), thanks to a proof normalisation theorem. In~general, for an unbounded number of sessions, this provides with a complete deduction strategy. In case of a bounded number of sessions, our theorem implies that the security problem is co-NP-complete. As an instance of our result we get a decision algorithm for the theory of blind-signatures, which, to our knowledge, was not known before.} }

@inproceedings{BCD-jouannaud, address = {Cachan, France}, month = jun, year = 2007, volume = 4600, series = {Lecture Notes in Computer Science}, publisher = {Springer}, acronym = {{R}ewriting, {C}omputation and {P}roof}, booktitle = {{R}ewriting, {C}omputation and {P}roof~--- {E}ssays {D}edicated to {J}ean-{P}ierre {J}ouannaud on the {O}ccasion of his 60th {B}irthday}, editor = {Comon{-}Lundh, Hubert and Kirchner, Claude and Kirchner, H{\'e}l{\`e}ne}, author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie}, title = {Deducibility Constraints, Equational Theory and Electronic Money}, pages = {196-212}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCD-jpj07.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCD-jpj07.ps}, doi = {10.1007/978-3-540-73147-4_10}, abstract = {The starting point of this work is a case study (from France T\'el\'ecom) of an electronic purse protocol. The~goal was to prove that the protocol is secure or that there is an attack. Modeling the protocol requires algebraic properties of a fragment of arithmetic, typically containing modular exponentiation. The~usual equational theories described in papers on security protocols are too weak: the~protocol cannot even be executed in these models. We~consider here an equational theory which is powerful enough for the protocol to be executed, and for which unification is still decidable.\par Our main result is the decidability of the so-called intruder deduction problem, i.e.,~security in presence of a passive attacker, taking the algebraic properties into account. Our~equational theory is a combination of several equational theories over non-disjoint signatures.} }

@inproceedings{CJP-fossacs07, address = {Braga, Portugal}, month = mar, year = 2007, volume = 4423, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Seidl, Helmut}, acronym = {{FoSSaCS}'07}, booktitle = {{P}roceedings of the 10th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'07)}, author = {Comon{-}Lundh, Hubert and Jacquemard, Florent and Perrin, Nicolas}, title = {Tree Automata with Memory, Visibility and Structural Constraints}, pages = {168-182}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJP-fossacs07.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJP-fossacs07.pdf}, doi = {10.1007/978-3-540-71389-0_13}, abstract = {Tree automata with one memory have been introduced in~2001. They generalize both pushdown (word) automata and the tree automata with constraints of equality between brothers of Bogaert and Tison. Though it has a decidable emptiness problem, the main weakness of this model is its lack of good closure properties. We~propose a generalization of the visibly pushdown automata of Alur and Madhusudan to a family of tree recognizers which carry along their (bottom-up) computation an auxiliary unbounded memory with a tree structure (instead of a symbol stack). In~other words, these recognizers, called visibly Tree Automata with Memory~(VTAM) define a subclass of tree automata with one memory enjoying Boolean closure properties. We show in particular that they can be determinized and the problems like emptiness, inclusion and universality are decidable for~VTAM. Moreover, we propose an extension of VTAM whose transitions may be constrained by structural equality and disequality tests between memories, and show that this extension preserves the good closure and decidability properties. } }

@inproceedings{BCD-stacs2007, address = {Aachen, Germany}, month = feb, year = 2007, volume = 4393, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Thomas, Wolfgang and Weil, Pascal}, acronym = {{STACS}'07}, booktitle = {{P}roceedings of the 24th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'07)}, author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie}, title = {Associative-Commutative Deducibility Constraints}, pages = {634-645}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-stacs07.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-stacs07.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCD-stacs07.ps}, doi = {10.1007/978-3-540-70918-3_54}, abstract = {We consider deducibility constraints, which are equivalent to particular Diophantine systems, arising in the automatic verification of security protocols, in presence of associative and commutative symbols. We show that deciding such Diophantine systems is, in general, undecidable. Then, we consider a simple subclass, which we show decidable. Though the solutions of these problems are not necessarily semi-linear sets, we show that there are (computable) semi-linear sets whose minimal solutions are not too far from the minimal solutions of the system. Finally, we consider a small variant of the problem, for which there is a much simpler decision algorithm. } }

@book{TATA07, author = {Comon{-}Lundh, Hubert and Dauchet, Max and Gilleron, R{\'e}mi and L{\"o}ding, Cristof and Jacquemard, Florent and Lugiez, Denis and Tison, Sophie and Tommasi, Marc}, title = {Tree Automata Techniques and Applications}, year = 2007, month = nov, url = {http://www.grappa.univ-lille3.fr/tata/}, nmhowpublished = {Available on: \url{http://www.grappa.univ-lille3.fr/tata}}, nmnote = {release October, 12th 2007} }

@inproceedings{HCL-fsttcs08, address = {Bangalore, India}, month = dec, year = 2008, volume = 2, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Hariharan, Ramesh and Mukund, Madhavan and Vinay, V.}, acronym = {{FSTTCS}'08}, booktitle = {{P}roceedings of the 28th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'08)}, author = {Comon{-}Lundh, Hubert}, title = {About models of security protocols}, nopages = {}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HCL-fsttcs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HCL-fsttcs08.pdf}, abstract = {In this paper, mostly consisting of definitions, we~revisit the models of security protocols: we~show that the symbolic and the computational models (as~well as others) are instances of a same generic model. Our definitions are also parametrized by the security primitives, the notion of attacker and, to some extent, the process calculus.} }

@inproceedings{CLC-ccs08, address = {Alexandria, Virginia, USA}, month = oct, year = 2008, publisher = {ACM Press}, acronym = {{CCS}'08}, booktitle = {{P}roceedings of the 15th {ACM} {C}onference on {C}omputer and {C}ommunications {S}ecurity ({CCS}'08)}, author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique}, title = {Computational Soundness of Observational Equivalence}, pages = {109-118}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CLC-ccs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CLC-ccs08.pdf}, doi = {10.1145/1455770.1455786}, abstract = {Many security properties are naturally expressed as indistinguishability between two versions of a protocol. In this paper, we show that computational proofs of indistinguishability can be considerably simplified, for a class of processes that covers most existing protocols. More precisely, we show a soundness theorem, following the line of research launched by Abadi and Rogaway in~2000: computational indistinguishability in presence of an active attacker is implied by the observational equivalence of the corresponding symbolic processes. We prove our result for symmetric encryption, but the same techniques can be applied to other security primitives such as signatures and public-key encryption. The proof requires the introduction of new concepts, which are general and can be reused in other settings.} }

@inproceedings{HCL-ijcar08, address = {Sydney, Australia}, month = aug, year = 2008, volume = {5195}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer-Verlag}, editor = {Armando, Alessandro and Baumgartner, Peter and Dowek, Gilles}, acronym = {{IJCAR}'08}, booktitle = {{P}roceedings of the 4th {I}nternational {J}oint {C}onference on {A}utomated {R}easoning ({IJCAR}'08)}, author = {Comon{-}Lundh, Hubert}, title = {Challenges in the Automated Verification of Security Protocols}, pages = {396-409}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HCL-ijcar08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HCL-ijcar08.pdf}, doi = {10.1007/978-3-540-71070-7_34}, abstract = {The application area of security protocols raises several problems that are relevant to automated deduction. We describe in this note some of these challenges.} }

@article{CJP-lmcs08, journal = {Logical Methods in Computer Science}, author = {Comon{-}Lundh, Hubert and Jacquemard, Florent and Perrin, Nicolas}, title = {Visibly Tree Automata with Memory and Constraints}, year = 2008, month = jun, volume = 4, number = {2\string:8}, nopages = {}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJP-lmcs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJP-lmcs08.pdf}, doi = {10.2168/LMCS-4(2:8)2008}, abstract = {Tree automata with one memory have been introduced in~2001. They generalize both pushdown (word) automata and the tree automata with constraints of equality between brothers of Bogaert and Tison. Though it has a decidable emptiness problem, the main weakness of this model is its lack of good closure properties.\par We propose a generalization of the visibly pushdown automata of Alur and~Madhusudan to a family of tree recognizers which carry along their (bottom-up) computation an auxiliary unbounded memory with a tree structure (instead of a symbol stack). In~other words, these recognizers, called Visibly Tree Automata with Memory~(VTAM) define a subclass of tree automata with one memory enjoying Boolean closure properties. We~show in particular that they can be determinized and the problems like emptiness, membership, inclusion and universality are decidable for VTAM. Moreover, we propose several extensions of VTAM whose transitions may be constrained by different kinds of tests between memories and also constraints \emph{{\`a}~la} Bogaert and~Tison. We~show that some of these classes of constrained VTAM keep the good closure and decidability properties, and we demonstrate their expressiveness with relevant examples of tree languages.} }

@misc{hcl:lecture07, author = {Comon{-}Lundh, Hubert}, title = {Soundness of abstract cryptography}, oldhowpublished = {Lecture notes, part 1. Available at \url{http://staff.aist.go.jp/h.comon-lundh/}}, year = {2007}, note = {Course notes (part~1), Symposium on Cryptography and Information Security (SCIS2008), Tokai, Japan}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CL-sac08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CL-sac08.pdf} }

@inproceedings{CCD-secco09, address = {Bologna, Italy}, month = oct, year = 2009, editor = {Boreale, Michele and Kremer, Steve}, acronym = {{SecCo}'09}, booktitle = {{P}reliminary {P}roceedings of the 7th {I}nternational {W}orkshop on {S}ecurity {I}ssues in {C}oordination {M}odels, {L}anguages and {S}ystems ({SecCo}'09)}, author = {Cheval, Vincent and Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie}, title = {A~decision procedure for proving observational equivalence}, nmnote = {did not appear in postproceedings EPTCS7}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCD-secco09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCD-secco09.pdf} }

@inproceedings{BCLD-asian09, address = {Seoul, Korea}, month = dec, year = 2009, volume = 5913, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Datta, Anupam}, acronym = {{ASIAN}'09}, booktitle = {{P}roceedings of the 13th {A}sian {C}omputing {S}cience {C}onference ({ASIAN}'09)}, author = {Bursuc, Sergiu and Delaune, St{\'e}phanie and Comon{-}Lundh, Hubert}, title = {Deducibility constraints}, pages = {24-38}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-asian09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-asian09.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCD-asian09.ps}, doi = {10.1007/978-3-642-10622-4_3}, abstract = {In their work on tractable deduction systems, D.~McAllester and later D.~Basin and H.~Ganzinger have identified a property of inference systems (the~locality property) that ensures the tractability of the \textit{Entscheidungsproblem}.\par On~the other hand, deducibility constraints are sequences of deduction problems in which some parts (formulas) are unknown. The~problem is to decide their satisfiability and to represent the set of all possible solutions. Such constraints have also been used for deciding some security properties of cryptographic protocols.\par In this paper we show that local inference systems (actually a slight modification of such systems) yield not only a tractable deduction problem, but also decidable deducibility constraints. Our algorithm not only allows to decide the existence of a solution, but also gives a representation of all solutions.} }

@incollection{ACL-fps09, noaddress = {}, month = may, year = 2009, volume = 5458, series = {Lecture Notes in Computer Science}, publisher = {Springer}, noacronym = {}, booktitle = {{F}ormal to {P}ractical {S}ecurity}, editor = {Cortier, V{\'e}ronique and Kirchner, Claude and Okada, Mitsuhiro and Sakurada, Hideki}, author = {Affeldt, Reynald and Comon{-}Lundh, Hubert}, title = {Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables}, pages = {1-20}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACL-fps09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACL-fps09.pdf}, doi = {10.1007/978-3-642-02002-5_1}, abstract = {First-order logic resolution is a standard way to automate the verification of security protocols. However, it sometimes fails to produce security proofs for secure protocols because of the detection of false attacks. For the verification of a bounded number of sessions, false attacks can be avoided by introducing rigid variables. Unfortunately, this yields complicated resolution procedures. We show here that there is a simple translation of the security problem for a bounded number of sessions into first-order logic, that does not introduce false attacks. This is shown by translating clauses involving rigid variables into classical first-order clauses, while preserving satisfiability. We illustrate this approach by giving a complete and terminating strategy for a first-order logic fragment resulting from the above translation, that yields a decision procedure for a bounded number of sessions.} }

@inproceedings{ABC-cav09, address = {Grenoble, France}, month = jun # {-} # jul, year = 2009, volume = 5643, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Bouajjani, Ahmad and Maler, Oded}, acronym = {{CAV}'09}, booktitle = {{P}roceedings of the 21st {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'09)}, author = {Abadi, Mart{\'\i}n and Blanchet, Bruno and Comon{-}Lundh, Hubert}, title = {Models and Proofs of Protocol Security: A~Progress Report}, pages = {35-49}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABC-cav09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABC-cav09.pdf}, doi = {10.1007/978-3-642-02658-4_5}, abstract = {This paper discusses progress in the verification of security protocols. Focusing on a small, classic example, it stresses the use of program-like representations of protocols, and their automatic analysis in symbolic and computational models.} }

@inproceedings{BCL-rta09, address = {Bras{\'\i}lia, Brazil}, month = jun # {-} # jul, year = 2009, volume = 5595, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Treinen, Ralf}, acronym = {{RTA}'09}, booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on {R}ewriting {T}echniques and {A}pplications ({RTA}'09)}, author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert}, title = {Protocol security and algebraic properties: decision results for a bounded number of sessions}, pages = {133-147}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL-rta09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL-rta09.pdf}, doi = {10.1007/978-3-642-02348-4_10}, abstract = {We consider the problem of deciding the security of cryptographic protocols for a bounded number of sessions, taking into account some algebraic properties of the security primitives, for instance Abelian group properties. We propose a general method for deriving decision algorithms, splitting the task into 4 properties of the rewriting system describing the intruder capabilities: locality, conservativity, finite variant property and decidability of one-step deducibility constraints. We illustrate this method on a non trivial example, combining several Abelian Group properties, exponentiation and a homomorphism, showing a decidability result for this combination. } }

@techreport{LSV:09:02, author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert}, title = {Protocols, insecurity decision and combination of equational theories}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2009}, month = feb, type = {Research Report}, number = {LSV-09-02}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-02.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-02.pdf}, note = {43~pages}, abstract = {We consider the problem of finding attacks for a bounded number of sessions of security protocols. We~contribute to this field, showing how to decompose the problem into pieces for a class of equational theories, which includes the hierarchical combinations, as well as non-hierarchical ones. We apply this result to an electronic purse case study: we~show the decidability in co-NP of the insecurity problem for a complex equational theory mixing three Abelian groups, exponentiation and homomorphism properties.\par The main technical contributions rely on equational logic, term rewriting and combination of theories.} }

@article{CCZ-tocl08, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique and Z{\u{a}}linescu, Eugen}, title = {Deciding security properties for cryptographic protocols. Application to key cycles}, volume = 11, number = 2, nopages = {}, month = jan, year = 2010, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCZ-tocl09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCZ-tocl09.pdf}, doi = {10.1145/1656242.1656244}, abstract = {There is a large amount of work dedicated to the formal verification of security protocols. In~this paper, we~revisit and extend the NP-complete decision procedure for a bounded number of sessions. We use a, now standard, deducibility constraint formalism for modeling security protocols. Our~first contribution is to give a simple set of constraint simplification rules, that allows to reduce any deducibility constraint to a set of solved forms, representing all solutions (within the bound on sessions).\par As a consequence, we prove that deciding the existence of key cycles is NP-complete for a bounded number of sessions. The problem of key-cycles has been put forward by recent works relating computational and symbolic models. The so-called soundness of the symbolic model requires indeed that no key cycle (\textit{e.g.},~enc\((k, k)\)) ever occurs in the execution of the protocol. Otherwise, stronger security assumptions (such as KDM-security) are required.\par We show that our decision procedure can also be applied to prove again the decidability of authentication-like properties and the decidability of a significant fragment of protocols with timestamps.} }

@inproceedings{CCD-ijcar10, address = {Edinburgh, Scotland, UK}, month = jul, year = 2010, volume = {6173}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer-Verlag}, editor = {Giesl, J{\"u}rgen and Haehnle, Reiner}, acronym = {{IJCAR}'10}, booktitle = {{P}roceedings of the 5th {I}nternational {J}oint {C}onference on {A}utomated {R}easoning ({IJCAR}'10)}, author = {Cheval, Vincent and Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie}, title = {Automating security analysis: symbolic equivalence of constraint systems}, pages = {412-426}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-ijcar10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-ijcar10.pdf}, doi = {10.1007/978-3-642-14203-1_35}, abstract = {We consider security properties of cryptographic protocols, that are either trace properties (such as confidentiality or authenticity) or equivalence properties (such as anonymity or strong secrecy).\par Infinite sets of possible traces are symbolically represented using \emph{deducibility constraints}. We give a new algorithm that decides the trace equivalence for the traces that are represented using such constraints, in the case of signatures, symmetric and asymmetric encryptions. Our algorithm is implemented and performs well on typical benchmarks. This is the first implemented algorithm, deciding symbolic trace equivalence.} }

@inproceedings{BC-post12, address = {Tallinn, Estonia}, month = mar, year = 2012, volume = {7215}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Degano, Pierpaolo and Guttman, Joshua D.}, acronym = {{POST}'12}, booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on {P}rinciples of {S}ecurity and {T}rust ({POST}'12)}, author = {Bana, Gergei and Comon{-}Lundh, Hubert}, title = {Towards Unconditional Soundness: Computationally Complete Symbolic Attacker}, pages = {189-208}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-post12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-post12.pdf}, doi = {10.1007/978-3-642-28641-4_11}, abstract = {We consider the question of the adequacy of symbolic models versus computational models for the verification of security protocols. We neither try to include properties in the symbolic model that reflect the properties of the computational primitives nor add computational requirements that enforce the soundness of the symbolic model. We propose in this paper a different approach: everything is possible in the symbolic model, unless it contradicts a computational assumption. In this way, we obtain unconditional soundness almost by construction. And we do not need to assume the absence of dynamic corruption or the absence of key-cycles, which are examples of hypotheses that are always used in related works. We set the basic framework, for arbitrary cryptographic primitives and arbitrary protocols, however for trace security properties only.} }

@inproceedings{CCS-post12, address = {Tallinn, Estonia}, month = mar, year = 2012, volume = {7215}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Degano, Pierpaolo and Guttman, Joshua D.}, acronym = {{POST}'12}, booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on {P}rinciples of {S}ecurity and {T}rust ({POST}'12)}, author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique and Scerri, Guillaume}, title = {Security proof with dishonest keys}, pages = {149-168}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCS-post12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCS-post12.pdf}, doi = {10.1007/978-3-642-28641-4_9}, abstract = {Symbolic and computational models are the two families of models for rigorously analysing security protocols. Symbolic models are abstract but offer a high level of automation while computational models are more precise but security proof can be tedious. Since the seminal work of Abadi and Rogaway, a new direction of research aims at reconciling the two views and many soundness results establish that symbolic models are actually sound w.r.t. computational models.\par This is however not true for the prominent case of encryption. Indeed, all existing soundness results assume that the adversary only uses honestly generated keys. While this assumption is acceptable in the case of asymmetric encryption, it is clearly unrealistic for symmetric encryption. In this paper, we provide with several examples of attacks that do not show-up in the classical Dolev-Yao model, and that do not break the IND-CPA nor INT-CTXT properties of the encryption scheme.\par Our main contribution is to show the first soundness result for symmetric encryption and arbitrary adversaries. We consider arbitrary indistinguishability properties and an unbounded number of sessions. This result relies on an extension of the symbolic model, while keeping standard security assumptions: IND-CPA and IND-CTXT for the encryption scheme.} }

@inproceedings{CCD-ccs11, address = {Chicago, Illinois, USA}, month = oct, year = 2011, publisher = {ACM Press}, editor = {Chen, Yan and Danezis, George and Shmatikov, Vitaly}, acronym = {{CCS}'11}, booktitle = {{P}roceedings of the 18th {ACM} {C}onference on {C}omputer and {C}ommunications {S}ecurity ({CCS}'11)}, author = {Cheval, Vincent and Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie}, title = {Trace Equivalence Decision: Negative Tests and Non-determinism}, pages = {321-330}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-ccs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-ccs11.pdf}, doi = {10.1145/2046707.2046744}, abstract = {We consider security properties of cryptographic protocols that can be modeled using the notion of trace equivalence. The notion of equivalence is crucial when specifying privacy-type properties, like anonymity, vote-privacy, and unlinkability.\par In this paper, we give a calculus that is close to the applied pi calculus and that allows one to capture most existing protocols that rely on classical cryptographic primitives. First, we propose a symbolic semantics for our calculus relying on constraint systems to represent infinite sets of possible traces, and we reduce the decidability of trace equivalence to deciding a notion of symbolic equivalence between sets of constraint systems. Second, we develop an algorithm allowing us to decide whether two sets of constraint systems are in symbolic equivalence or not. Altogether, this yields the first decidability result of trace equivalence for a general class of processes that may involve else branches and\slash or private channels (for a bounded number of sessions).} }

@incollection{CDM-fmtasp11, author = {Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie and Millen, Jonathan K.}, title = {Constraint solving techniques and enriching the model with equational theories}, booktitle = {Formal Models and Techniques for Analyzing Security Protocols}, editor = {Cortier, V{\'e}ronique and Kremer, Steve}, series = {Cryptology and Information Security Series}, volume = 5, publisher = {{IOS} Press}, nochapter = {}, pages = {35-61}, year = 2011, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDM-fmtasp11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDM-fmtasp11.pdf}, abstract = {Derivability constraints represent in a symbolic way the infinite set of possible executions of a finite protocol, in presence of an arbitrary active attacker. Solving a derivability constraint consists in computing a simplified representation of such executions, which is amenable to the verification of any (trace) security property. Our goal is to explain this method on a non-trivial combination of primitives.\par In this chapter we explain how to model the protocol executions using derivability constraints, and how such constraints are interpreted, depending on the cryptographic primitives and the assumed attacker capabilities. Such capabilities are represented as a deduction system that has some specific properties. We choose as an example the combination of exclusive-or, symmetric encryption{\slash}decryption and pairing{\slash}unpairing. We explain the properties of the deduction system in this case and give a complete and terminating set of rules that solves derivability constraints. A similar set of rules has been already published for the classical Dolev-Yao attacker, but it is a new result for the combination of primitives that we consider. This allows to decide trace security properties for this combination of primitives and arbitrary finite protocols.} }

@inproceedings{CLC-stacs11, address = {Dortmund, Germany}, month = mar, year = 2011, volume = 9, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {D{\"u}rr, Christoph and Schwentick, {\relax Th}omas}, acronym = {{STACS}'11}, booktitle = {{P}roceedings of the 28th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'11)}, author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique}, title = {How to prove security of communication protocols? A~discussion on the soundness of formal models w.r.t. computational ones}, pages = {29-44}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CLC-stacs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CLC-stacs11.pdf}, doi = {10.4230/LIPIcs.STACS.2011.29}, abstract = {Security protocols are short programs that aim at securing communication over a public network. Their design is known to be error-prone with flaws found years later. That is why they deserve a careful security analysis, with rigorous proofs. Two main lines of research have been (independently) developed to analyse the security of protocols. On the one hand, formal methods provide with symbolic models and often automatic proofs. On the other hand, cryptographic models propose a tighter modeling but proofs are more difficult to write and to check. An approach developed during the last decade consists in bridging the two approaches, showing that symbolic models are sound w.r.t. symbolic ones, yielding strong security guarantees using automatic tools. These results have been developed for several cryptographic primitives (e.g. symmetric and asymmetric encryption, signatures, hash) and security properties. While proving soundness of symbolic models is a very promising approach, several technical details are often not satisfactory. Focusing on symmetric encryption, we describe the difficulties and limitations of the available results.} }

@inproceedings{CCS-cade2013, address = {Lake Placid, New~York, USA}, month = jun, year = 2013, volume = 7898, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Bonacina, Maria Paola}, acronym = {{CADE}'13}, booktitle = {{P}roceedings of the 24th {I}nternational {C}onference on {A}utomated {D}eduction ({CADE}'13)}, author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique and Scerri, Guillaume}, title = {Tractable inference systems: an extension with a deducibility predicate}, pages = {91-108}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCS-cade2013.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCS-cade2013.pdf}, doi = {10.1007/978-3-642-38574-2_6}, abstract = {The main contribution of the paper is a PTIME decision procedure for the satisfiability problem in a class of first-order Horn clauses. Our result is an extension of the tractable classes of Horn clauses of Basin & Ganzinger in several respects. For instance, our clauses may contain atomic formulas \(S \vdash t\) where \(\vdash\) is a predicate symbol and \(S\) is a finite set of terms instead of a term. \(\vdash\)~is used to represent any possible computation of an attacker, given a set of messages~\(S\). The class of clauses that we consider encompasses the clauses designed by Bana~\& Comon-Lundh for security proofs of protocols in a computational model. \par Because of the (variadic) \(\vdash\) predicate symbol, we cannot use ordered resolution strategies only, as in Basin~\& Ganzinger: given \(S \vdash t\), we must avoid computing \(S' \vdash t\) for all subsets \(S'\) of~\(S\). Instead, we design PTIME entailment procedures for increasingly expressive fragments, such procedures being used as oracles for the next fragment. \par Finally, we obtain a PTIME procedure for arbitrary ground clauses and saturated Horn clauses (as in Basin~\& Ganzinger), together with a particular class of (non saturated) Horn clauses with the \(\vdash\) predicate and constraints (which are necessary to cover the application).} }

@inproceedings{BC-ccs14, address = {Scottsdale, Arizona, USA}, month = nov, year = 2014, publisher = {ACM Press}, editor = {Ahn, Gail-Joon and Yung, Moti and Li, Ninghui}, acronym = {{CCS}'14}, booktitle = {{P}roceedings of the 21st {ACM} {C}onference on {C}omputer and {C}ommunications {S}ecurity ({CCS}'14)}, author = {Bana, Gergei and Comon{-}Lundh, Hubert}, title = {A~Computationally Complete Symbolic Attacker for Equivalence Properties}, pages = {609-620}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-ccs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-ccs14.pdf}, doi = {10.1145/2660267.2660276}, abstract = {We consider the problem of computational indistinguishability of protocols. We design a symbolic model, amenable to automated deduction, such that a successful inconsistency proof implies computational indistinguishability. Conversely, symbolic models of distinguishability provide clues for likely computational attacks. We follow the idea we introduced earlier for reachability properties, axiomatizing what an attacker cannot violate. This results a computationally complete symbolic attacker, and ensures unconditional computational soundness for the symbolic analysis. We present a small library of computationally sound, modular axioms, and test our technique on an example protocol. Despite additional difficulties stemming from the equivalence properties, the models and the soundness proofs turn out to be simpler than they were for reachability properties.} }

@incollection{CD-nato12, author = {Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie}, title = {Formal Security Proofs}, booktitle = {Software Safety and Security}, pages = {26-63}, editor = {Nipkow, Tobias and Grumberg, Orna and Hauptmann, Benedikt}, series = {NATO Science for Peace and Security Series~-- D:~Information and Communication Security}, volume = {33}, publisher = {{IOS} Press}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-nato12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-nato12.pdf}, year = 2012, month = may }

@inproceedings{CLHKS-ispec12, address = {Hangzhou, China}, year = 2012, month = apr, volume = 7232, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ryan, Mark D. and Smyth, Ben and Wang, Guilin}, acronym = {{ISPEC}'12}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {I}nformation {S}ecurity {P}ractice and {E}xperience ({ISPEC}'12)}, author = {Comon{-}Lundh, Hubert and Hagiya, Masami and Kawamoto, Yusuke and Sakurada, Hideki}, title = {Computational Soundness of Indistinguishability Properties without Computable Parsing}, pages = {63-79}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CHKS-ispec12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CHKS-ispec12.pdf}, doi = {10.1007/978-3-642-29101-2_5}, abstract = {We provide a symbolic model for protocols using public-key encryption and hash function, and prove that this model is computationally sound: if there is an attack in the computational world, then there is an attack in the symbolic (abstract) model. Our original contribution is that we deal with the security properties, such as anonymity, which cannot be described using a single execution trace, while considering an unbounded number of sessions of the protocols in the presence of active and adaptive adversaries. Our soundness proof is different from all existing studies in that it does not require a computable parsing function from bit strings to terms. This allows us to deal with more cryptographic primitives, such as a preimage-resistant and collision-resistant hash function whose input may have different lengths.} }

@article{BCD-icomp13, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie}, title = {Deducibility constraints and blind signatures}, year = {2014}, month = nov, volume = 238, pages = {106-127}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCD-icomp13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCD-icomp13.pdf}, nonote = {32~pages}, doi = {10.1016/j.ic.2014.07.006}, abstract = {Deducibility constraints represent in a symbolic way the infinite set of possible executions of a finite protocol. Solving a deducibility constraint amounts to finding all possible ways of filling the gaps in a proof. For finite local inference systems, there is an algorithm that reduces any deducibility constraint to a finite set of solved forms. This allows one to decide any trace security property of cryptographic protocols.\par We investigate here the case of infinite local inference systems, through the case study of blind signatures. We show that, in this case again, any deducibility constraint can be reduced to finitely many solved forms (hence we can decide trace security properties). We sketch also another example to which the same method can be applied.} }

@comment{{B-arxiv16, author = Bollig, Benedikt, affiliation = aff-LSVmexico, title = One-Counter Automata with Counter Visibility, institution = Computing Research Repository, number = 1602.05940, month = feb, nmonth = 2, year = 2016, type = RR, axeLSV = mexico, NOcontrat = "", url = http://arxiv.org/abs/1602.05940, PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf", lsvdate-new = 20160222, lsvdate-upd = 20160222, lsvdate-pub = 20160222, lsv-category = "rapl", wwwpublic = "public and ccsb", note = 18~pages, abstract = "In a one-counter automaton (OCA), one can read a letter from some finite alphabet, increment and decrement the counter by one, or test it for zero. It is well-known that universality and language inclusion for OCAs are undecidable. We consider here OCAs with counter visibility: Whenever the automaton produces a letter, it outputs the current counter value along with~it. Hence, its language is now a set of words over an infinite alphabet. We show that universality and inclusion for that model are in PSPACE, thus no harder than the corresponding problems for finite automata, which can actually be considered as a special case. In fact, we show that OCAs with counter visibility are effectively determinizable and closed under all boolean operations. As~a~strict generalization, we subsequently extend our model by registers. The general nonemptiness problem being undecidable, we impose a bound on the number of register comparisons and show that the corresponding nonemptiness problem is NP-complete.", }}

@inproceedings{CK-csf17, address = {Santa Barbara, California, USA}, month = aug, publisher = {{IEEE} Computer Society Press}, editor = {K{\"o}pf, Boris and Chong, Steve}, acronym = {{CSF}'17}, booktitle = {{P}roceedings of the 30th {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'17)}, author = {Comon, Hubert and Koutsos, Adrien}, title = {Formal Computational Unlinkability Proofs of RFID Protocols}, pages = {100-114}, year = {2017}, doi = {10.1109/CSF.2017.9}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CK-csf17.pdf}, url = {http://ieeexplore.ieee.org/document/8049714/}, abstract = {We set up a framework for the formal proofs of RFID protocols in the computational model. We rely on the so-called computationally complete symbolic attacker model. Our contributions are: 1) To design (and prove sound) axioms reflecting the proper- ties of hash functions (Collision-Resistance, PRF). 2) To formalize computational unlinkability in the model. 3) To illustrate the method, providing the first formal proofs of unlinkability of RFID protocols, in the computational model.} }

@article{CCD-ic17, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Vincent Cheval and Hubert Comon{-}Lundh and St{\'e}phanie Delaune}, title = {{A procedure for deciding symbolic equivalence between sets of constraint systems}}, volume = {255}, year = {2017}, pages = {94-125}, doi = {10.1016/j.ic.2017.05.004}, url = {https://www.sciencedirect.com/science/article/pii/S0890540117300949}, abstract = {We consider security properties of cryptographic protocols that can be modelled using trace equivalence, a crucial notion when specifying privacy-type properties, like anonymity, vote-privacy, and unlinkability. Infinite sets of possible traces are symbolically represented using deducibility constraints. We describe an algorithm that decides trace equivalence for protocols that use standard primitives and that can be represented using such constraints. More precisely, we consider symbolic equivalence between sets of constraint systems, and we also consider disequations. Considering sets and disequations is actually crucial to decide trace equivalence for processes that may involve else branches and/or private channels (for a bounded number of sessions). Our algorithm for deciding symbolic equivalence between sets of constraint systems is implemented and performs well in practice. Unfortunately, it does not scale up well for deciding trace equivalence between processes. This is however the first implemented algorithm deciding trace equivalence on such a large class of processes.} }

@inproceedings{CJS-ccs20, address = {Orlando, USA}, month = nov, publisher = {ACM Press}, editor = {Jonathan Katz and Giovanni Vigna}, acronym = {{CCS}'20}, booktitle = {{P}roceedings of the 27th {ACM} {C}onference on {C}omputer and {C}ommunications {S}ecurity ({CCS}'20)}, author = {Hubert Comon and Charlie Jacomme and Guillaume Scerri}, title = {Oracle simulation: a technique for protocol composition with long term shared secrets}, pages = {1427-1444}, year = {2020}, doi = {10.1145/3372297.3417229} }

*This file was generated by
bibtex2html 1.98.*