Some publications




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

SecRet

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