Selected publications by Hubert Comon-Lundh

2012

• G. Bana and H. Comon-Lundh.  Towards Unconditional Soundness: Computationally Complete Symbolic Attacker.  In POST'12, LNCS. Springer, 2012. To appear. ( BibTeX )
• H. Comon-Lundh, V. Cortier and G. Scerri.  Security proof with dishonest keys.  In POST'12, LNCS. Springer, 2012. To appear. ( BibTeX )

2011

• H. Comon-Lundh, S. Delaune and J. Millen.  Constraint solving techniques and enriching the model with equational theories.  In Formal Models and Techniques for Analyzing Security Protocols, Cryptology and Information Security Series 5, pages 35-61. IOS Press, 2011. ( PDF | BibTeX + Abstract )
• V. Cheval, H. Comon-Lundh and S. Delaune.  Trace Equivalence Decision: Negative Tests and Non-determinism.  In CCS'11, pages 321-330. ACM Press, 2011. ( PDF | BibTeX + Abstract )
• H. Comon-Lundh and V. Cortier.  How to prove security of communication protocols? A discussion on the soundness of formal models w.r.t. computational ones.  In STACS'11, Leibniz International Proceedings in Informatics 9, pages 29-44. Leibniz-Zentrum für Informatik, 2011. ( PDF | BibTeX + Abstract )

2010

• S. Bursuc, H. Comon-Lundh and S. Delaune.  Deducibility constraints and blind signatures.  Research Report LSV-10-24, Laboratoire Spécification et Vérification, ENS Cachan, France, November 2010. 32 pages. ( PDF | BibTeX + Abstract )
• V. Cheval, H. Comon-Lundh and S. Delaune.  Automating security analysis: symbolic equivalence of constraint systems.  In IJCAR'10, LNAI 6173, pages 412-426. Springer-Verlag, 2010. ( PDF | BibTeX + Abstract )
• H. Comon-Lundh, V. Cortier and E. Zălinescu.  Deciding security properties for cryptographic protocols. Application to key cycles.  ACM Transactions on Computational Logic 11(2), 2010. ( PDF | BibTeX + Abstract )

2009

• S. Bursuc, S. Delaune and H. Comon-Lundh.  Deducibility constraints.  In ASIAN'09, LNCS 5913, pages 24-38. Springer, 2009. ( PDF | PS | PS.GZ | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract )
• V. Cheval, H. Comon-Lundh and S. Delaune.  A decision procedure for proving observational equivalence.  In SecCo'09. 2009. ( PDF | BibTeX )
• M. Abadi, B. Blanchet and H. Comon-Lundh.  Models and Proofs of Protocol Security: A Progress Report.  In CAV'09, LNCS 5643, pages 35-49. Springer, 2009. ( PDF | BibTeX + Abstract )
• S. Bursuc and H. Comon-Lundh.  Protocol security and algebraic properties: decision results for a bounded number of sessions.  In RTA'09, LNCS 5595, pages 133-147. Springer, 2009. ( PDF | BibTeX + Abstract )
• R. Affeldt and H. Comon-Lundh.  Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables.  In Formal to Practical Security, LNCS 5458, pages 1-20. Springer, 2009. ( PDF | BibTeX + Abstract )
• S. Bursuc and H. Comon-Lundh.  Protocols, insecurity decision and combination of equational theories.  Research Report LSV-09-02, Laboratoire Spécification et Vérification, ENS Cachan, France, February 2009. 43 pages. ( PDF | BibTeX + Abstract )

2008

• H. Comon-Lundh.  About models of security protocols.  In FSTTCS'08, Leibniz International Proceedings in Informatics 2. Leibniz-Zentrum für Informatik, 2008. ( PDF | BibTeX + Abstract )
• H. Comon-Lundh and V. Cortier.  Computational Soundness of Observational Equivalence.  In CCS'08, pages 109-118. ACM Press, 2008. ( PDF | BibTeX + Abstract )
• H. Comon-Lundh.  Challenges in the Automated Verification of Security Protocols.  In IJCAR'08, LNAI 5195, pages 396-409. Springer-Verlag, 2008. ( PDF | BibTeX + Abstract )
• H. Comon-Lundh, F. Jacquemard and N. Perrin.  Visibly Tree Automata with Memory and Constraints.  Logical Methods in Computer Science 4(2:8), 2008. ( PDF | BibTeX + Abstract )
• V. Bernat and H. Comon-Lundh.  Normal proofs in intruder theories.  In ASIAN'06, LNCS 4435, pages 151-166. Springer, 2008. ( PDF | BibTeX + Abstract )

2007

• H. Comon-Lundh, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison and M. Tommasi.  Tree Automata Techniques and Applications, 2007. ( Web page | BibTeX )
• S. Bursuc, H. Comon-Lundh and S. Delaune.  Deducibility Constraints, Equational Theory and Electronic Money.  In Rewriting, Computation and Proof, LNCS 4600, pages 196-212. Springer, 2007. ( PS | PS.GZ | BibTeX + Abstract )
• H. Comon-Lundh, C. Kirchner and H. Kirchner (eds.).  Rewriting, Computation and Proof - Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of his 60th Birthday, Cachan, France, June 2007, LNCS 4600. Springer. ( Web page | BibTeX )
• H. Comon-Lundh, F. Jacquemard and N. Perrin.  Tree Automata with Memory, Visibility and Structural Constraints.  In FoSSaCS'07, LNCS 4423, pages 168-182. Springer, 2007. ( PDF | PDF (long version) | BibTeX + Abstract )
• S. Bursuc, H. Comon-Lundh and S. Delaune.  Associative-Commutative Deducibility Constraints.  In STACS'07, LNCS 4393, pages 634-645. Springer, 2007. ( PDF | PS | PS.GZ | BibTeX + Abstract )

2005

• H. Comon-Lundh and S. Delaune.  The finite variant property: How to get rid of some algebraic properties.  In RTA'05, LNCS 3467, pages 294-307. Springer, 2005. ( PDF | PS | PS.GZ | PS (long version) | PS.GZ (long version) | Slides | BibTeX + Abstract )
• H. Comon and V. Cortier.  Tree Automata with One Memory, Set Constraints and Cryptographic Protocols.  Theoretical Computer Science 331(1), pages 143-214, 2005. ( PS | PS.GZ | BibTeX )

2004

• V. Bernat, H. Comon-Lundh, V. Cortier, S. Delaune, F. Jacquemard, P. Lafourcade, Y. Lakhnech and L. Mazaré.  Sufficient conditions on properties for an automated verification: theoretical report on the verification of protocols for an extended model of the intruder.  Technical Report 4, projet RNTL PROUVÉ, December 2004. 33 pages. ( PS | PS.GZ | BibTeX + Abstract )
• H. Comon-Lundh.  Intruder Theories (Ongoing Work).  In FoSSaCS'04, LNCS 2987, pages 1-4. Springer, 2004. Invited talk. ( BibTeX )
• H. Comon-Lundh and V. Cortier.  Security Properties: Two Agents are Sufficient.  Science of Computer Programming 50(1-3), pages 51-71, 2004. ( PS | PS.GZ | BibTeX )

2003

• H. Comon and F. Jacquemard.  Ground Reducibility is EXPTIME-complete.  Information and Computation 187(1), pages 123-153, 2003. ( PDF | PS | PS.GZ | BibTeX )
• H. Comon-Lundh and V. Cortier.  New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protocols.  In RTA'03, LNCS 2706, pages 148-164. Springer, 2003. ( PS | PS.GZ | BibTeX )
• H. Comon-Lundh and V. Shmatikov.  Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive Or.  In LICS'03, pages 271-280. IEEE Computer Society Press, 2003. ( BibTeX )
• H. Comon-Lundh and V. Cortier.  Security properties: two agents are sufficient.  In ESOP'03, LNCS 2618, pages 99-113. Springer, 2003. ( PS | PS.GZ | BibTeX )
• H. Comon-Lundh and R. Treinen.  Easy Intruder Deductions.  In Verification: Theory and Practice, LNCS 2772, pages 225-242. Springer, 2003. Invited paper. ( PS | PS.GZ | BibTeX )
• H. Comon, P. Narendran, R. Nieuwenhuis and M. Rusinowitch.  Deciding the Confluence of Ordered Term Rewrite Systems.  ACM Transactions on Computational Logic 4(1), pages 33-55, 2003. ( BibTeX )
• H. Comon-Lundh and V. Shmatikov.  Constraint Solving, Exclusive Or and the Decision of Confidentiality for Security Protocols Assuming a Bounded Number of Sessions.  Research Report LSV-03-1, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2003. 17 pages. ( PS | PS.GZ | BibTeX )

2002

• H. Comon and V. Shmatikov.  Is it Possible to Decide whether a Cryptographic Protocol is Secure or not?  Journal of Telecommunications and Information Technology 4/2002, pages 5-15, 2002. ( PDF | BibTeX )

2001

• H. Comon.  Inductionless Induction.  In Handbook of Automated Reasoning, chapter 14, pages 913-962. Elsevier Science Publishers, 2001. ( PS | PS.GZ | BibTeX )
• H. Comon and C. Kirchner.  Constraint Solving on Terms.  In CCL'99, LNCS 2002, pages 47-103. Springer, 2001. ( BibTeX )
• H. Comon, C. Marché and R. Treinen (eds.).  Revised Lectures of the International Summer School on Constraints in Computational Logics (CCL'99), Gif-sur-Yvette, France, September 1999, LNCS 2002. Springer, 2001. ( Web page | BibTeX )
• H. Comon, G. Godoy and R. Nieuwenhuis.  The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time.  In FOCS'01, pages 298-307. IEEE Computer Society Press, 2001. ( PS | PS.GZ | BibTeX )
• G. Berry, H. Comon and A. Finkel (eds.).  Proceedings of the 13th International Conference on Computer Aided Verification (CAV'01), Paris, France, July 2001, LNCS 2102. Springer. ( Web page | BibTeX )
• H. Comon, V. Cortier and J. Mitchell.  Tree Automata with One Memory, Set Constraints and Ping-Pong Protocols.  In ICALP'01, LNCS 2076, pages 682-693. Springer, 2001. ( PS | PS.GZ | BibTeX )

2000

• H. Comon and V. Cortier.  Flatness is not a Weakness.  In CSL 2000, LNCS 1862, pages 262-276. Springer, 2000. ( PS | PS.GZ | BibTeX )
• H. Comon and R. Nieuwenhuis.  Inductive Proofs = I-Axiomatization + First-Order Consistency.  Information and Computation 159(1-2), pages 151-186, 2000. ( PS | PS.GZ | BibTeX )
• H. Comon.  Sequentiality, Monadic Second Order Logic and Tree Automata.  Information and Computation 157(1-2), pages 25-51, 2000. ( PS | PS.GZ | BibTeX )

1999

• H. Comon, M. Dincbas, J.-P. Jouannaud and C. Kirchner.  A Methodological View of Constraint Solving.  Constraints 4(4), pages 337-361, 1999. ( PS | PS.GZ | BibTeX )
• H. Comon and Y. Jurski.  Timed Automata and the Theory of Real Numbers.  In CONCUR'99, LNCS 1664, pages 242-257. Springer, 1999. ( PS | PS.GZ | BibTeX )

1998

• H. Comon and Y. Jurski.  Higher-Order Matching and Tree Automata.  In CSL'97, LNCS 1414, pages 157-176. Springer, 1998. ( PS | PS.GZ | BibTeX )
• H. Comon and Y. Jurski.  Higher-order matching and tree automata.  In CSL'97, LNCS 1414, pages 157-176. Springer, 1998. Invited lecture. ( PS | PS.GZ | BibTeX )
• H. Comon and Y. Jurski.  Multiple Counters Automata, Safety Analysis and Presburger Arithmetic.  In CAV'98, LNCS 1427, pages 268-279. Springer, 1998. ( PS | PS.GZ | BibTeX )
• H. Comon, P. Narendran, R. Nieuwenhuis and M. Rusinowitch.  Decision Problems in Ordered Rewriting.  In LICS'98, pages 276-286. IEEE Computer Society Press, 1998. ( PS | PS.GZ | BibTeX )
• H. Comon.  Completion of Rewrite Systems with Membership Constraints. Part I: Deduction Rules.  Journal of Symbolic Computation 25(4), pages 397-420, 1998. ( PS | PS.GZ | BibTeX )
• H. Comon.  Completion of Rewrite Systems with Membership Constraints. Part II: Constraint Solving.  Journal of Symbolic Computation 25(4), pages 421-454, 1998. ( PS | PS.GZ | BibTeX )
• H. Comon.  About proofs by consistency.  In RTA'98, LNCS 1379, pages 136-137. Springer, 1998. Invited lecture. ( BibTeX )

1997

• H. Comon.  Applications of Tree Automata in Rewriting and Lambda-Calculus, Invited lecture, 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97), Warsaw, Poland, 1997. ( BibTeX )
• H. Comon and F. Jacquemard.  Ground Reducibility is EXPTIME-Complete.  In LICS'97, pages 26-34. IEEE Computer Society Press, 1997. ( PS | PS.GZ | BibTeX )
• H. Comon (ed.).  Proceedings of the 8th International Conference on Rewriting Techniques and Applications (RTA'97), June 1997, LNCS 1232. Springer. ( Web page | BibTeX )
• H. Comon and R. Treinen.  The First-Order Theory of Lexicographic Path Orderings is Undecidable.  Theoretical Computer Science 176(1-2), pages 67-87, 1997. ( PS | PS.GZ | BibTeX )
• J.-C. Bajard, H. Comon, C. Kenyon, D. Krob, M. Morvan, J.-M. Muller, A. Petit and Y. Robert.  Exercices d'algorithmique (oraux d'ENS). Vuibert, 1997. ( BibTeX )

1996

• A. Boudet and H. Comon.  Diophantine Equations, Presburger Arithmetic and Finite Automata.  In CAAP'96, LNCS 1059, pages 30-43. Springer, 1996. ( BibTeX )

1995

• A. Boudet and H. Comon.  Résolution de contraintes symboliques, Notes du cours de DEA d'Informatique de Paris Université Paris-Sud 11, Orsay, France, 1995. ( BibTeX )
• H. Comon and J.-P. Jouannaud (eds.).  Term Rewriting: French Spring School of Theoretical Computer Science, Font Romeux, France, May 1993, LNCS 909. Springer, 1995. ( Web page | BibTeX )
• H. Comon and J.-P. Jouannaud.  Les termes en logique et en programmation, Notes du cours de DEA Sémantique, preuves et programmation, 1995. ( BibTeX )
• H. Comon.  Sequentiality, Second-Order Monadic Logic and Tree Automata.  In Theory of Rewriting Systems and Its Applications, Kyoto, Japan, August 1995. Research Institute for Mathematical Sciences, 1995. Invited talk. ( BibTeX )
• H. Comon.  Sequentiality, Second-Order Monadic Logic and Tree Automata.  In LICS'95, pages 508-517. IEEE Computer Society Press, 1995. ( PS | PS.GZ | BibTeX )
• H. Comon, R. Nieuwenhuis and A. Rubio.  Orderings, AC-Theories and Symbolic Constraint Solving.  In LICS'95, pages 375-385. IEEE Computer Society Press, 1995. ( PS | PS.GZ | BibTeX )
• H. Comon.  On Unification of Terms with Integer Exponents.  Mathematical Systems Theory 28(1), pages 67-88, 1995. ( PS | PS.GZ | BibTeX )

1994

• S. Cerrito, H. Comon and C. Crépeau.  Calculabilité et Complexité.  Notes du cours de C3, Maîtrise d'Informatique de Université Paris-Sud 11, Orsay, France, 1994. ( BibTeX )
• H. Comon.  Constraints in Term Algebras (Short Survey).  In AMAST'93, Workshops in Computing, pages 145-152. Springer-Verlag, 1994. Invited paper. ( PS | PS.GZ | BibTeX )
• H. Comon and C. Delor.  Equational Formulae with Membership Constraints.  Information and Computation 112(2), pages 167-216, 1994. ( PS | PS.GZ | BibTeX )
• A.-C. Caron, H. Comon, J.-L. Coquidé, M. Dauchet and F. Jacquemard.  Pumping, Cleaning and Symbolic Constraints Solving.  In ICALP'94, LNCS 820, pages 436-449. Springer-Verlag, 1994. ( BibTeX )
• H. Comon.  Inductionless Induction.  In Lecture Notes of the 2nd International Conference in Logic for Computer Science: Automated Deduction, Université de Savoie, Chambéry, France, July 1994. 1994. ( PS | PS.GZ | BibTeX )
• H. Comon, M. Haberstrau and J.-P. Jouannaud.  Syntacticness, Cycle-Syntacticness and Shallow Theories.  Information and Computation 111(1), pages 154-191, 1994. ( PS | PS.GZ | BibTeX )
• H. Comon and R. Treinen.  Ordering Constraints on Trees.  In CAAP'94, LNCS 787, pages 1-14. Springer-Verlag, 1994. Invited paper. ( PS | PS.GZ | BibTeX )
• H. Comon and F. Jacquemard.  Ground Reducibility and Automata with Disequality Constraints.  In STACS'94, LNCS 775, pages 151-162. Springer-Verlag, 1994. ( BibTeX )

1993

• H. Comon.  Complete Axiomatizations of Some Quotient Term Algebras.  Theoretical Computer Science 118(2), pages 167-191, 1993. ( PS | PS.GZ | BibTeX )
• A. Boudet and H. Comon.  About the Theory of Tree Embedding.  In TAPSOFT'93, LNCS 668, pages 376-390. Springer, 1993. ( PS | PS.GZ | BibTeX )

1992

• H. Comon.  Constraints in Term Algebras. Application to Rewrite Systems.  Atti Degli Incontri Di Logica Matematica 8, pages 5-17, 1992. ( BibTeX )
• H. Comon and M. Fernández.  Negation Elimination in Equational Formulae.  In MFCS'92, LNCS 629, pages 191-199. Springer-Verlag, 1992. ( BibTeX )
• H. Comon.  Completion of Rewrite Systems with Membership Constraints.  In ICALP'92, LNCS 623, pages 392-403. Springer-Verlag, 1992. ( BibTeX )
• H. Comon, M. Haberstrau and J.-P. Jouannaud.  Decidable Problems in Shallow Equational Theories.  In LICS'92, pages 255-262. IEEE Computer Society Press, 1992. ( BibTeX )
• H. Comon.  Résolution de contraintes dans des algèbres de termes.  Mémoire d'habilitation, Laboratoire de Recherche en Informatique, Orsay, France, April 1992. ( PS | PS.GZ | BibTeX )

1991

• H. Comon.  Disunification: a survey.  In Computational Logic - Essays in Honor of Alan Robinson, pages 322-359. MIT Press, 1991. ( PS | PS.GZ | BibTeX + Abstract )
• H. Comon.  Ground normal forms and inductive proofs. Part I: Complement problems.  Research Report 698, Laboratoire de Recherche en Informatique, Orsay, France, 1991. ( BibTeX )
• H. Comon.  Complete axiomatizations of some quotient term algebras.  In ICALP'91, LNCS 510, pages 469-480. Springer-Verlag, 1991. ( PDF | BibTeX )
• H. Comon, D. Lugiez and Ph. Schnoebelen.  A Rewrite-Based Type Discipline for a Subset of Computer Algebra.  Journal of Symbolic Computation 11(4), pages 349-368, 1991. ( BibTeX )

1990

• H. Comon.  Solving symbolic ordering constraints.  International Journal of Foundations of Computer Science 1(4), pages 387-411, 1990. ( PS | PS.GZ | BibTeX + Abstract )
• H. Comon.  Equational formulas in order-sorted algebras.  In ICALP'90, LNCS 443, pages 674-688. Springer-Verlag, 1990. ( BibTeX )
• H. Comon.  Solving inequations in term algebras.  In LICS'90, pages 62-69. IEEE Computer Society Press, 1990. ( BibTeX )

1989

• H. Comon.  Inductive proofs by specifications transformation.  In RTA'89, LNCS 355, pages 76-91. Springer, 1989. ( PDF | BibTeX )
• H. Comon and P. Lescanne.  Equational problems and disunification.  Journal of Symbolic Computation 7(3-4), pages 371-425, 1989. ( PDF | BibTeX + Abstract )

About LSV

• News
• People
• Research
• Seminars
• Teaching
• Contact

• École Normale Supérieure de Cachan
• Centre National de la Recherche Scientifique