Symbolic Protocol Analysis in the Union of Disjoint Intruder Theories: Combining Decision Procedures. Yannick Chevalier, MR. Theoretical Computer Science 411 (2010), pp. 1261-1282

*Towards an Automatic Analysis of Web Service Security*
** Yannick Chevalier, Denis Lugiez, Michael Rusinowitch in Frontiers of Combining Systems, 6th International Symposium, FroCoS 2007, Liverpool, UK, September 10-12, 2007, Proceedings. Lecture Notes in Computer Science 4720 Springer 2007, ISBN 978-3-540-74620-1,**
Long version as INRIA Research Report 6341

*Verifying Cryptographic Protocols with Subterms Constraints*
*Yannick Chevalier, Denis Lugiez, Michael Rusinowitch * in 14th International Conference on
Logic for Programming Artificial Intelligence and Reasoning Proceedings. October 15-19, 2007
Yerevan, Armenia. Lecture Notes in Computer Science Springer 2007, ISBN

*Intruders with Caps*
* Siva Anantharaman, Paliath Narendran, Michael Rusinowitch * in 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings. Lecture Notes in Computer Science 4533 Springer 2007, ISBN 978-3-540-73447-5

*
Applying a Theorem Prover to the Verification of Optimistic Replication Algorithms.*
*Abdessamad Imine, Michael Rusinowitch* in Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday. Lecture Notes in Computer Science 4600 Springer 2007, ISBN 978-3-540-73146-7

*Combining
Intruder Theories* **ICALP, International Colloquium on
Automata, Languages and Programming 2005, Lisbon, Portugal. Springer
LNCS** * joint work with Yannick Chevalier*.

*Closure
properties and decision problems of dag automata* **Information
Processing Letters, 2005, Volume 94, no 5, pages "231--240",** *
joint work with Siva Anantharaman, Paliath Narendran*.

*An
NP Decision Procedure for Protocol Insecurity with XOR* **Theoretical
Computer Science,Volume 338, Issues 1-3, 10 June 2005, Pages 247-274** *
joint work with Chevalier, Yannick - Küsters, Ralf - Turuani,
Mathieu *.

*Formal Design and Verification of Operational Transformation
Algorithms for Copies Convergence. ***Theoretical Computer
Science**, December 2005. To appear. *joint work with
Abdessamad Imine, Pascal Molli, Gerald Oster *.

*A
resolution Strategy for Verifying Cryptographic Protocols with CBC
Encryption and Blind Signatures. * In Proc. of the 7th
ACM-SIGPLAN **International Conference on Principles and
Practice of Declarative Programming PPDP'2005**, pages
12-22, Lisboa, Portugal, July 2005. ACM press. *joint work with
V. Cortier, E. Zalinescu.*

*The AVISPA Tool for the automated validation of internet
security protocols and applications, ***17th International
Conference on Computer Aided Verification, CAV'2005**, volume
3576 of * Lecture Notes in Computer Science*, pages 281-285,
Edinburgh, Scotland, 2005. Springer. joint work with AVISPA TEAM.

*Towards Synchronizing Linear Collaborative Objects with
Operational Transformation.* In Farn Wang, editor, **Twenty-Fifth
IFIP WG 6.1 International Conference on Formal Techniques for Networked
and Distributed Systems - FORTE'2005**, volume 3731 of *Lecture
Notes in Computer Science*, pages 411-427, Taipei, Taiwan,
October 2005. Springer.* joint work with Abdessamad Imine, Pascal
Molli, Gerald Oster *.

*Tree vs Dag Automata. ***Proceedings of the 19th
International Workshop on Unification**, pages 93-103, Nara,
Japan, April 2005. * joint work with Siva Anantharaman, Paliath
Narendran*.

*Deciding
the Security of Protocols with Commuting Public Key Encryption.* **
Electronic Notes in Theoretical Computer Science, Volume 125, Issue 1,
Pages 1-161 (3 March 2005)** * joint work with Chevalier,
Yannick - Küsters, Ralf - Turuani, Mathieu *.

*
Tree automata with equality constraints modulo equational theories*.
Research Report LSV-05-16, Laboratoire Spécification et
Vérification, ENS Cachan, France, August 2005. 34
pages. * joint work with * F. Jacquemard,and L. Vigneron.

*Unification
Modulo ACUI Plus Distributivity Axioms* ** Journal of
Automated Reasoning, Vol. 33, issue 1, 2004** * joint work
with Siva Anantharaman, Paliath Narendran*.

*IJCAR*
Automated Reasoning: Second International Joint Conference, IJCAR 2004,
Cork, Ireland, July 4-8, 2004. Proceedings. Lecture Notes in Computer
Science 3097. ISBN: 3-540-22345-2 * co-edited with D. Basin*.

*
Protocol Analysis in Intrusion Detection Using Decision Tree*
International Conference on Information Technology: Coding and Computing
(ITCC'04)Volume 1 April 05 - 07, 2004, Las Vegas, Nevada * joint
work with Tarek Abbes, Adel Bouhoula*.

*Deductive
Verification of Distributed Groupware Systems* AMAST 2004, July
12th - 16th, 2004, Stirling, Scotland, UK. * joint work with
Abdessamad Imine, Pascal Molli, Gerald Oster *.

*
On the Fly Pattern Matching For Intrusion Detection with Snort* Annals of
telecommunications. Vol. 59, n°9-10, sept.-oct. 2004 * joint
work with Tarek Abbes, Adel Bouhoula*.

*Deciding
the Security of Protocols with Diffie-Hellman Exponentiation and
Products in Exponents.* **FST-TCS 03. December 15--17,
2003. Indian Institute of Technology, Bombay. Mumbai, INDIA Lecture
Notes in Computer Science. ** (acc. 20%) * joint work with
Chevalier, Yannick - Küsters, Ralf - Turuani, Mathieu *.

*Computing
Metatransitions for Linear Transition Systems.* **FME
2003, 12th International FME Symposium. Pisa, Italy -September 8-14** *
joint work with Julien Musset*.

*Extending the
Dolev-Yao Intruder for Analyzing an Unbounded Number of Sessions * **CSL
2003, Computer Science Logic, Vienna, Austria** (acc. 26 %) *
joint work with Chevalier, Yannick - Küsters, Ralf - Turuani,
Mathieu -Vigneron, Laurent*.

*An NP Decision
Procedure for Protocol Insecurity with XOR * **LICS'2003**
(acc. 27 %) * joint work with Chevalier, Yannick - Küsters, Ralf
- Turuani, Mathieu *.

*Unification
modulo ACUI plus Homomorphisms/Distributivity* **CADE'2003** *
joint work with Siva Anantharaman, Paliath Narendran*.

*AC(U)ID-Unification
is NEXPTIME-Decidable* **MFCS'2003** * joint
work with Siva Anantharaman, Paliath Narendran*.

*Proving
correctness of transformation functions in real-time groupware* **ECSCW
2003, In 8th European Conference on Computer-Supported Cooperative
Work, Helsinki, Finland** * joint work with Abdessamad Imine,
Pascal Molli, Gérald Oster*.

*Development
of Transformation Functions Assisted by a Theorem Prover* **Proceedings
of the Fourth International Workshop on Collaborative Editing Systems**
Hosted by the ACM Conference on Computer Supported Cooperative Work New
Orleans, Louisiana, November 16, 2002 * joint work with Abdessamad
Imine, Pascal Molli, Gérald Oster*.

*Protocol
Insecurity with Finite Number of Sessions and Composed Keys is
NP-complete * **Theoretical Computer Science A, 299
(2003), pp 451-475** * joint work with M. Turuani*.

*A
Rewriting Approach to Satisfiability Procedures* **Information
and Computation, 183(2): 140-164 (2003)** * joint work with A.
Armando, S. Ranise*.

*Mechanical
Verification of an Ideal ABR Conformance Algorithm* **Journal
of Automated Reasoning, February 2003, Volume 30, Issue 2** *
pp. 153-177, joint work with S. Stratulat and F. Klay*.

*The
AVISS Security Protocols Analysis Tool - system description* **Conference
on Computer Aided Verification 02** * joint work with A.
Armando, David Basin, Mehdi Bouallagui, Yannick Chevalier, Luca
Compagna, Sebastian Moedersheim, Mathieu Turuani, Luca Vigano`, Laurent
Vigneron*.

*Deciding
the Confluence of Ordered Rewriting. * **ACM
Transactions on Computational Logic, TOCL 4(1): 33-55 (2003). ** *
joint work with H. Comon, P. Narendran, R. Nieuwenhuis. *.

*Observational
proofs by rewriting * **Theoretical Computer Science,
275 (1-2) (2002) pp. 675-698** * joint work with A. Bouhoula*.

*Protocol
Insecurity with Finite Number of Sessions is NP-complete * **14th
IEEE Computer Security Foundations Workshop June 11-13, 2001 Cape
Breton, Nova Scotia, Canada ** * joint work with M. Turuani*.

*Incorporating
Decision Procedures in Implicit Induction* **Journal of
Symbolic Computation. Vol. 34, No. 4, October 1, 2002.** *
joint work with A. Armando, S. Stratulat*.

*Uniform
Derivation of Decision Procedures by Superposition* **Proceedings
of Annual Conference of the European Association for Computer Science
Logic, CSL 01 ** * joint work with A. Armando, S. Ranise*. *long
version*

*Compiling
and Verifying Security Protocols* **Logic for Programming
and Automated Reasoning, Reunion Island, november 2000. LNCS 1955.** *
joint work with F. Jacquemard and L. Vigneron*.

*The
theory of total unary rpo is decidable* **First
International Conference on Computational Logic, 24th to 28th July,
2000, London, UK.** * joint work with P. Narendran*.

*Mechanical
Verification of an Ideal ABR Conformance Algorithm* **Conference
on Computer Aided Verification, 15--19 July 2000, Chicago, USA. LNCS
1855** * joint work with S. Stratulat and F. Klay*.

*
Algorithms and Reduction for Rewriting Problems*, **Fundamenta
Informaticae. Volume 46, Number 3, May 2001** * joint work
with R. Verma and D. Lugiez *.

*Patterns
in words vs patterns in trees: a brief survey and some new results,* **International
Conference "Perspectives of Systems Informatics",** * July
1999, Novosibirsk, Russia. LNCS 1755. pages: 280-293. joint work with G.
Kucherov*.

*RPO
Constraint Solving is in NP* , **CSL'98,** *
August 1998. Brno, Tchequie. joint work with P. Narendran, R. Verma*.

*Analyzing
Feature Interactions with Automated Deduction Systems *, **7th
International Conference on Telecommunication Systems Modeling and
Analysis, ** * March 18-21, 1999. Nashville, Tennessee, USA.
joint work with F. Klay, S. Stratulat. Preliminary version *.

*
Decision Problems in Ordered Rewriting*, ** LICS 1998.** *
joint work with H. Comon, P. Narendran, R. Nieuwenhuis *. Long version

*
Algorithms and Reduction for Rewriting Problems*, ** RTA
1998.** * joint work with R. Verma and D. Lugiez *.

*
Observational Proofs with Critical Contexts.*, **Fundamental
Approaches to Software Engineering ** March/April 1998. LNCS
1382, pp 38--53. * joint work with N.Berregeb, A.Bouhoula *.

*
Matching a Set of Strings with Variable Length Don't Cares *, **
Theoretical Computer Science A (178)1-2 (1997) pp. 129-154** *
joint work with G. Kucherov*.

*
Automated verification by induction with associative-commutative
operators.* ** Proceedings 8th International Conference
on Computer Aided Verification, ** volume 1102 of LNCS, pages
220--231, New Jersey, USA, 1996. * joint work with N.~Berregeb and
A.~Bouhoula *.

*Any
ground associative-commutative theory has a finite canonical system.* **
Journal of Automated Reasoning, 17: 131-143, 1996** * joint
work with P. Narendran *.

*Implicit
Induction in Conditional Theories* **Journal of Automated
Reasoning, 14(2):189-235, 1995** *joint work with A. Bouhoula *.

*Automated
Mathematical Induction* **Journal of Logic and
Computation, 1995 **, 5, 5, pages 631--668. *joint work with
A. Bouhoula and E. Kounalis *.

*
Automated Deduction with Associative-Commutative Operators *. **
Applicable Algebra in Engineering, Communication and Computation, 1995 **,
6(1):23-56. * joint work with Laurent Vigneron *.

*Undecidability
of Ground Reducibility for Word Rewriting Systems with Variables*,**Information
Processing Letters**, 53, 1995, pp 209-215. *joint work with
G. Kucherov*, 8 pages

*Complexity
of Testing Ground Reducibility for Linear Word Rewriting Systems With
Variables*, **4th International Workshop on Conditional
(and Typed) Term Rewriting Systems**, 1994, Jerusalem (Israel),
to appear in Lecture Notes in Computer Science, Springer Verlag. *joint
work with G. Kucherov*, 15 pages.

return back to M.Rusinowitch's home page

mail to Michael.Rusinowitch@loria.fr