@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.