Equipe de recherche CASSIS

Publications de l'équipe CASSIS

2012

Articles dans des revues avec comité de lecture

Titre: Loops and overloops for Tree Walking Automata
Auteurs: Pierre-Cyrille Heam ; Vincent Hugot; Olga Kouchnarenko
Détail: Theoretical Computer Science, Elsevier, 2012, Implementation and Application of Automata (CIAA 2011), 450, pp. 43-53
Accès au bibtex

Titre: Decidability of Equivalence of Symbolic Derivations
Auteurs: Yannick Chevalier; Michael Rusinowitch
Détail: Journal of Automated Reasoning, Springer Netherlands, 2012, 48 (2), pp. 263-292
Accès au bibtex

Titre: String rewriting and security analysis: an extension of a result of Book and Otto
Auteurs: Siva Anantharaman ; Paliath Narendran; Michael Rusinowitch
Détail: Journal of Automata, Languages and Combinatorics, 2012, 16 (2--4), pp. 83-98
Accès au bibtex

Titre: Attacking and fixing Helios: An analysis of ballot secrecy
Auteurs: Véronique Cortier; Ben Smyth
Détail: Journal of Computer Security, IOS Press, 2012
Accès au bibtex

Titre: YAPA: A~generic tool for computing intruder knowledge
Auteurs: Mathieu Baudet; Véronique Cortier; Stéphanie Delaune
Détail: ACM Transactions on Computational Logic, ACM Press, 2012
Accès au bibtex

Titre: Decidability and combination results for two notions of knowledge in security protocols.
Auteurs: Véronique Cortier; Stéphanie Delaune
Détail: Journal of Automated Reasoning, Springer-Verlag, 2012, 48 (October), pp. 441-487
Accès au bibtex

Titre: Unification modulo Homomorphic Encryption
Auteurs: Siva Anantharaman; Hai Lin; Christopher Lynch; Paliath Narendran; Michael Rusinowitch
Détail: Journal of Automated Reasoning, Springer Verlag, 2012, 48 (2), pp. 135-158
Accès au bibtex

Titre: Computing knowledge in security protocols under convergent equational theories
Auteurs: Stefan Ciobaca; Stéphanie Delaune; Steve Kremer
Détail: Journal of Automated Reasoning, Springer, 2012, 48 (2), pp. 219-262
Accès au bibtex

Titre: Reducing Equational Theories for the Decision of Static Equivalence
Auteurs: Steve Kremer; Antoine Mercier; Ralf Treinen
Détail: Journal of Automated Reasoning, Springer, 2012, 48 (2), pp. 197-217
Accès au bibtex

Communications avec actes

Titre: Towards the Orchestration of Secured Services under Non-disclosure Policies.
Auteurs: Tigran Avanesov; Yannick Chevalier; Michael Rusinowitch; Mathieu Turuani
Détail: Igor V. Kotenko and Victor A. Skormin. 6th International Conference on Mathematical Methods, Models and Architectures for Computer Network Security, MMM-ACNS 2012, Oct 2012, St. Petersburg, Russian Federation. Springer, 7531, pp. 130-145, Lecture Notes in Computer Science
Accès au bibtex

Titre: Unification modulo Synchronous Distributivity
Auteurs: Siva Anantharaman ; Serdar Erbatur; Christopher Lynch; Paliath Narendran; Michael Rusinowitch
Détail: B. Gramlich, D. Miller, and U. Sattler. IJCAR 2012 (The 6th International Joint Conference on Automated Reasoning), Jun 2012, Manchester, United Kingdom. Springer-Verlag, Berlin, Heidelberg, 7364, pp. 14-29
Accès au bibtex

Titre: Unification modulo Chaining
Auteurs: Siva Anantharaman ; Christopher Bouchard; Paliath Narendran; Michaël Rusinowitch
Détail: A.-H. Dediu and C. Martín-Vide. The 6th International Conference on Language and Automata Theory and Applications, Mar 2012, A Coruna, Spain. Springer, Berlin - Heidelberg, 7183, pp. 70-82, Lecture Notes in Computer Science
Accès au bibtex

Titre: Distributed Orchestration of Web Services under Security Constraints
Auteurs: Tigran Avanesov; Yannick Chevalier; Mohammed Anis Mekki; Michael Rusinowitch; Mathieu Turuani
Détail: 4th SETOP International Workshop on Autonomous and Spontaneous Security, Sep 2011, Leuven, Belgium. Springer, Post-Proceedings of the 4th SETOP International Workshop on Autonomous and Spontaneous Security, 2012, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: Web Services Verification and Prudent Implementation
Auteurs: Tigran Avanesov; Yannick Chevalier; Mohammed Anis Mekki; Michael Rusinowitch
Détail: 4th SETOP International Workshop on Autonomous and Spontaneous Security, Sep 2011, Leuven, Belgium. Springer, Post-Proceedings of the 4th SETOP International Workshop on Autonomous and Spontaneous Security, 2012, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: Security protocols, constraint systems, and group theories
Auteurs: Stéphanie Delaune; Steve Kremer ; Daniel Pasaila
Détail: 6th International Joint Conference on Automated Reasoning (IJCAR'12), Jun 2012, Manchester, United Kingdom. Springer, Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR'12), 7364, pp. 164-178, Lecture Notes in Computer Science
Accès au bibtex

Titre: Revoke and Let Live: A Secure Key Revocation API for Cryptographic Devices
Auteurs: Véronique Cortier; Graham Steel; Cyrille Wiedling
Détail: 19th ACM Conference on Computer and Communications Security (CCS'12), Oct 2012, Raleigh, United States. ACM
Accès au bibtex

Titre: Measuring Vote Privacy, Revisited.
Auteurs: David Bernhard; Véronique Cortier; Olivier Pereira; Bogdan Warinschi
Détail: 19th ACM Conference on Computer and Communications Security (CCS'12), Oct 2012, Raleigh, United States. ACM
Accès au bibtex

Titre: Automated verification of equivalence properties of cryptographic protocols
Auteurs: Rohit Chadha; Stefan Ciobaca; Steve Kremer
Détail: Helmut Seidl. 21th European Symposium on Programming (ESOP'12), Mar 2012, Talinn, Estonia. Springer, Proceedings of the 21th European Symposium on Programming (ESOP'12), 7211, pp. 108-127, Lecture Notes in Computer Science
Accès au bibtex

Titre: A formal analysis of the Norwegian E-voting protocol
Auteurs: Véronique Cortier; Cyrille Wiedling
Détail: Pierpaolo Degano and Joshua D. Guttman. 1st International Conference on Principles of Security and Trust (POST'12), Mar 2012, Tallinn, Estonia. Springer, Proceedings of the 1st International Conference on Principles of Security and Trust (POST'12), 7215, pp. 109-128, Lecture Notes in Computer Science
Accès au bibtex

Titre: Security proof with dishonest keys
Auteurs: Hubert Comon-Lundh; Véronique Cortier; Guillaume Scerri
Détail: Pierpaolo Degano and Joshua D. Guttman. 1st International Conference on Principles of Security and Trust (POST'12), Mar 2012, Tallinn, Estonia. Springer, Proceedings of the 1st International Conference on Principles of Security and Trust (POST'12), 7215, pp. 149-168, Lecture Notes in Computer Science
Accès au bibtex

Titre: Analysing routing protocols: four nodes topologies are sufficient
Auteurs: Véronique Cortier; Jan Degrieck; Stéphanie Delaune
Détail: Pierpaolo Degano and Joshua D. Guttman. 1st International Conference on Principles of Security and Trust (POST'12), Mar 2012, Tallinn, Estonia. Springer, Proceedings of the 1st International Conference on Principles of Security and Trust (POST'12), 7215, pp. 30-50, Lecture Notes in Computer Science
Accès au bibtex

Titre: Program Slicing Enhances a Verification Technique Combining Static and Dynamic Analysis
Auteurs: Omar Chebaro; Nikola\"\i Kosmatov; Alain Giorgetti; Jacques Julliand
Détail: SAC 2012, 27-th ACM Symposium On Applied Computing, Mar 2012, Trento, Italy. ACM, Proceedings of the 27th Annual ACM Symposium on Applied Computing, pp. 1284-1291
Accès au bibtex

Titre: A Rule-Based Framework for Building Superposition-Based Decision Procedures
Auteurs: Elena Tushkanova; Alain Giorgetti; Christophe Ringeissen; Olga Kouchnarenko
Détail: Franciso Durán. Rewriting Logic and Its Applications, Mar 2012, Tallinn, Estonia. Springer Berlin / Heidelberg, Rewriting Logic and Its Applications 9th International Workshop, WRLA 2012, Held as a Satellite Event of ETAPS, Tallinn, Estonia, March 24-25, 2012, Revised Selected Papers, 7571, pp. 221-239, Lecture Notes in Computer Science
Accès au bibtex

Titre: Grammar-Based Testing using Realistic Domains in PHP
Auteurs: Ivan Enderlin; Frédéric Dadeau; Alain Giorgetti; Fabrice Bouquet
Détail: IEEE Fifth International Conference on Software Testing, Verification and Validation (ICST), 2012, Apr 2012, Montreal, Canada. IEEE Computer Society, IEEE Fifth International Conference on Software Testing, Verification and Validation (ICST), 2012, , pp. 509-518
Accès au bibtex

Titre: Rewriting Strategies for a Two-Scale Method: Application to Combined Thin and Periodic Structures
Auteurs: B. Yang; W. Belkhir; R.N. Dhara; A. Giorgetti; M. Lenczner
Détail: d Software Implementation for Distributed MEMS - dMEMS 2012, Apr 2012, Besançon, France. IEEE Computer Society, Second Workshop on Design, Control and Software Implementation for Distributed MEMS - dMEMS 2012, , pp. 82-89
Accès au bibtex

Titre: Specification and Validation of Algorithms Generating Planar Lehman Words
Auteurs: Alain Giorgetti; Valerio Senni
Détail: GASCom 2012 - 8th International Conference on random generation of combinatorial structures, Jun 2012, Bordeaux, France.
Accès au bibtex

Titre: Lazy AC-Pattern Matching for Rewriting
Auteurs: Walid Belkhir; Alain Giorgetti
Détail: Santiago Escobar. 10th International Workshop on Reduction Strategies in Rewriting and Programming, May 2011, Novi Sad, Serbia. Proceedings 10th International Workshop on Reduction Strategies in Rewriting and Programming, 82, pp. 37-51, 2012
Accès au bibtex

Titre: On Positive TAGED with a Bounded Number of Constraints
Auteurs: Pierre-Cyrille Heam ; Vincent Hugot; Olga Kouchnarenko
Détail: CIAA - 17th International Conference on Implementation and Application of Automata 2012, Jul 2012, Porto, Portugal. Springer, 7381, pp. 329-336, Lecture Notes in Computer Science
Accès au bibtex

Titre: From Linear Temporal Logic Properties to Rewrite Propositions
Auteurs: Pierre-Cyrille Heam ; Vincent Hugot; Olga Kouchnarenko
Détail: IJCAR - International Joint Conference on Automated Reasonning 2012, Jun 2012, Manchester, United Kingdom. Springer, Automated Reasoning, 7364, pp. 316-331, Lecture Notes in Computer Science
Accès au bibtex

Titre: The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures
Auteurs: Alessandro Armando; Wihem Arsac; Tigran Avanesov; Michele Barletta; Alberto Calvi; Alessandro Cappai; Roberto Carbone; Yannick Chevalier; Luca Compagna; Jorge Cuellar; Gabriel Erzse; Simone Frau; Marius Minea; Sebastian Modersheim; David Von Oheimb; Giancarlo Pellegrino; Serena Elisa Ponta; Marco Rocchetto; Michaël Rusinowitch; Mohammad Torabi Dashti; Mathieu Turuani; Luca Vigano
Détail: Cormac Flanagan and Barbara Konig. Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Mar 2012, Tallinn, Estonia. Springer, 7214, pp. 267-282, Lecture Notes in Computer Science
Accès au bibtex

Rapports

Titre: Automatic Decidability for Theories Modulo Integer Offsets
Auteurs: Elena Tushkanova; Christophe Ringeissen ; Alain Giorgetti; Olga Kouchnarenko
Détail: [Research Report], 2012, pp. 20. RR-8139
Accès au texte intégral et bibtex

Titre: On the Polling Problem for Social Networks
Auteurs: Hoang Bao Thien; Abdessamad Imine
Détail: [Research Report], 2012. RR-8055
Accès au texte intégral et bibtex

Titre: Revoke and Let Live: A Secure Key Revocation API for Cryptographic Devices
Auteurs: Véronique Cortier; Graham Steel; Cyrille Wiedling
Détail: [Research Report], 2012, pp. 41. RR-7949
Accès au texte intégral et bibtex

Titre: Intruder deducibility constraints with negation. Decidability and application to secured service compositions.
Auteurs: Tigran Avanesov; Yannick Chevalier; Michaël Rusinowitch; Mathieu Turuani
Détail: [Research Report], 2012. RR-8017
Accès au texte intégral et bibtex

Titre: Automated Synthesis of a Finite Complexity Ordering for Saturation
Auteurs: Yannick Chevalier; Mounira Kourjieh
Détail: [Research Report], 2012
Accès au texte intégral et bibtex

Titre: A General Approach for Securely Querying and Updating XML Data
Auteurs: Houari Mahfoud; Abdessamad Imine
Détail: [Research Report], 2012, pp. 23. RR-7870
Accès au texte intégral et bibtex

Documents sans référence de publication

Titre: Rewrite Closure and CF Hedge Automata
Auteurs: Florent Jacquemard; Michaël Rusinowitch
Détail: Nov. 2012
Accès au texte intégral et bibtex

Titre: Universally Composable Key-Management
Auteurs: Steve Kremer ; Robert Kunnemann ; Graham Steel
Détail: Apr. 2012. This is the full version of the paper.
Accès au texte intégral et bibtex

2011

Articles dans des revues avec comité de lecture

Titre: Scenario-based testing from UML/OCL behavioral models Application to POSIX compliance
Auteurs: Kalou Cabrera Castillos; Frédéric Dadeau; Jacques Julliand
Détail: International Journal on Software Tools for Technology Transfer, Springer-Verlag, 2011, VSTTE 2009, 13 (5), pp. 431-448
Accès au bibtex

Titre: On the Complexity of Computing the Profinite Closure of a Rational Language
Auteurs: Pierre-Cyrille Heam
Détail: Theoretical Computer Science, Elsevier, 2011, 412 (41), pp. 5808-5813
Accès au texte intégral et bibtex

Titre: A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems.
Auteurs: Véronique Cortier; Steve Kremer; Bogdan Warinschi
Détail: Journal of Automated Reasoning, Springer-Verlag, 2011, 46 (3-4), pp. 225-259
Accès au bibtex

Titre: Automatic Decidability and Combinability
Auteurs: Christopher Lynch; Silvio Ranise; Christophe Ringeissen; Duc-Khanh Tran
Détail: Information and Computation, Elsevier, 2011, 209 (7), pp. 1026-1047
Accès au bibtex

Titre: Deciding knowledge in security protocols under some e-voting theories
Auteurs: Mouhebeddine Berrima; Narjes Ben Rajeb; Véronique Cortier
Détail: RAIRO - Theoretical Informatics and Applications, EDP Sciences, 2011, 45 (3), pp. 269-299
Accès au bibtex

Communications avec actes

Titre: Combining Proof and Model-checking to Validate Reconfigurable Architectures
Auteurs: Arnaud Lanoix; Julien Dormoy; Olga Kouchnarenko
Détail: 8th International Workshop on Formal Engineering approaches to Software Components and Architectures - FESCA 2011, joint to ETAPS 2011, Apr 2011, Saarbrucken, Germany. 279(2), pp. 43-57, Electr. Notes Theor. Comput. Sci.
Accès au bibtex

Titre: Orchestration under Security Constraints
Auteurs: Yannick Chevalier; Mohammed Anis Mekki; Michael Rusinowitch
Détail: Bernhard K Aichernig and Frank S. de Boer and Marcello M. Bonsangue. Formal Methods for Components and Objects (FMCO 2010), Nov 2010, Graz, Austria. Springer, Formal Methods for Components and Objects, 6957, 2011, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: Praspel: A Specification Language for Contract-Based Testing in PHP
Auteurs: Ivan Enderlin; Frédéric Dadeau; Alain Giorgetti; Abdallah Ben Othman
Détail: Burkhartt Wolff and Fatiha Zaidi. 23rd IFIP International Conference on Testing Software and Systems (ICTSS'11), Nov 2011, Paris, France. Springer-Verlag, Testing Software and Systems, 7019, pp. 64-79, Lecture Notes in Computer Science
Accès au bibtex

Titre: Measuring Test Properties Coverage for evaluating UML/OCL Model-Based Tests
Auteurs: Kalou Cabrera Castillos; Frédéric Dadeau; Jacques Julliand; Safouan Taha
Détail: Burkhartt Wolff and Fatiha Zaidi. 23rd IFIP International Conference on Testing Software and Systems, Nov 2011, Paris, France. Springer-Verlag, Testing Software and Systems, 7019, pp. 32-47, Lecture Notes in Computer Science
Accès au bibtex

Titre: Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components
Auteurs: Julien Dormoy; Olga Kouchnarenko ; Arnaud Lanoix
Détail: 8th International Symposium on Formal Aspects of Component Software - FACS 2011, Sep 2011, Oslo, Norway. Springer, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: UML/OCL based impact analysis to test evolving critical software
Auteurs: Elizabeta Fourneret; Fabrice Bouquet
Détail: 10th International Conference Society for Electronics, Telecommunications, Automatics and Informatics - ETAI'11, Sep 2011, Ohrid, Macedonia, The Former Yugoslav Republic Of.
Accès au bibtex

Titre: DeSCal --- Decentralized Shared Calendar for P2P and Ad-Hoc Networks
Auteurs: Jagdish Prasad Achara; Abdessamad Imine ; Michaël Rusinowitch
Détail: The 10th International Symposium on Parallel and Distributed Computing - ISPDC 2011, Jul 2011, Cluj-Napoca, Romania. IEEE
Accès au bibtex

Titre: Grey-Box Testing and Verification of Java/JML
Auteurs: Frédéric Dadeau; Fabien Peureux
Détail: Arnaud Gotlieb and Gordon Fraser. 3rd International Workshop on Constraints in Software Testing Verification and Analysis, Mar 2011, Berlin, Germany. IEEE Computer Society Press, Software Testing, Verification and Validation Workshops (ICSTW), pp. 298-303
Accès au bibtex

Titre: Scenario Based Test Generation Using Test Designer
Auteurs: Kalou Cabrera Castillos; Julien Botella
Détail: Frederic Dadeau and Lydie du Bousquet. 1st International Workshop on Scenario-Based Testing (SCENARIOS'2011), Mar 2011, Berlin, Germany. IEEE Computer Society Press, Software Testing, Verification and Validation Workshops (ICSTW), pp. 79-88
Accès au bibtex

Titre: Selective Test Generation Method for Evolving Critical Systems
Auteurs: Elizabeta Fourneret; Fabrice Bouquet; Frédéric Dadeau; Stéphane Debricon
Détail: Per Runeson and Shin Yoo. 1st International Workshop on Regression Testing, Mar 2011, Berlin, Germany. IEEE Computer Society Press, Software Testing, Verification and Validation Workshops (ICSTW), pp. 125 - 134
Accès au bibtex

Titre: The SANTE Tool: Value Analysis, Program Slicing and Test Generation for C Program Debugging
Auteurs: Omar Chebaro; Nikolai Kosmatov; Alain Giorgetti; Jacques Julliand
Détail: Martin Gogolla and Burkhart Wolff. 5th International Conference on Tests & Proofs, Jun 2011, Zurich, Switzerland. Springer Verlag, Tests and Proofs 5th International Conference, TAP 2011, 6706, pp. 78-83, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: Comparative behaviour of recent incremental and non-incremental clustering methods on text: an extended study
Auteurs: Jean-Charles Lamirel; Raghvendra Mall; M. Ahmad
Détail: The Twenty-fourth International Conference on Industrial, Engineering and Other Applications of Applied Intelligent Systems (IEA/AIE 2011), Jun 2011, Syracuse, United States.
Accès au bibtex

Titre: Mutation-Based Test Generation from Security Protocols in HLPSL
Auteurs: Frédéric Dadeau; Pierre-Cyrille Héam; Rafik Kheddam
Détail: Harman, Mark and Korel, Bodgan. 4th International Conference on Software Testing Verification and Validation (ICST'2011), Mar 2011, Berlin, Germany. IEEE Computer Society Press, ICST 2011, 4th Int. Conf. on Software Testing, Verification and Validation
Accès au bibtex

Titre: Using Temporal Logic for Dynamic Reconfigurations of Components
Auteurs: Julien Dormoy; Olga Kouchnarenko; Arnaud Lanoix
Détail: 7th International Workshop on Formal Aspects of Component Software - FACS'2010, Oct 2010, Guimaraes, Portugal. 2011
Accès au texte intégral et bibtex

Titre: Comportement comparatif des méthodes de clustering incrémentales et non incrémentales sur les données textuelles hétérogènes
Auteurs: Jean-Charles Lamirel; Raghvendra Mall; M. Ahmad
Détail: 11th International Francophone Conference on Knowledge Extraction and Management (EGC 2011), Jan 2011, Brest, France.
Accès au bibtex

Titre: How to prove security of communication protocols? A discussion on the soundness of formal models w.r.t. computational ones.
Auteurs: Hubert Comon-Lundh; Véronique Cortier
Détail: Symposium on Theoretical Aspects of Computer Science - STACS2011, Mar 2011, Dortmund, Germany. 9, pp. 29-44
Accès au texte intégral et bibtex

Titre: Seed, an Easy-to-Use Random Generator of Recursive Data Structures for Testing
Auteurs: Pierre-Cyrille Héam; Cyril Nicaud
Détail: 4th IEEE International Conference on Software Testing, Verification and Validation (ICST'11), Mar 2011, Berlin, Germany. IEEE, pp. 60 - 69
Accès au bibtex

Titre: Loops and Overloops for Tree Walking Automata
Auteurs: Pierre-Cyrille Heam ; Vincent Hugot; Olga Kouchnarenko
Détail: Béatrice Bouchou-Markhoff and Pascal Caron and Jean-Marc Champarnaud and Denis Maurel. 16th International Conference on Implementation and Application of Automata - CIAA 2011, Jul 2011, Blois, France. Springer, Implementation and Application of Automata, 6807, pp. 166-177, Lecture Notes in Computer Science
Accès au bibtex

Titre: A Random Testing Approach Using Pushdown Automata
Auteurs: Pierre-Cyrille Heam ; Catherine Masson
Détail: Martin Gogolla and Burkhart Wolff. 5th International Conference on Tests and Proofs - TAP 2011, Jun 2011, Zurich, Switzerland. Springer, Tests and Proofs, 6706, pp. 119-133, Lecture Notes in Computer Science
Accès au bibtex

Titre: Lazy Rewriting Modulo Associativity and Commutativity
Auteurs: Walid Belkhir; Alain Giorgetti
Détail: WRS 2011, 10-th Int. workshop on Reduction Strategies in Rewriting and Programming, May 2011, Novi Sad, Serbia. pp. 17-21
Accès au bibtex

Titre: Simulations over Two-Dimensional On-Line Tessellation Automata
Auteurs: Gérard Cécé; Alain Giorgetti
Détail: Mauri, Giancarlo and Leporati, Alberto. 15th International Conference on Developments in Language Theory - DLT 2011, Jul 2011, Milan, Italy. Springer, Developments in Language Theory, 6795, pp. 141-152, Lecture Notes in Computer Science
Accès au bibtex

Titre: Model-Based Security Verification and Testing for Smart-cards
Auteurs: Elizabeta Fourneret; Martin Ochoa; Fabrice Bouquet; Julien Botella; Jan Jürjens; Parvaneh Yousefi
Détail: 6th International Conference on Availability, Reliability and Security - ARES 2011, Aug 2011, Vienna, Austria. IEEE, 2011 Sixth International Conference on Availability, Reliability and Security (ARES), pp. 272 - 279
Accès au bibtex

Titre: Development of an automated MBT toolchain from UML/SysML models
Auteurs: Jonathan Lasalle; Fabien Peureux; Frédéric Fondement
Détail: 4th IEEE Int. Workshop on UML and Formal Methods - UML&FM'2011, Jun 2011, Limerick, Ireland, Ireland. Springer, Special issue: Unified Modeling Language and Formal Methods 2011, 7 n°4, pp. 247-256, Innovations in Systems and Software Engineering
Accès au bibtex

Titre: Automatic test concretization to supply end-to-end MBT for automotive mecatronic systems
Auteurs: Jonathan Lasalle; Fabien Peureux; Jérôme Guillet
Détail: 1st International Workshop on End-to-End Test Script Engineering - ETSE 2011, Jul 2011, Toronto, Canada, Canada. ACM, pp. 16-23
Accès au bibtex

Titre: Optimistic access control for distributed collaborative editors
Auteurs: Asma Cherif; Abdessamad Imine; Michaël Rusinowitch
Détail: 2011 ACM Symposium on Applied Computing (SAC), Mar 2011, Taichung, Taiwan, Province Of China. ACM, Proceedings of the 2011 ACM Symposium on Applied Computing, pp. 861-868
Accès au bibtex

Titre: Ballot stuffing in a postal voting system
Auteurs: Véronique Cortier; Jérémie Detrey; Pierrick Gaudry; Frédéric Sur; Emmanuel Thomé; Mathieu Turuani; Paul Zimmermann
Détail: Revote 2011 - International Workshop on Requirements Engineering for Electronic Voting Systems, 2011, Trento, Italy. IEEE, pp. 27 - 36
Accès au texte intégral et bibtex

Titre: Modular Termination and Combinability for Superposition Modulo Counter Arithmetic
Auteurs: Christophe Ringeissen; Valerio Senni
Détail: Cesare Tinelli and Viorica Sofronie-Stokkermans. Frontiers of Combining Systems, 8th International Symposium, FroCoS'2011, Oct 2011, Saarbruecken, Germany. Springer, Frontiers of Combining Systems, 6989, pp. 211-226, Lecture Notes in Artificial Intelligence
Accès au bibtex

Titre: Transforming Password Protocols to Compose
Auteurs: Céline Chevalier; Stéphanie Delaune; Steve Kremer
Détail: 31st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'11), Dec 2011, Mumbai, India.
Accès au bibtex

Titre: A Composable Computational Soundness Notion
Auteurs: Véronique Cortier; Bogdan Warinschi
Détail: 18th ACM Conference on Computer and Communications Security - CSS 2011, Oct 2011, Chicago, United States. ACM, pp. 63-74
Accès au bibtex

Titre: Adapting Helios for provable ballot secrecy
Auteurs: David Bernhard; Véronique Cortier; Olivier Pereira; Ben Smyth; Bogdan Warinschi
Détail: Vijay Atluri and Claudia Diaz. 16th European Symposium on Research in Computer Security (ESORICS'11), Sep 2011, Louvain, Belgium. Springer Verlag, Proceedings of the 16th European Symposium on Research in Computer Security, Leuven, Belgium, September 12-14,2011, 6879, pp. 335-354, Lecture Notes in Computer Science
Accès au bibtex

Titre: Attacking and fixing Helios: An analysis of ballot secrecy
Auteurs: Véronique Cortier; Ben Smyth
Détail: 24th IEEE Computer Security Foundations Symposium (CSF'11), Jun 2011, Cernay-la-Ville, France. IEEE Computer Society Press, pp. 297 - 311
Accès au bibtex

Titre: Deciding security for protocols with recursive tests
Auteurs: Mathilde Arnaud; Véronique Cortier; Stéphanie Delaune
Détail: Bj\orner, Nikolaj and Sofronie-Stokkermans, Viorica. 23rd International Conference on Automated Deduction (CADE'11), Aug 2011, Wroclaw, Poland. Springer, pp. 49-63
Accès au bibtex

Titre: A composable computational soundness notion (Abstract)
Auteurs: Véronique Cortier; Bogdan Warinschi
Détail: 7th Workshop on Formal and Computational Cryptography (FCC 2011), Jun 2011, Paris, France.
Accès au bibtex

Conférences invitées

Titre: Orchestrating Security and System Engineering for Evolving Systems
Auteurs: Fabio Massacci; Fabrice Bouquet; Elizabeta Fourneret; Jan Jurjens; Mass Lund; Sébastien Madelénat; JanTobias Muehlberg; Federica Paci; Stéphane Paul; Frank Piessens; Bjornar Solhaug; Sven Wenzel
Détail: Witold Abramowicz and Ignacio M. Llorente and Mike Surridge and Andrea Zisman and Julien Vayssière. 4th European Conference, Towards a Service-Based Internet - ServiceWave 2011, Oct 2011, Poznan, Poland. Springer, Towards a Service-Based Internet, 6994, pp. 134-143, Lecture Notes in Computer Science
Accès au bibtex

Chapitres d'ouvrages scientifiques

Titre: Test Generation using Symbolic Animation of Models
Auteurs: Frédéric Dadeau; Fabien Peureux; Bruno Legeard; Régis Tissot; Jacques Julliand; Pierre-Alain Masson; Fabrice Bouquet
Détail: Zander, Justyna and Schieferdecker, Ina and Mosterman, Pieter J.. Model-Based Testing for Embedded Systems, CRC Press, Sep. 2011, Series on Computational Analysis, Synthesis, Design of Dynamic Systems, 978-1-4398184-5-9
Accès au bibtex

Directions d'ouvrages

Titre: Proceedings of the 8th International Workshop on Security Issues in Concurrency
Auteurs: Konstantinos Chatzikokolakis; Véronique Cortier
Détail: Konstantinos Chatzikokolakis and Véronique Cortier. 51, Electronic Proceedings in Theoretical Computer Science, pp. 51, 2011, Electronic Proceedings in Theoretical Computer Science
Accès au bibtex

HDR

Titre: Déduction automatique appliquée à l'analyse et la vérification de systèmes infinis
Auteurs: Laurent Vigneron
Détail: Université Nancy II, Nov. 2011. French
Accès au texte intégral et bibtex

Autres publications

Titre: From Linear Temporal Logic Properties to Rewrite Propositions
Auteurs: Pierre-Cyrille Heam; Vincent Hugot; Olga Kouchnarenko
Détail: Oct. 2011. Work document
Accès au bibtex

Ouvrages scientifiques

Titre: Industrialiser le test fonctionnel Pour maîtriser les risques métier et accroître l'efficacité du test
Auteurs: Fabrice Bouquet ; Bruno Legeard; Natacha Pickaert
Détail: DUNOD, pp. 304, Nov. 2011, 9782100566563
Accès au bibtex

Titre: Formal Models and Techniques for Analyzing Security Protocols
Auteurs: Véronique Cortier; Steve Kremer
Détail: 5. Cortier, Véronique and Kremer, Steve. IOS Press, pp. 312, 2011, Cryptology and Information Security Series, 978-1-60750-713-0
Accès au bibtex

Rapports

Titre: Secure Querying of Recursive XML Views: A Standard XPath-based Technique
Auteurs: Houari Mahfoud; Abdessamad Imine
Détail: [Research Report], 2011, pp. 30. RR-7834
Accès au texte intégral et bibtex

Titre: On the Undoability Problem in Distributed Collaborative Applications
Auteurs: Asma Cherif; Abdessamad Imine
Détail: [Research Report], 2011, pp. 30
Accès au bibtex

Titre: A formal analysis of the Norwegian e-voting protocol
Auteurs: Véronique Cortier; Cyrille Wiedling
Détail: [Research Report], 2011. RR-7781
Accès au texte intégral et bibtex

Titre: Automated verification of equivalence properties of cryptographic protocols
Auteurs: Rohit Chadha; Stefan Ciobaca; Steve Kremer
Détail: [Research Report], 2011
Accès au texte intégral et bibtex

Titre: Unification modulo Block Chaining
Auteurs: Siva Anantharaman; Christopher Bouchard; Paliath Narendran; Michael Rusinowitch
Détail: [Research Report], 2011
Accès au bibtex

Titre: A note on replay attacks that violate privacy in electronic voting schemes
Auteurs: Ben Smyth; Véronique Cortier
Détail: [Research Report], 2011. RR-7643
Accès au texte intégral et bibtex

Thèses

Titre: Stratégies d'optimisation de la mémoire pour le calcul d'applications linéaires et l'indexation de document partagés
Auteurs: Mumtaz Ahmad
Détail: mathématiques et informatique. Université Henri Poincaré - Nancy I, Nov. 2011. English
Accès au texte intégral et bibtex

Titre: Résolution de contraintes de déductibilité. Application à la composition de services Web sécurisés
Auteurs: Tigran Avanesov
Détail: informatique. Université Henri Poincaré - Nancy I, Sep. 2011. English
Accès au texte intégral et bibtex

Titre: Contributions à l'analyse de systèmes par approximation d'ensembles réguliers
Auteurs: Roméo Courbis
Détail: informatique. Université de Franche-Comté, Sep. 2011. French
Accès au texte intégral et bibtex

Documents sans référence de publication

Titre: Rewriting and Symbolic Transformations for Multiscale Methods
Auteurs: Walid Belkhir; Alain Giorgetti; Michel Lenczner
Détail: Jan. 2011. 25 pages
Accès au bibtex

2010

Articles dans des revues avec comité de lecture

Titre: Combination of Convex Theories: Modularity, Deduction Completeness, and Explanation
Auteurs: Duc-Khanh Tran; Christophe Ringeissen; Silvio Ranise; Hélène Kirchner
Détail: Journal of Symbolic Computation, Elsevier, 2010, Automated Deduction: Decidability, Complexity, Tractability, 45 (2), pp. 261-286
Accès au bibtex

Titre: Formal Verification of Secure Group Communications Using AVISPA and TURTLE
Auteurs: Pierre De Saqui-Sannes; Thierry Villemur; Benjamin Fontan; Sara Mota; Mohamed Salah Bouassida; Najah Chridi; Isabelle Chrisment; Laurent Vigneron
Détail: The Innovations in Systems and Software Engineering journal, 2010
Accès au bibtex

Titre: Composition of Services with Constraints
Auteurs: Fahima Cheikh; Pierre-Cyrille Héam; Olga Kouchnarenko
Détail: Electronic Notes in Theoretical Computer Science, 2010, 236 (Special Issue, selected papers of FACS'09), pp. 31-46
Accès au texte intégral et bibtex

Titre: Parametric Random Generation of Deterministic Tree Automata
Auteurs: Pierre-Cyrille Heam; Cyril Nicaud; Sylvain Schmitz
Détail: Theoretical Computer Science, 2010, 411 (1), pp. 3469-3480
Accès au texte intégral et bibtex

Titre: Component Simulation-based Substitutivity Managing QoS and Composition Issues
Auteurs: Pierre-Cyrille Héam; Olga Kouchnarenko; Jérôme Voinot
Détail: Electronic Notes in Theoretical Computer Science, 2010, 260, pp. 109-123
Accès au texte intégral et bibtex

Titre: Design and Verification of a Non-repudiation Protocol Based on Receiver-Side Smart Card
Auteurs: Liu Jing; Laurent Vigneron
Détail: IET Information Security, IET, 2010, 4 (1), pp. 15-29
Accès au bibtex

Titre: Symbolic Protocol Analysis in the Union of Disjoint Intruder Theories: Combining Decision Procedures
Auteurs: Yannick Chevalier; Michael Rusinowitch
Détail: Theoretical Computer Science, Elsevier, 2010, 411 (10), pp. 1261-1282
Accès au bibtex

Titre: Component Simulation-based Substitutivity Managing QoS and Composition Issues
Auteurs: Pierre-Cyrille Heam; Olga Kouchnarenko; Jérôme Voinot
Détail: Science of Computer Programming, Elsevier, 2010, 75 (10), pp. 898-917
Accès au bibtex

Titre: Deciding security properties for cryptographic protocols. Application to key cycles.
Auteurs: Hubert Comon-Lundh; Véronique Cortier; Eugen Zalinescu
Détail: ACM Transactions on Computational Logic, ACM Digital Library, 2010, 11 (2), pp. Article 9
Accès au bibtex

Titre: Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator
Auteurs: Enrica Nicolini; Christophe Ringeissen; Michael Rusinowitch
Détail: Fundamenta Informaticae, IOS Press, 2010, 105 (1-2), pp. 163-187
Accès au bibtex

Titre: Decidability of Equivalence of Symbolic Derivations
Auteurs: Yannick Chevalier; Michael Rusinowitch
Détail: Journal of Automated Reasoning, Springer, 2010, 45 (2), pp. 1-30
Accès au bibtex

Titre: Compiling and securing cryptographic protocols
Auteurs: Yannick Chevalier; Michael Rusinowitch
Détail: Information Processing Letters, Elsevier, 2010, 110 (3), pp. 116–122
Accès au bibtex

Titre: Efficient Decision Tree for Protocol Analysis in Intrusion Detection
Auteurs: Tarek Abbes; Adel Bouhoula; Michael Rusinowitch
Détail: International Journal of Security and Networks, Inderscience Enterprises Ltd;, 2010, 5 (4), pp. 220-235
Accès au bibtex

Titre: An Access Control Model Based Testing Approach for Smart Card Applications: Results of the POSÉ Project
Auteurs: Pierre-Alain Masson; Marie-Laure Potet; Jacques Julliand; Régis Tissot; Fabrice Bouquet; Bruno Legeard; Eddie Jaffuel; Boutheina Chetali; June Andronick; Amal Haddad
Détail: Journal of Information Assurance and Security, MIR Labs, 2010, 5 (1), pp. 335-351
Accès au bibtex

Titre: VETESS : IDM, Test et SysML
Auteurs: Frédéric Fondement; P-A. Muller; Brice Wittmann; Fabrice Ambert; Fabrice Bouquet; Jonathan Lasalle; Emilie Oudot; Fabien Peureux; Bruno Legeard; M. Alter; C. Scherrer
Détail: Génie logiciel, GL& IS, 2010, 93, pp. 43-48
Accès au bibtex

Titre: A Decidability Result for the Model Checking of Infinite-State Systems
Auteurs: Daniele Zucchelli; Enrica Nicolini
Détail: Journal of Automated Reasoning, Springer, 2010, (Online)
Accès au bibtex

Titre: Formal Verification of Secure Group Communication Protocols Modelled in UML
Auteurs: Pierre Saqui-Sannes; Thierry Villemur; Benjamin Fontan; Sara Mota; Mohamed Salah Bouassida; Najah Chridi; Isabelle Chrisment; Laurent Vigneron
Détail: Innovations in Systems and Software Engineering, Springer, 2010, Special Issue ICFEM'09, 6 (1-2), pp. 125-133
Accès au bibtex

Communications avec actes

Titre: Symbolic Model-Checking of Optimistic Replication Algorithms
Auteurs: Hanifa Boucheneb; Abdessamad Imine; Manal Najem
Détail: Mery, Dominique and Merz, Stephan. 8th International Conference on Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, Integrated Formal Methods, 6396, pp. 89-104, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: Log Garbage Collector-based Real Time Collaborative Editor for Mobile Devices
Auteurs: Moulay Driss Mechaoui; Asma Cherif; Abdessamad Imine; Fatima Bendella
Détail: 6th International Conference on Collaborative Computing: Networking, Applications and Worksharing (CollaborateCom 2010), Oct 2010, Chicago, United States.
Accès au bibtex

Titre: On Coordinating Collaborative Objects
Auteurs: Abdessamad Imine
Détail: Mohammad Reza Mousavi and Gwen Salaün. 9th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA), Sep 2010, Paris, France. Open Publishing Association, Proceedings Ninth International Workshop on the Foundations of Coordination Languages and Software Architectures, 30, pp. 78-92, Electronic Proceedings in Theoretical Computer Science
Accès au bibtex

Titre: Assessing the Quality of B Models
Auteurs: Adrien De Kermadec; Frédéric Dadeau; Fabrice Bouquet
Détail: Maggiolo-Schettini, Andrea and Fiadeiro, José Luis and Gnesi, Stefania. SEFM'10 - 8th IEEE International Conference on Software Engineering and Formal Methods, Sep 2010, Pisa, Italy. Proceedings Software Engineering and Formal Methods - SEFM 2010, IEEE computer society
Accès au bibtex

Titre: Safe and Efficient Strategies for Updating Firewall Policies
Auteurs: Zeeshan Ahmed; Abdessamad Imine; Michael Rusinowitch
Détail: Sokratis K. Katsikas and Javier Lopez and Miguel Soriano. 7th International Conference on Trust, Privacy & Security in Digital Business - TrustBus 2010, Aug 2010, Bilbao, Spain. Springer, Trust, Privacy and Security in Digital Business, 6264, pp. 45-57, Lecture Notes of Computer Science
Accès au bibtex

Titre: Building a Test-ready Abstraction of a Behavioral Model using CLP
Auteurs: Pierre-Christophe Bué; Frédéric Dadeau; Adrien De Kermadec; Fabrice Bouquet
Détail: Fraser, Gordon and Gargantini, Angelo. 4th International Conference on Tests and Proofs - TAP 2010, Jul 2010, Malaga, Spain. Springer-Verlag, Tests and Proofs, 6143, pp. 167-182, Lecture Notes in Computer Science
Accès au bibtex

Titre: Approximations par réécriture pour deux problèmes indécidables
Auteurs: Roméo Courbis; Pierre-Cyrille Heam; Pierre Jourdan; Olga Kouchnarenko
Détail: Yamine Aït-Ameur. AFADL, Jun 2010, Poitiers, France. 10, pp. 7
Accès au texte intégral et bibtex

Titre: Une approche parallèle et distribuée pour la complétion d'automates d'arbre
Auteurs: Adrian Caciula; Roméo Courbis; Violeta Felea; Pierre-Cyrille Heam; Rasvan Ionescu
Détail: Yamine Aït-Ameur. 10es Journées Francophones Internationales sur les Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL 2010, Jun 2010, Poitiers, France. 10, pp. 43
Accès au texte intégral et bibtex

Titre: Cap Unification: Application to Protocol Security modulo Homomorphic Encryption
Auteurs: Siva Anantharaman; Hai Lin; Christopher Lynch; Paliath Narendran; Michael Rusinowitch
Détail: David Basin, Peng Liu. 5th ACM Symposium on Information, Computer and Communications Security - ASIACCS 2010, Apr 2010, Beijing, China. ACM
Accès au bibtex

Titre: Model-Based Testing using Symbolic Animation and Machine Learning
Auteurs: Pierre-Christophe Bué; Frédéric Dadeau; Pierre-Cyrille Héam
Détail: Fraser, Gordon and Gotlieb, Arnaud and Michel, Claude and Pretschner, Alexander. 2nd Workshop on Constraints in Software Testing, Verification, and Analysis - CSTVA'2010, Apr 2010, Paris, France. IEEE Press, Software Testing, Verification, and Validation Workshops (ICSTW), 2010 Third International Conference on Software Testing, Verification, and Validation
Accès au bibtex

Titre: Component Simulation-based Substitutivity Managing QoS Aspects
Auteurs: Pierre-Cyrille Heam; Olga Kouchnarenko; Jérôme Voinot
Détail: Carlos Canal and Corina Pasareanu. Formal Aspects On Component Softwre - FACS'08, Sep 2008, Malaga, Spain. 260 (2010), pp. 109-123, 2010, Electr. Notes Theor. Comput. Sci.
Accès au bibtex

Titre: Composition of services with constraints
Auteurs: Philippe Balbiani; Fahima Cheikh; Pierre-Cyrille Heam; Olga Kouchnarenko
Détail: Formal Aspects of Component Software, Nov 2009, Eindhoven, Netherlands. 263, pp. 31-46, 2010, Electronic Notes in Theoretical Computer Science
Accès au bibtex

Titre: Combining Static Analysis and Test Generation for {C} Program Debugging
Auteurs: Omar Chebaro; Nikolaï Kosmatov; Alain Giorgetti; Jacques Julliand
Détail: TAP'10, 4th Int. Conf. on Tests and Proofs, 2010, Spain. pp. 94-100
Accès au texte intégral et bibtex

Titre: {SAT} Solvers for Queries over Tree Automata with Constraints
Auteurs: Pierre-Cyrille Héam; Vincent Hugot; Olga Kouchnarenko
Détail: CSTVA'10, 2nd Int. Workshop on Constraints in Software Testing Verification and Analysis - co-located with ICST'2010, 2010, France. pp. ***-***
Accès au texte intégral et bibtex

Titre: Associer des techniques de preuve et de résolution de contraintes pour la construction d'abstractions
Auteurs: Pierre-Christophe Bué; Jacques Julliand; Pierre-Alain Masson; Fabrice Bouquet
Détail: 10èmes Journées Francophones Internationales sur les Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'10, Jun 2010, Poitiers, France. pp. 11-25
Accès au texte intégral et bibtex

Titre: Guessing a Conjecture in Enumerative Combinatorics and Proving It with a Computer Algebra System
Auteurs: Alain Giorgetti
Détail: T. Jebelean and M. Mosbah and N. Popov. Symbolic Computation in Software Science, Jul 2010, Linz, Austria. pp. 5-18
Accès au texte intégral et bibtex

Titre: Modeling and Verifying Ad Hoc Routing Protocols.
Auteurs: Mathilde Arnaud; Véronique Cortier; Stéphanie Delaune
Détail: 23rd IEEE Computer Security Foundations Symposium - CSF'10, 2010, Edinburgh, United Kingdom.
Accès au bibtex

Titre: Protocol composition for arbitrary primitives.
Auteurs: Stefan Ciobaca; Véronique Cortier
Détail: 23rd IEEE Computer Security Foundations Symposium - CSF'10, 2010, Edinburgh, United Kingdom. pp. 322-336
Accès au bibtex

Titre: Specifying Generic Java Programs: two case studies
Auteurs: Alain Giorgetti; Claude Marché; Elena Tushkanova; Olga Kouchnarenko
Détail: 11th International Workshop on Language Descriptions, Tools, and Applications - LDTA'2010, Mar 2010, Paphos, Cyprus. pp. 92-106
Accès au texte intégral et bibtex

Titre: Using SysML for Smart Surface Modeling
Auteurs: Alain Giorgetti; Ahmed Hammad; Bruno Tatibouët
Détail: dMEMS'10, 1st workshop on design, control and software implementation for distributed MEMS, Jun 2010, Besançon, France. IEEE, pp. 100-107
Accès au texte intégral et bibtex

Titre: Satisfiability of General Intruder Constraints with a Set Constructor
Auteurs: Tigran Avanesov; Yannick Chevalier; Michael Rusinowitch; Mathieu Turuani
Détail: The Fifth International Conference on Risks and Security of Internet and Systems - CRiSIS 2010, Oct 2010, Montreal, Canada.
Accès au bibtex

Titre: Test Generation Based on Abstraction and Test Purposes to Complement Structural Tests
Auteurs: Fabrice Bouquet; Pierre-Christophe Bué; Jacques Julliand; Pierre-Alain Masson
Détail: A-MOST'10, 6th int. Workshop on Advances in Model Based Testing, in conjunction with ICST'10, Apr 2010, Paris, France. pp. 54-61
Accès au bibtex

Titre: XML Access Control: from XACML to Annotated Schemas
Auteurs: Ryma Abassi; Florent Jacquemard; Michael Rusinowitch; Sihem Guemara El Fatmi
Détail: Second International Conference on Communications and Networking (ComNet), Nov 2010, Tozeur, Tunisia. IEEE Computer Society Press, pp. 1-8
Accès au bibtex

Titre: Rewrite-Based Verification of XML Updates
Auteurs: Florent Jacquemard; Michael Rusinowitch
Détail: Kutsia, Temur and Schreiner, Wolfgang and Fernández, Maribel. 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming (PPDP), Jul 2010, Hagenberg, Austria. ACM
Accès au texte intégral et bibtex

Rapports

Titre: Random Generation of Positive TAGEDs wrt. the Emptiness Problem
Auteurs: Pierre-Cyrille Heam; Vincent Hugot; Olga Kouchnarenko
Détail: [Research Report], 2010, pp. 43. RR-7441
Accès au texte intégral et bibtex

Titre: A Constraint-based Approach to Web Services Provisioning
Auteurs: Eric Monfroy; Olivier Perrin; Christophe Ringeissen; Laurent Vigneron
Détail: [Research Report], 2010, pp. 39. RR-7413
Accès au texte intégral et bibtex

Titre: Simulations for a Class of Two-Dimensional Automata
Auteurs: Gérard Cécé; Alain Giorgetti
Détail: [Research Report], 2010, pp. 18. RR-7425
Accès au texte intégral et bibtex

Titre: Satisfiability of General Intruder Constraints with and without a Set Constructor
Auteurs: Tigran Avanesov; Yannick Chevalier; Michael Rusinowitch; Mathieu Turuani
Détail: [Research Report], 2010, pp. 50. RR-7276
Accès au texte intégral et bibtex

Documents sans référence de publication

Titre: Rewriting Approximations For Properties Verification Over CCS Specifications
Auteurs: Roméo Courbis
Détail: Jun. 2010
Accès au texte intégral et bibtex

2009

Articles dans des revues avec comité de lecture

Titre: Politiques d'adaptation pour la reconfiguration du composant de localisation
Auteurs: Julien Dormoy; Olga Kouchnarenko; Hassan Mountassir
Détail: Journal Européen des Systèmes Automatisés, 2009, 43 (7-8-9), pp. 773-789
Accès au texte intégral et bibtex

Titre: jSynoPSys - A Scenario-Based Testing Tool based on the Symbolic Animation of B Machines
Auteurs: Frédéric Dadeau; Régis Tissot
Détail: Electronic Notes in Theoretical Computer Science, Elsevier, 2009, Proceedings of Fifth Workshop on Model Based Testing (MBT 2009), 253 (2), pp. 117-132
Accès au bibtex

Titre: On the Use of Uniform Random Generation of Automata for Testing
Auteurs: Frédéric Dadeau; Pierre-Cyrille Héam; Jocelyn Levrey
Détail: Electronic Notes in Theoretical Computer Science, Elsevier, 2009, Proceedings of Fifth Workshop on Model Based Testing (MBT 2009), 253 (2), pp. 37-51
Accès au bibtex

Titre: Test fonctionnel de conformité vis-à-vis d'une politique de contôle d'accès
Auteurs: Frédéric Dadeau; Amal Haddad; Thierry Moutet
Détail: Revue Technique et Science Informatiques (TSI), Hermes, 2009, Supervision et sécurité dans les grands réseaux, 28 (4), pp. 533-563
Accès au bibtex

Titre: Automated UML models merging for web services testing
Auteurs: Vincent Pretre; Adrien De Kermadec; Fabrice Bouquet; Christophe Lang; Frédéric Dadeau
Détail: International Journal of Web and Grid Services, 2009, 5 (2), pp. 107-129
Accès au texte intégral et bibtex

Titre: Handling Non Left-Linear Rules When Completing Tree Automata
Auteurs: Yohan Boichut; Roméo Courbis; Pierre-Cyrille Héam; Olga Kouchnarenko
Détail: International Journal of Foundations of Computer Science, 2009, 20 (5), pp. 837-849
Accès au texte intégral et bibtex

Titre: Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives
Auteurs: Yohan Boichut; Pierre-Cyrille Héam; Olga Kouchnarenko
Détail: Electronic Notes in Theoretical Computer Science, 2009, 239, pp. 57-72
Accès au texte intégral et bibtex

Titre: Safely composing security protocols
Auteurs: Véronique Cortier; Stéphanie Delaune
Détail: Formal Methods in System Design, Kluwer Academic Publishers, 2009, 34 (1), pp. 1-36
Accès au bibtex

Titre: Abusing SIP authentication
Auteurs: Humberto Abdelnur; Tigran Avanesov; Michael Rusinowitch; Radu State
Détail: Journal of Information Assurance and Security, Dynamic Publishers Inc., USA, 2009, Special Issue on Access Control and Protcols, 4 (4), pp. 311-318
Accès au texte intégral et bibtex

Titre: Computationally Sound Implementations of Equational Theories against Passive Adversaries
Auteurs: Mathieu Baudet; Véronique Cortier; Steve Kremer
Détail: Information and Computation, Elsevier Science Publishers, 2009, 207 (4), pp. 496-520
Accès au bibtex

Titre: New results on rewrite-based satisfiability procedures
Auteurs: Alessandro Armando; Maria Paola Bonacina; Silvio Ranise; Stephan Schulz
Détail: ACM Transactions on Computational Logic, ACM, 2009, 10 (1), Article 4, 51 p.
Accès au bibtex

Communications avec actes

Titre: A Flexible Access Control Model for Distributed Collaborative Editors
Auteurs: Abdessamad Imine; Asma Cherif; Michael Rusinowitch
Détail: Willem Jonker and Milan Petkovic. 6th VLDB Workshop on Secure Data Management - SDM 2009, Aug 2009, Lyon, France. Springer, Secure Data Management, 5776, pp. 89-106, Lecture Notes in Computer Science
Accès au bibtex

Titre: Undo-Based Access Control for Distributed Collaborative Editors
Auteurs: Asma Cherif; Abdessamad Imine
Détail: Yuhua Luo. 6th International Conference on Cooperative Design, Visualization, and Engineering - CDVE 2009, Sep 2009, Luxembourg, Luxembourg. Springer, Cooperative Design, Visualization, and Engineering, 5738, pp. 101-108, Lecture Notes in Computer Science
Accès au bibtex

Titre: How to Tackle Integer Weighted Automata Positivity
Auteurs: Yohan Boichut; Pierre-Cyrille Heam; Olga Kouchnarenko
Détail: Olivier Bournez and Igor Potapov. 3rd InternationalWorkshop on Reachability Problems - RP 2009, Sep 2009, Palaiseau, France. Springer -Verlag, Reachability Problems, 5797, pp. 79-92, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: Decidable Analysis for a Class of Cryptographic Group Protocols with Unbounded Lists
Auteurs: Najah Chridi; Mathieu Turuani; Michael Rusinowitch
Détail: Computer Security Foundations Symposium, Jul 2009, Port Jefferson, United States. IEEE, Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF'09), pp. 277-289
Accès au bibtex

Titre: On Model-Checking Optimistic Replication Algorithms
Auteurs: Hanifa Boucheneb; Abdessamad Imine
Détail: David Lee and Antónia Lopes and Arnd Poetzsch-Heffter. 11th IFIP WG 6.1 International Conference FMOODS 2009 and 29th IFIP WG 6.1 International Conference FORTE 2009, Jun 2009, Lisbonne, Portugal. Springer, Formal Techniques for Distributed Systems, 5522, pp. 73-89, Lecture Notes in Computer Science
Accès au bibtex

Titre: From Business Processes to Integration Testing
Auteurs: Stéphane Debricon; Fabrice Bouquet; Bruno Legeard
Détail: Olivier Zendra. 5èmes journées sur l'Ingénierie Dirigée par les Modèles - IDM 2009, Mar 2009, Nancy, France. Actes des 5èmes journées sur l'Ingénierie Dirigée par les Modèles, 1, pp. 49-64
Accès au bibtex

Titre: UML Modeling and Formal Verification of Secure Group Communication Protocols
Auteurs: Pierre De Saqui-Sannes; Thierry Villemur; Benjamin Fontan; Sara Mota; Mohamed Salah Bouassida; Najah Chridi; Isabelle Chrisment; Laurent Vigneron
Détail: Second IEEE International workshop UML and Formal Methods - UML&FM'2009, 2009, Rio de Janeiro, Brazil.
Accès au bibtex

Titre: Génération automatique de tests à partir de patrons de propriétés
Auteurs: Frédéric Dadeau
Détail: AFADL'09, Approches Formelles dans l'Assistance au Développement de Logiciels, Jan 2009, Toulouse, France. pp. 177-191
Accès au texte intégral et bibtex

Titre: Automatic Methods for Analyzing Non-repudiation Protocole with an Active Intruder
Auteurs: Francis Klay; Laurent Vigneron
Détail: Pierpaolo Degano, Joshua D. Guttman and Fabio Martinelli. 5th International Workshop on Formal Aspects in Security and Trust - FAST 2008, Oct 2008, Malaga, Spain. Springer-Verlag, Formal Aspects in Security and Trust, 5491, pp. 192-209, 2009, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: TAGED Approximations for Temporal Properties Model-Checking
Auteurs: Roméo Courbis; Pierre-Cyrille Heam; Olga Kouchnarenko
Détail: Proceedings of the 14th International Conference on Implementation and Application of Automata - CIAA'09, Jul 2009, Sydney, Australia.
Accès au texte intégral et bibtex

Titre: Graph Based Reduction of Program Verification Conditions
Auteurs: Jean-François Couchot; Alain Giorgetti; Nicolas Stouls
Détail: Hassen Saïdi and N. Shankar. Automated Formal Methods (AFM'09), colocated with CAV'09, Jun 2009, Grenoble, France. ACM Press, pp. 40-47
Accès au texte intégral et bibtex

Titre: Random Generation of Deterministic Tree (Walking) Automata
Auteurs: Pierre-Cyrille Héam; Cyril Nicaud; Sylvain Schmitz
Détail: Sebastian Maneth. 14th International Conference on Implementation and Application of Automata - CIAA 2009, Jul 2009, Sydney, Australia. Springer-Verlag, Implementation and Application of Automata, 5642, pp. 115-124, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: A Generic Security API for Symmetric Key Management on Cryptographic Devices
Auteurs: Véronique Cortier; Graham Steel
Détail: Michael Backes and Peng Ning. 14th European Symposium On Research In Computer Security - ESORICS'09, Sep 2009, St Malo, France. Springer, Computer security - ESORICS 2009, 5789, pp. 605-620, Lecture Notes in Coputer Science
Accès au bibtex

Titre: A method for proving observational equivalence
Auteurs: Véronique Cortier; Stéphanie Delaune
Détail: 22nd IEEE Computer Security Foundations Symposium - CSF'09, Jul 2009, Port Jefferson, United States. IEEE Computer Society Press, pp. 266-276
Accès au bibtex

Titre: YAPA: A generic tool for computing intruder knowledge
Auteurs: Mathieu Baudet; Véronique Cortier; Stéphanie Delaune
Détail: Ralf Treinen. 20th International Conference on Rewriting Techniques and Applications - RTA'09, Jun 2009, Brasilia, Brazil. Springer, Rewriting techniques and applications, 5595, pp. 148-163, Lecture Notes in Computer Science
Accès au bibtex

Titre: Unification Modulo Homomorphic Encryption
Auteurs: Siva Anantharaman; Hai Lin; Christopher Lynch; Paliath Narendran; Michael Rusinowitch
Détail: Silvio Ghilardi and Roberto Sebastiani. 7th International Symposium on Frontiers of Combining Systems - FroCoS 2009, Sep 2009, Trento, Italy. Springer, Frontiers of Combining Systems, 5749, pp. 100-116, Lecture Notes in Computer Science
Accès au bibtex

Titre: Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
Auteurs: Enrica Nicolini; Christophe Ringeissen; Michael Rusinowitch
Détail: Stefan Kowalewski and Anna Philippou. 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS 2009, Mar 2009, York, United Kingdom. Springer, Tools and Algorithms for the Construction and Analysis of Systems, 5505, pp. 428-442, Lecture Notes in Computer Science
Accès au bibtex

Titre: Combinable Extensions of Abelian Groups
Auteurs: Enrica Nicolini; Christophe Ringeissen; Michael Rusinowitch
Détail: Renate Schmidt. 22nd International Conference on Automated Deduction - CADE-22, Aug 2009, Montreal, Canada. Springer, Automated Deduction – CADE-22, 5663, pp. 51-66, Lecture Notes in Artificial Intelligence
Accès au bibtex

Titre: Data Structures with Arithmetic Constraints: a Non-disjoint Combination
Auteurs: Enrica Nicolini; Christophe Ringeissen; Michael Rusinowitch
Détail: Silvio Ghilardi and Roberto Sebastiani. 7th International Symposium on Frontiers of Combining Systems - FroCoS'2009, Sep 2009, Trento, Italy. Springer, Frontiers of Combining Systems, 5749, pp. 335-350, Lecture Notes in Artificial Intelligence
Accès au bibtex

Titre: Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives
Auteurs: Yohan Boichut; Pierre-Cyrille Heam; Olga Kouchnarenko
Détail: 9th International Workshop on Verification of Infinite-State Systems - INFINITY'07, 2007, Lisbonnes, Portugal. 239, pp. 57-72, 2009
Accès au bibtex

Titre: A Logical Framework for Reasoning about Policies with Trust Negotiation and Workflows
Auteurs: Philippe Balbiani; Yannick Chevalier; Marwa El-Houri
Détail: Proceedings of the 4th International Conference on Risks and Security of Internet and Systems - CRiSIS 2009, Oct 2009, Toulouse, France.
Accès au bibtex

Titre: Coordination Model for Real-Time Collaborative Editors
Auteurs: Abdessamad Imine
Détail: John Field and Vasco T. Vasconcelos. Coordination Models and Languages, 11th International Conference, COORDINATION 2009, Jun 2009, Lisboa, Portugal. Springer, Coordination Models and Languages 11th International Conference, COORDINATION 2009, Lisboa, Portugal, June 9-12, 2009. Proceedings, 5521, pp. 225-246, Lecture Notes in Computer Science
Accès au bibtex

Titre: Mapping Computation with No Memory
Auteurs: Serge Burckel; Emeric Gioan ; Emmanuel Thomé
Détail: UC'2009: 8th International Conference on Unconventional Computation, Sep 2009, Ponta Delgada, Portugal. Springer, 5715, pp. 85-97, LNCS
Accès au bibtex

Communications sans actes

Titre: Petri Nets with May/Must Semantics
Auteurs: Olga Kouchnarenko; Natalia Sidorova; Nikola Trcka
Détail: Workshop on Concurrency, Specification, and Programming - CS&P 2009, Sep 2009, Kraków-Przegorzały, Poland. Concurrency, Specification, and Programming, 1
Accès au bibtex

Titre: Modeling and Verifying Ad Hoc Routing Protocol
Auteurs: Mathilde Arnaud; Véronique Cortier; Stéphanie Delaune
Détail: 4th International Workshop on Security and Rewriting Techniques - SecReT'09, Jul 2009, Port Jefferson, United States. pp. 33-46
Accès au bibtex

Conférences invitées

Titre: Verification of Security Protocols
Auteurs: Véronique Cortier
Détail: Neil D. Jones and Markus Müller-Olm. 10th Conference on Verification, Model Checking, and Abstract Interpretation - VMCAI'09, Jan 2009, Savannah, United States. Springer, Verification, Model Checking, and Abstract Interpretation, 5403, pp. 5-13, Lecture Notes in Computer Science
Accès au bibtex

Chapitres d'ouvrages scientifiques

Titre: Validating Integrity for the Ephemerizer's Protocol with CL-Atse
Auteurs: Charu Arora; Mathieu Turuani
Détail: Véronique Cortier and Claude Kirchner and Mitsuhiro Okada and Hideki Sakurada. Formal to Practical Security : Papers Issued from the 2005-2008 French-Japanese Collaboration, 5458, Springer Berlin Heidelberg, pp. 21-32, 2009, Lecture Notes in Computer Science, 978-3-642-02002-5
Accès au bibtex

HDR

Titre: Raisonnement équationnel et méthodes de combinaison: de la programmation à la preuve
Auteurs: Christophe Ringeissen
Détail: Université Henri Poincaré - Nancy I, Nov. 2009. French
Accès au texte intégral et bibtex

Titre: Analyse des protocoles cryptographiques: des modèles symboliques aux modèles calculatoires
Auteurs: Véronique Cortier
Détail: Institut National Polytechnique de Lorraine - INPL, Nov. 2009. French
Accès au texte intégral et bibtex

Titre: Automates finis pour la fiabilité logicielle et l'analyse d'accessibilité
Auteurs: Pierre-Cyrille Heam
Détail: Université de Franche-Comté, Nov. 2009. French
Accès au texte intégral et bibtex

Autres publications

Titre: Specifying and Proving a Sorting Algorithm
Auteurs: Elena Tushkanova; Alain Giorgetti; Olga Kouchnarenko
Détail: Oct. 2009. Rapport de recherche LIFC
Accès au texte intégral et bibtex

Ouvrages scientifiques

Titre: Formal to practical Security
Auteurs: Véronique Cortier; Claude Kirchner; Mitsuhiro Okada; Hideki Sakurada
Détail: 5458. Springer, pp. 200, Feb. 2009, Lecture Notes in Computer Science, 978-3-642-02001-8
Accès au bibtex

Rapports

Titre: Synthesising Secure APIs
Auteurs: Véronique Cortier; Graham Steel
Détail: [Research Report], 2009, pp. 24. RR-6882
Accès au texte intégral et bibtex

Titre: Deciding knowledge in security protocols under some e-voting theories
Auteurs: Mouhebeddine Berrima; Narjes Ben Rajeb; Véronique Cortier
Détail: [Research Report], 2009, pp. 29. RR-6903
Accès au texte intégral et bibtex

Titre: A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems
Auteurs: Véronique Cortier; Steve Kremer; Bogdan Warinschi
Détail: [Research Report], 2009, pp. 42. RR-6912
Accès au texte intégral et bibtex

Titre: Safe and Efficient Strategies for Updating Firewall Policies
Auteurs: Zeeshan Ahmed; Abdessamad Imine; Michaël Rusinowitch
Détail: [Research Report], 2009, pp. 19. RR-6940
Accès au texte intégral et bibtex

Titre: An Optimistic Mandatory Access Control Model for Distributed Collaborative Editors
Auteurs: Abdessamad Imine; Asma Cherif; Michaël Rusinowitch
Détail: [Research Report], 2009, pp. 20. RR-6939
Accès au texte intégral et bibtex

Titre: Combinable Extensions of Abelian Groups
Auteurs: Enrica Nicolini; Christophe Ringeissen; Michael Rusinowitch
Détail: [Research Report], 2009, pp. 30. RR-6920
Accès au texte intégral et bibtex

Titre: Data Structures with Arithmetic Constraints: a Non-Disjoint Combination
Auteurs: Enrica Nicolini; Christophe Ringeissen; Michael Rusinowitch
Détail: [Research Report], 2009, pp. 23. RR-6963
Accès au texte intégral et bibtex

Titre: Rewrite based Verification of XML Updates
Auteurs: Florent Jacquemard; Michael Rusinowitch
Détail: [Research Report], 2009, pp. 39. RR-7007
Accès au texte intégral et bibtex

Titre: Compiling and securing cryptographic protocols
Auteurs: Yannick Chevalier; Michael Rusinowitch
Détail: [Research Report], 2009, pp. 12
Accès au texte intégral et bibtex

Titre: Sequential decomposition of operations and compilers optimization
Auteurs: Mumtaz Ahmad; Serge Burckel; Adam Cichon
Détail: [Research Report], 2009, pp. 91. RR-7076
Accès au texte intégral et bibtex

Titre: Seed: an easy to use random generator of recursive data structures for testing
Auteurs: Pierre-Cyrille Heam; Cyril Nicaud
Détail: [Research Report], 2009, pp. 18
Accès au texte intégral et bibtex

Thèses

Titre: Contributions à la vérification automatique de protocoles de groupes.
Auteurs: Najah Chridi
Détail: informatique. Université Henri Poincaré - Nancy I, Sep. 2009. French
Accès au texte intégral et bibtex

2008

Articles dans des revues avec comité de lecture

Titre: A Note on Partially Ordered Tree Automata
Auteurs: Pierre-Cyrille Héam
Détail: Information Processing Letters, 2008, 108 (4), pp. 242-246
Accès au texte intégral et bibtex

Titre: Verification of class liveness properties with Java modeling language
Auteurs: Alain Giorgetti; Julien Groslambert; Jacques Julliand; Olga Kouchnarenko
Détail: IET Software, 2008, 2 (6), pp. 500-514
Accès au texte intégral et bibtex

Titre: Efficiency of Automata in Semi-Commutation Verification Techniques
Auteurs: Gérard Cécé; Pierre-Cyrille Héam; Yann Mainier
Détail: Theoretical Informatics and Applications, 2008, 42 (2), pp. 197-215
Accès au texte intégral et bibtex

Titre: A Theoretical Limit for Safety Verification Techniques with Regular Fix-point Computations
Auteurs: Yohan Boichut; Pierre-Cyrille Heam
Détail: Information Processing Letters, Elsevier, 2008, 108 (1), pp. 1-2
Accès au bibtex

Titre: Tree automata with equality constraints modulo equational theories
Auteurs: Florent Jacquemard; Michael Rusinowitch; Laurent Vigneron
Détail: Journal of Logic and Algebraic Programming, Elsevier, 2008, 75 (2), pp. 182-208
Accès au texte intégral et bibtex

Titre: Hierarchical combination of intruder theories
Auteurs: Yannick Chevalier; Michael Rusinowitch
Détail: Information and Computation, Elsevier Inc., 2008, 206 (2-4), pp. 352-377
Accès au texte intégral et bibtex

Titre: Complexity results for security protocols with Diffie-Hellman exponentiation and commuting public key encryption
Auteurs: Yannick Chevalier; Ralf Kuesters; Michael Rusinowitch; Mathieu Turuani
Détail: ACM Transactions on Computational Logic (TOCL), ACP, 2008, 9 (4), pp. Article 24
Accès au bibtex

Titre: Approximation based tree regular model checking
Auteurs: Yohan Boichut; Pierre-Cyrille Heam; Olga Kouchnarenko
Détail: Nordic Journal of Computing, Publishing Association Nordic Journal of Computing, 2008, 14, pp. 216-241
Accès au texte intégral et bibtex

Titre: Timed Specification For Web Services Compatibility Analysis
Auteurs: Nawal Guermouche; Olivier Perrin; Christophe Ringeissen
Détail: Electronic Notes in Theoretical Computer Science, Electronic Notes in Theoretical Computer Science, 2008, 200 (3), pp. 155-170
Accès au bibtex

Titre: A comprehensive combination framework
Auteurs: Silvio Ghilardi; Enrica Nicolini; Daniele Zucchelli
Détail: ACM Transactions on Computational Logic, ACM, 2008, 9 (2), pp. Article n° 8
Accès au bibtex

Communications avec actes

Titre: In Situ Design of Register Operations
Auteurs: Emeric Gioan ; Serge Burckel
Détail: ISVLSI'08: IEEE Computer Society Annual Symposium on Very-Large-Scale Integration, Apr 2008, Montpellier, France. IEEE Computer Society, Trends in VLSI Technology and Design, pp. 4
Accès au bibtex

Titre: Teaching Model-Based Testing with {L}eirios {T}est {G}enerator
Auteurs: Frédéric Dadeau; Régis Tissot
Détail: FORMED'08, Int. Workshop on Formal Methods in Computer Science Education, co-located with ETAPS'2008), 2008, Hungary. pp. 129-138
Accès au texte intégral et bibtex

Titre: Handling Left-Quadratic Rules When Completing Tree Automata
Auteurs: Yohan Boichut; Roméo Courbis; Pierre-Cyrille Héam; Olga Kouchnarenko
Détail: 2nd Workshop on Reachability Problems in Computational Models - RP'08, Sep 2008, Liverpool, United Kingdom. Elsevier, 223, pp. 61-70, Electronic Notes in Theoretical Computer Science
Accès au texte intégral et bibtex

Titre: Finer is better: Abstraction Refinement for Rewriting Approximations
Auteurs: Yohan Boichut; Roméo Courbis; Pierre-Cyrille Héam; Olga Kouchnarenko
Détail: Andrei Voronkov. RTA'08, 19th international conference on Rewriting Techniques and Applications, Jul 2008, Hagenberg, Austria. Springer, 5117, pp. 48-62, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: A Mediator Based Approach For Services Composition
Auteurs: Nawal Guermouche; Olivier Perrin; Christophe Ringeissen
Détail: International Conference on Software Engineering Research, Management and Applications (SERA'08), Aug 2008, Prague, Czech Republic.
Accès au bibtex

Titre: Computational soundness of observational equivalence
Auteurs: Hubert Comon-Lundh; Véronique Cortier
Détail: 15th ACM Conference on Computer and Communications Security - CCS'08, Oct 2008, Alexandria, United States. ACM
Accès au bibtex

Titre: Abusing SIP Authentication
Auteurs: Humberto Abdelnur; Tigran Avanesov; Michaël Rusinowitch; Radu State
Détail: Information Assurance and Security ( ISIAS), Sep 2008, Naples, Italy. IEEE, Information Assurance and Security, 2008. ISIAS '08., pp. 237-242
Accès au texte intégral et bibtex

Titre: An inference system for detecting firewall filtering rules anomalies
Auteurs: Tarek Abbes; Adel Bouhoula; Michael Rusinowitch
Détail: 23rd Annual ACM Symposium on Applied Computing - SAC'08, 2008, Fortaleza, Brazil. ACM, pp. 2122-2128
Accès au bibtex

Titre: Closure of Hedge-Automata Languages by Hedge Rewriting
Auteurs: Florent Jacquemard; Michael Rusinowitch
Détail: A. Voronkov. 19th International Conference on Rewriting Techniques and Applications - RTA 2008, 2008, Hagenberg, Austria. Springer Berlin / Heidelberg, Rewriting Techniques and Applications, 5117, pp. 157-171, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: Dynamic Web Services Provisioning with Constraints
Auteurs: Eric Monfroy; Olivier Perrin; Christophe Ringeissen
Détail: Robert Meersman and Zahir Tari. International Conference on Cooperative Information Systems, OTM Conferences, Nov 2008, Monterrey, Mexico. Springer, OTM 2008, Part I, 5331, pp. 26-43, Lecture Notes in Computer Science
Accès au bibtex

Titre: Combining Scenario- and Model-Based Testing to ensure POSIX Compliance
Auteurs: Frédéric Dadeau; Adrien De Kermadec; Régis Tissot
Détail: Egon Börger, Michael Butler, Jonathan P. Bowen and Paul Boca. First International Conference on ASM, B and Z - ABZ'08, Sep 2008, London, United Kingdom. Springer Berlin / Heidelberg, Abstract State Machines, B and Z, 5238, pp. 153-166, Lecture Notes in Computer Science
Accès au bibtex

Titre: A Verifiable Conformance Relationship between Smart Card Applets and B security Models
Auteurs: Frédéric Dadeau; Julien Lamboley; Thierry Moutet; Marie-Laure Potet
Détail: Egon Börger, Michael Butler, Jonathan P. Bowen and Paul Boca. First International Conference on ASM, B and Z - ABZ'08, Sep 2008, London, United Kingdom. Springer Berlin / Heidelberg, Abstract State Machines, B and Z, 5238, pp. 237-250, Lecture Notes in Computer Science
Accès au bibtex

Titre: A B Formal Framework for Security Developments in the Domain of Smart Card Applications
Auteurs: Frédéric Dadeau; Régis Tissot; Marie-Laure Potet
Détail: 23rd International Information Security Conference - SEC'08, Sep 2008, Milano, Italy. Springer, 278, pp. 141-155, IFIP
Accès au bibtex

Titre: Automatic Composition of Services with Security Policies
Auteurs: Yannick Chevalier; Mohammed Anis Mekki; Michael Rusinowitch
Détail: Web Service Composition and Adaptation Workshop (held in conjunction with SCC/SERVICES-2008), Jul 2008, Honolulu, United States. IEEE, pp. 529-537
Accès au bibtex

Titre: Towards a Constrained-based Verification of Parameterized Cryptographic Protocols
Auteurs: Najah Chridi; Mathieu Turuani; Michael Rusinowitch
Détail: Michael Hanus. 18th International Symposium on Logic-Based Program Synthesis and Transformation - LOPSTR 2008, Jul 2008, Valence, Spain. pp. 191-206
Accès au texte intégral et bibtex

Titre: Decentralized concurrency control for real-time collaborative editors
Auteurs: Abdessamad Imine
Détail: Djamal Benslimane, Aris Ouksel. 8th international conference on New technologies in distributed systems - NOTERE'2008, Jun 2008, Lyon, France. ACM New York, NY, USA, NOTERE '08: Proceedings of the 8th international conference on New technologies in distributed systems, pp. 313-321
Accès au bibtex

Titre: Flexible Concurrency Control for Real-Time Collaborative Editors
Auteurs: Abdessamad Imine
Détail: 28th International Conference on Distributed Computing Systems Workshops - ICDCS'08, Jun 2008, Beijing, China. IEEE Computer Society, pp. 423-428
Accès au bibtex

Titre: Towards SMT Model Checking of Array-Based Systems
Auteurs: Silvio Ghilardi; Enrica Nicolini; Silvio Ranise; Daniele Zucchelli
Détail: Alessandro Armando and Peter Baumgartner and Gilles Dowek. Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Aug 2008, Sydney, Australia. Springer, Automated Reasoning 4th International Joint Conference, IJCAR 2008 Sydney, Australia, August 12-15, 2008 Proceedings, 5195, pp. 67-82, Lecture Notes in Computer Science
Accès au bibtex

Communications sans actes

Titre: Computational soundness of observational equivalence
Auteurs: Hubert Comon-Lundh; Véronique Cortier
Détail: 4th Workshop on Formal and Computational Cryptography - FCC 2008, Jun 2008, Pittsburgh, United States.
Accès au bibtex

Titre: Active Intruders with Caps
Auteurs: Siva Anatharaman; Hai Lin; Chris Lynch; Paliath Narendran; Michael Rusinowitch
Détail: FCS-ARSPA-WITS'08, Jun 2008, Pittsburgh, United States.
Accès au bibtex

Rapports

Titre: Computational soundness of observational equivalence
Auteurs: Hubert Comon-Lundh; Véronique Cortier
Détail: [Research Report], 2008, pp. 36. RR-6508
Accès au texte intégral et bibtex

Titre: Experiments in Model-Checking Optimistic Replication Algorithms
Auteurs: Hanifa Boucheneb; Abdessamad Imine
Détail: [Research Report], 2008, pp. 49. RR-6510
Accès au texte intégral et bibtex

Titre: Combination of Convex Theories: Modularity, Deduction Completeness, and Explanation
Auteurs: Duc-Khanh Tran; Christophe Ringeissen; Silvio Ranise; Hélène Kirchner
Détail: [Research Report], 2008, pp. 34. RR-6688
Accès au texte intégral et bibtex

Titre: Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
Auteurs: Enrica Nicolini; Christophe Ringeissen; Michael Rusinowitch
Détail: [Research Report], 2008, pp. 22. RR-6697
Accès au texte intégral et bibtex

Titre: Constraints-based Verification of Parameterized Cryptographic Protocols.
Auteurs: Najah Chridi; Mathieu Turuani; Michaël Rusinowitch
Détail: [Research Report], 2008, pp. 54. RR-6712
Accès au texte intégral et bibtex

Titre: Graph-based Reduction of Program Verification Conditions
Auteurs: Jean-François Couchot; Alain Giorgetti; Nicolas Stouls
Détail: [Research Report], 2008, pp. 22. RR-6702
Accès au texte intégral et bibtex

Thèses

Titre: Combinaison de Méthodes de Vérification
Auteurs: Daniele Zucchelli
Détail: Université Henri Poincaré - Nancy I, Jan. 2008. English
Accès au texte intégral et bibtex

Documents sans référence de publication

Titre: On the Decidability of (ground) Reachability Problems for Cryptographic Protocols (extended version)
Auteurs: Yannick Chevalier; Mounira Kourjieh
Détail: 2008
Accès au texte intégral et bibtex

2007

Articles dans des revues avec comité de lecture

Titre: Relating two standard notions of secrecy
Auteurs: Véronique Cortier; Michaël Rusinowitch; Eugen Zalinescu
Détail: Logical Methods in Computer Science, Logical Methods in Computer Science, 2007, 3 (3, paper 2), pp. 1-29
Accès au bibtex

Titre: Decision procedures for extensions of the theory of arrays
Auteurs: Silvio Ghilardi; Enrica Nicolini; Silvio Ranise; Daniele Zucchelli
Détail: Annals of Mathematics and Artificial Intelligence, Springer, 2007, 50 (3-4), pp. 231-254
Accès au bibtex

Titre: Automated Verification of a Key Management Architecture for Hierarchical Group Protocols
Auteurs: Mohamed Salah Bouassida; Najah Chridi; Isabelle Chrisment; Olivier Festor; Laurent Vigneron
Détail: Annales des Télécommunications, Hermes, 2007, 62 (11-12), pp. 1365-1387
Accès au bibtex

Articles dans des revues sans comité de lecture

Titre: Vérifier automatiquement les protocoles de sécurité
Auteurs: Yohan Boichut; Pierre-Cyrille Heam; Olga Kouchnarenko
Détail: Techniques de l'Ingenieur, Editions T.I., 2007, pp. 1-9
Accès au bibtex

Communications avec actes

Titre: Towards automatic control for microfactories.
Auteurs: Eric Descourvières; Stéphane Debricon; Dominique Gendreau; Philippe Lutz; Laurent Philippe; Fabrice Bouquet
Détail: 5th International Conference on Industrial Automation, IAIA'2007., Jun 2007, Montréal, Canada. Pratt & Withney Canada, sur CD ROM - 4 p.
Accès au texte intégral et bibtex

Titre: Intruders with Caps
Auteurs: Siva Anantharaman; Paliath Narendran; Michael Rusinowitch
Détail: F. Baader. Rewriting Techniques and Applications - RTA'07, Jun 2007, Paris, France. Springer-Verlag, pp. 20-35, Lecture Notes in Computer Science
Accès au bibtex

Titre: Instantiation of Parameterized Data Structures for Model-Based Testing
Auteurs: Fabrice Bouquet; Jean-François Couchot; Frédéric Dadeau; Alain Giorgetti
Détail: Jacques Julliand et Olga Kouchnarenko. 7th International Formal Specification and Development in B Conference, B 2007, Jan 2007, Besançon, France. Springer-Verlag, 4355, pp. 96-110, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: Optimistic Non-repudiation Protocol Analysis
Auteurs: Judson Santos Santiago; Laurent Vigneron
Détail: Damien Sauveron and Konstantinos Markantonakis and Angelos Bilas and Jean-Jacques Quisquater. Information Security Theory and Practices - Smart Cards, Mobile and Ubiquitous Computing Systems, May 2007, Heraklion, Greece. Springer, First IFIP TC6 / WG 8.8 / WG 11.2 International Workshop, WISTP 2007, Heraklion, Crete, Greece, May 9-11, 2007. Proceedings, 4462, pp. 90-101, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: Un programme annoté en vaut deux
Auteurs: Alain Giorgetti; Julien Groslambert
Détail: Journée Francophone des Langages Applicatifs - JFLA07, Jan 2007, Aix-les-Bains, France.
Accès au texte intégral et bibtex

Titre: Safely Composing Security Protocols
Auteurs: Véronique Cortier; Jérémie Delaitre; Stéphanie Delaune
Détail: 27th Conference on Foundations of Software Technology and Theoretical Computer Science - FSTTCS'07, Dec 2007, New Delhi, India.
Accès au bibtex

Titre: Synthetizing secure protocols
Auteurs: Véronique Cortier; Bogdan Warinschi; Eugen Zalinescu
Détail: Joachim Biskup et Javier López. 12th European Symposium On Research In Computer Security - ESORICS'07, Sep 2007, Dresden, Germany. Springer-Verlag, Computer Security – ESORICS 2007 12th European Symposium On Research In Computer Security, Dresden, Germany, September 24 — 26, 2007. Proceedings, 4734, pp. 406-421, Lecture Notes in Computer Science
Accès au bibtex

Titre: A Cryptographic Model for Branching Time Security Properties -- the Case of Contract Signing Protocols.
Auteurs: Véronique Cortier; Ralf Kuesters; Bogdan Warinschi
Détail: Joachim Biskup et Javier López. 12th European Symposium On Research In Computer Security - ESORICS'07, Sep 2007, Dresden, Germany. Springer-Verlag, Computer Security – ESORICS 2007 12th European Symposium On Research In Computer Security, Dresden, Germany, September 24 — 26, 2007. Proceedings, 4734, pp. 422-437, Lecture Notes in Computer Science
Accès au bibtex

Titre: Deciding knowledge in security protocols for monoidal equational theories.
Auteurs: Véronique Cortier; Stéphanie Delaune
Détail: 14th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR'07, Oct 2007, Yerevan, Armenia.
Accès au bibtex

Titre: Combining algorithms for deciding knowledge in security protocols
Auteurs: Mathilde Arnaud; Véronique Cortier; Stéphanie Delaune
Détail: 6th International Symposium on Frontiers of Combining Systems - FroCoS'07, Sep 2007, Liverpool, United Kingdom.
Accès au bibtex

Titre: A Formal Theory of Key Conjuring.
Auteurs: Véronique Cortier; Stéphanie Delaune; Graham Steel
Détail: 20th IEEE Computer Security Foundations Symposium - CSF'07, Jul 2007, Venice, Italy. IEEE Computer Society, pp. 79-96
Accès au bibtex

Titre: Automatic Analysis of the Security of XOR-based Key Management Schemes.
Auteurs: Véronique Cortier; Keighren Gavin; Graham Steel
Détail: Orna Grumberg et Michael Huth. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07),, Mar 2007, Braga, Portugal. Springer-Verlag, Tools and Algorithms for the Construction and Analysis of Systems 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007. Proceedi, 4424, pp. 538-552, Lecture Notes in Computer Science
Accès au bibtex

Titre: How to Handle QoS Aspects in Web Services Substitutivity Verification
Auteurs: Pierre-Cyrille Heam; Olga Kouchnarenko; Jérôme Voinot
Détail: 16th IEEE International Workshops on Enabling Technologies: Infrastructures for Collaborative Enterprises - WETICE 2007, Jun 2007, Paris, France.
Accès au bibtex

Titre: Combining Proof-Producing Decision Procedures
Auteurs: Silvio Ranise; Christophe Ringeissen; Duc-Khanh Tran
Détail: Boris Konev and Frank Wolter. 6th International Symposium o Frontiers of Combining Systems - FroCoS 2007, Sep 2007, Liverpool, United Kingdom. Springer Berlin / Heidelberg, 4720, pp. 237-251, Lecture Notes in Artificial Intelligence
Accès au bibtex

Titre: Timed Specification For Web Services Compatibility Analysis
Auteurs: Nawal Guermouche; Olivier Perrin; Christophe Ringeissen
Détail: International Workshop on Automated Specification and Verification of Web Systems - WWV 2007, Dec 2007, San Servolo island, Venice, Italy. Elsevier
Accès au bibtex

Titre: How Symbolic Animation can help designing an Efficient Formal Model
Auteurs: Fabrice Bouquet; Frédéric Dadeau; Bruno Legeard
Détail: Kung-Kiu Lau and Richard Banach. 7th International Conference on Formal Engineering Methods - ICFEM 2005, Nov 2005, Manchester, France. Springer Berlin / Heidelberg, Formal Methods and Software Engineering, 3785, pp. 96-110, 2007, Lecture Notes in Computer Science
Accès au bibtex

Titre: Towards an Automatic Analysis of Web Service Security
Auteurs: Yannick Chevalier; Denis Lugiez; Michael Rusinowitch
Détail: Konev, Boris and Wolter, Franck. 6th International Symposium on Frontiers of Combining Systems - FroCoS'07, Sep 2007, Liverpool, United Kingdom. Springer, Frontiers of Combining Systems, 4720, pp. 133-147, Lecture Notes in Artificial Intelligence
Accès au bibtex

Titre: Verifying Cryptographic Protocols with Subterms Constraints
Auteurs: Yannick Chevalier; Denis Lugiez; Michael Rusinowitch
Détail: Dershowitz, Nachum and Voronkov, Andrei. 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR 2007, Oct 2007, Yerevan, Armenia. Springer, Logic for Programming, Artificial Intelligence, and Reasoning, 4790, pp. 181-195, Lecture Notes in Artificial Intelligence
Accès au bibtex

Titre: Noetherianity and Combination Problems
Auteurs: Silvio Ghilardi; Enrica Nicolini; Silvio Ranise; Daniele Zucchelli
Détail: Boris Konev and Frank Wolter. Frontiers of Combining Systems, Sep 2007, Liverpool, United Kingdom. Springer, Frontiers of Combining Systems 6th International Symposium, FroCoS 2007 Liverpool, UK, September 10-12, 2007 Proceedings, 4720, pp. 206-220, Lecture Notes in Computer Science
Accès au bibtex

Titre: Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
Auteurs: Silvio Ghilardi; Enrica Nicolini; Silvio Ranise; Daniele Zucchelli
Détail: Frank Pfenning. Automated Deduction - CADE-21, Jul 2007, Bremen, Germany. Springer, Automated Deduction - CADE-21 21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007 Proceedings, 4603, pp. 362-378, Lecture Notes in Computer Science
Accès au bibtex

Titre: Automatic Decidability and Combinability Revisited
Auteurs: Christopher Lynch; Duc-Khanh Tran
Détail: Automated Deduction - CADE-21, 2007, Bremen, Germany. Springer, 4603, pp. 328-344, Lecture Notes in Computer Science
Accès au bibtex

Communications sans actes

Titre: Deciding knowledge in security protocols for monoidal equational theories.
Auteurs: Véronique Cortier; Stéphanie Delaune
Détail: Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis - FCS-ARSPA'07, Jul 2007, Wrocław, Poland.
Accès au bibtex

Titre: A Cryptographic Model for Branching Time Security Properties -- the Case of Contract Signing Protocols.
Auteurs: Véronique Cortier; Ralf Kuesters; Bogdan Warinschi
Détail: 3rd Workshop on Formal and Computational Cryptography - FCC 2007, Jul 2007, Venise, Italy.
Accès au bibtex

Titre: Deciding key cycles for security protocols.
Auteurs: Véronique Cortier; Eugen Zalinescu
Détail: 3rd Workshop on Formal and Computational Cryptography - FCC 2007, Jul 2007, Venise, Italy.
Accès au bibtex

Chapitres d'ouvrages scientifiques

Titre: Strategy for Flaws Detection based on a Services-driven Model for Group Protocols
Auteurs: Laurent Vigneron; Najah Chridi
Détail: Frédéric Benhamou and Narendra Jussien and Barry O\'Sullivan. Future and Trends in Constraint Programming, ISTE, pp. 361-370, 2007, 1905209975
Accès au bibtex

Autres publications

Titre: Intruders with Caps
Auteurs: Siva Anantharaman; Paliath Narendran; Michaël Rusinowitch
Détail: May. 2007, Rapport LIFO, RR-2007-02 (Projet PRV, Catégorie Z). Version détaillée du papier accepté au RTA'07. (Version courte apparaitra dans les actes du RTA'07, dans la série LNCS, en juin 2007.)
Accès au texte intégral et bibtex

Rapports

Titre: Combining algorithms for deciding knowledge in security protocols
Auteurs: Mathilde Arnaud; Véronique Cortier; Stéphanie Delaune
Détail: [Research Report], 2007. RR-6118
Accès au texte intégral et bibtex

Titre: A Formal Theory of Key Conjuring
Auteurs: Véronique Cortier; Stéphanie Delaune; Graham Steel
Détail: [Research Report], 2007, pp. 38. RR-6134
Accès au texte intégral et bibtex

Titre: Toward an Automatic Analysis of Web Service Security
Auteurs: Yannick Chevalier; Denis Lugiez; Michael Rusinowitch
Détail: [Research Report], 2007, pp. 40. RR-6341
Accès au texte intégral et bibtex

Titre: From passive to active security via a simple transformation
Auteurs: Zalinescu Eugen; Véronique Cortier; Bogdan Warinschi
Détail: [Research Report], 2007
Accès au bibtex

Titre: Synthesizing secure protocols
Auteurs: Véronique Cortier; Bogdan Warinschi; Eugen Zalinescu
Détail: [Research Report], 2007, pp. 32. RR-6166
Accès au texte intégral et bibtex

Titre: Towards Formalizing QoS of Web Services with Weighted Automata
Auteurs: Pierre-Cyrille Heam; Olga Kouchnarenko; Jérôme Voinot
Détail: [Research Report], 2007, pp. 22. RR-6218
Accès au texte intégral et bibtex

Titre: Safely composing security protocols
Auteurs: Véronique Cortier; Jérémie Delaitre; Stéphanie Delaune
Détail: [Research Report], 2007, pp. 26. RR-6234
Accès au texte intégral et bibtex

Titre: Transitive Closures of Semi-commutation Relations on Regular omega-Languages
Auteurs: Pierre-Cyrille Héam
Détail: [Research Report], 2007, pp. 20. RR-6239
Accès au texte intégral et bibtex

Titre: A Methodology For Web Services Composition
Auteurs: Nawal Guermouche; Olivier Perrin; Christophe Ringeissen
Détail: [Interne], 2007
Accès au bibtex

Titre: Automatic Methods for Analyzing Non-Repudiation Protocols with an Active Intruder
Auteurs: Francis Klay; Judson Santiago; Laurent Vigneron
Détail: [Research Report], 2007, pp. 22. RR-6324
Accès au texte intégral et bibtex

Thèses

Titre: Sécurité des protocoles cryptographiques : décidabilité et résultats de transfert
Auteurs: Eugen Zalinescu
Détail: informatique. Université Henri Poincaré - Nancy I, Dec. 2007. French
Accès au texte intégral et bibtex

Titre: Vérification des protocoles cryptographiques : Comparaison des modèles symboliques avec une application des résultats --- Etude des protocoles récursifs
Auteurs: Heinrich Hördegen
Détail: Université Henri Poincaré - Nancy I, Nov. 2007. French
Accès au texte intégral et bibtex

Titre: Conception de Procédures de Décision par Combinaison et Saturation
Auteurs: Duc-Khanh Tran
Détail: Université Henri Poincaré - Nancy I, Feb. 2007. French
Accès au texte intégral et bibtex

2006

Articles dans des revues avec comité de lecture

Titre: A note on maximally repeated sub-patterns of a point set
Auteurs: Véronique Cortier; Xavier Goaoc; Mira Lee; Na Hyeon-Suk
Détail: Discrete Mathematics, 2006, 306 (16), pp. 1965-1968
Accès au texte intégral et bibtex

Titre: Formal Design and Verification of Operational Transformation Algorithms for Copies Convergence
Auteurs: Abdessamad Imine; Michaël Rusinowitch; Gérald Oster; Pascal Molli
Détail: Theoretical Computer Science, Elsevier, 2006, Algebraic Methodology and Software Technology, 351 (2), pp. 167-183
Accès au bibtex

Titre: A Survey of Algebraic Properties Used in Cryptographic Protocols
Auteurs: Véronique Cortier; Stéphanie Delaune; Pascal Lafourcade
Détail: Journal of Computer Security, IOS Press, 2006, 14 (1), pp. 1-43
Accès au bibtex

Titre: Compositional Analysis of Contract Signing Protocols
Auteurs: Michael Backes; Anupam Datta; Ante Derek; John C. Mitchell; Mathieu Turuani
Détail: Theoretical Computer Science, Elsevier, 2006, Theoretical Computer Science
Accès au bibtex

Titre: Sécurité des communications de groupe
Auteurs: Najah Chridi; Laurent Vigneron
Détail: La Revue de l'Electricité et de l'Electronique, Société de l'Électricité, de l'Électronique et des Technologies de l'Information et de la Communication, 2006, Risques et sécurité des réseaux et des systèmes à composante logicielle, 6/7, pp. 51-60
Accès au bibtex

Titre: Deciding knowledge in security protocols under equational theories.
Auteurs: Véronique Cortier; Martin Abadi
Détail: Theoretical Computer Science, Elsevier, 2006, 367 (1-2), pp. 2-32
Accès au bibtex

Articles dans des revues sans comité de lecture

Titre: Ces protocoles qui nous protègent
Auteurs: Véronique Cortier
Détail: Tangente, Editions Pole, 2006
Accès au bibtex

Titre: Divers protocoles couramment utilisés en informatique
Auteurs: Véronique Cortier
Détail: Tangente, Editions Pole, 2006
Accès au bibtex

Titre: Protocoles cryptographiques : analyse par méthodes formelles
Auteurs: Véronique Cortier
Détail: Techniques de l'Ingenieur, Techniques de l'ingénieur, 2006
Accès au bibtex

Communications avec actes

Titre: Handling Algebraic Properties in Automatic Analysis of Security Protocols
Auteurs: Yohan Boichut; Pierre-Cyrille Héam; Olga Kouchnarenko
Détail: ICTAC'2006, Nov 2006, Tunis, Tunisia. pp. 153-167
Accès au bibtex

Titre: Feasible Trace Reconstruction for Rewriting Approximations
Auteurs: Yohan Boichut; Thomas Genet
Détail: RTA'2006, Aug 2006, Seattle, United States. pp. 123-135
Accès au bibtex

Titre: {JML}-based Verification of Liveness Properties on a Class in isolation
Auteurs: Julien Groslambert; Jacques Julliand; Olga Kouchnarenko
Détail: SAVCBS'06, Specification and Verification of Component-Based Systems, 2006, United States. pp. 41-48
Accès au texte intégral et bibtex

Titre: Safety Property Driven Test Generation from {JML} Specifications
Auteurs: Fabrice Bouquet; Frédéric Dadeau; Julien Groslambert; Jacques Julliand
Détail: FATES/RV'06, 1st Int. Workshop on Formal Approaches to Testing and Runtime Verification, 2006, United States. pp. 225-239
Accès au texte intégral et bibtex

Titre: Computationally Sound Compositional Logic for Security Protocols
Auteurs: Anupam Datta; Ante Derek; John C. Mitchell; Arnab Roy; Vitaly Shmatikov; Mathieu Turuani; Bogdan Warinschi
Détail: Véronique Cortier et Steve Kremer. Workshop on Formal and Computational Cryptography - FCC 2006, Jul 2006, Venice/Italy.
Accès au texte intégral et bibtex

Titre: Soundness of Symbolic Equivalence for Modular Exponentiation
Auteurs: Yassine Lakhnech; Laurent Mazare; Bogdan Warinschi
Détail: Véronique Cortier et Steve Kremer. Workshop on Formal and Computational Cryptography - FCC 2006, Jul 2006, Venice/Italy.
Accès au texte intégral et bibtex

Titre: Automatic Verification of Key Management Architecture for Hierarchical Group Protocols
Auteurs: Mohamed Salah Bouassida; Najah Chridi; Isabelle Chrisment; Olivier Festor; Laurent Vigneron
Détail: Sécurité et Architecture des Réseaux - SAR 2006, May 2006, Seignosse/France. pp. 381-397
Accès au texte intégral et bibtex

Titre: Adding Integrity to the Ephemerizer's Protocol
Auteurs: Charu Arora; Mathieu Turuani
Détail: Stephan Merz and Tobias Nipkow. Sixth International Workshop on Automatic Verification of Critical Systems - AVOCS'06, Sep 2006, Nancy/France. pp. 146-151
Accès au texte intégral et bibtex

Titre: The CL-Atse Protocol Analyser
Auteurs: Mathieu Turuani
Détail: Frank Pfenning. 17th International Conference on Term Rewriting and Applications - RTA 2006, Aug 2006, Seattle, WA/USA. Springer, 4098, pp. 277-286, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: Implementing a Unification Algorithm for Protocol Analysis with XOR
Auteurs: Max Tuengerthal; Ralf Küsters; Mathieu Turuani
Détail: 20th International Workshop on Unification - UNIF'06, Aug 2006, Seattle, WA/USA. pp. 1-5
Accès au texte intégral et bibtex

Titre: Strategy for Flaws Detection based on a Services-driven Model for Group Protocols
Auteurs: Najah Chridi; Laurent Vigneron
Détail: Workshop on Constraints in Software Testing, Verification and Analysis - CSTVA 06, Sep 2006, Nantes/France. pp. 88-99
Accès au texte intégral et bibtex

Titre: Validation of Prouve Protocols using the Automatic Tool TA4SP
Auteurs: Yohan Boichut; Nikolai Kosmatov; Laurent Vigneron
Détail: 3rd Taiwanese-French Conference on Information Technology, Mar 2006, Nancy/France. pp. 467-480
Accès au bibtex

Titre: Automatically Analysing Non-repudiation with Authentication
Auteurs: Judson Santos Santiago; Laurent Vigneron
Détail: 3rd Taiwanese-French Conference on Information Technology - TFIT 06, Mar 2006, Nancy/France. pp. 541-554
Accès au bibtex

Titre: Computationally Sound Symbolic Secrecy in the Presence of Hash Functions
Auteurs: Véronique Cortier; Steve Kremer; Ralf Kuesters; Bogdan Warinschi
Détail: Proceedings of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06), Dec 2006, Kolkata, India.
Accès au bibtex

Titre: Deciding key cycles for security protocols
Auteurs: Véronique Cortier; Eugen Zalinescu
Détail: Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), Nov 2006, Phnom Penh, Cambodia.
Accès au bibtex

Titre: Relating two standard notions of secrecy
Auteurs: Véronique Cortier; Michaël Rusinowitch; Eugen Zalinescu
Détail: Proc. of the 20th Int. Conference Computer Science Logic (CSL'06), Sep 2006, Szeged, Hungary.
Accès au bibtex

Titre: On the Decidability of a Class of XOR-based Key-management APIs
Auteurs: Véronique Cortier; Graham Steel
Détail: Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA'06), Aug 2006, Seattle, Washington.
Accès au bibtex

Titre: Explicit Randomness is not Necessary when Modeling Probabilistic Encryption
Auteurs: Véronique Cortier; Heinrich Hoerdegen; Bogdan Warinschi
Détail: Workshop on Information and Computer Security (ICS 2006), Sep 2006, Timisoara, Romania.
Accès au bibtex

Titre: Data Consistency for P2P Collaborative Editing
Auteurs: Gérald Oster; Pascal Urso; Pascal Molli; Abdessamad Imine
Détail: ACM Conference on Computer-Supported Cooperative Work - CSCW 2006, Nov 2006, Banff, Alberta, Canada. ACM Press, Proceedings of the 2006 20th anniversary conference on Computer supported cooperative work, pp. 259 - 268
Accès au texte intégral et bibtex

Titre: Tombstone Transformation Functions for Ensuring Consistency in Collaborative Editing Systems
Auteurs: Gérald Oster; Pascal Molli; Pascal Urso; Abdessamad Imine
Détail: IEEE Conference on Collaborative Computing: Networking, Applications and Worksharing - CollaborateCom 2006, Nov 2006, Atlanta, Georgia, USA. IEEE, Collaborative Computing: Networking, Applications and Worksharing, 2006. CollaborateCom 2006. International Conference on, pp. 1-10
Accès au texte intégral et bibtex

Titre: JAG: JML Annotation Generation for Verifying Temporal Properties
Auteurs: Alain Giorgetti; Julien Groslambert
Détail: L. Baresi and R. Heckel. 9th International Conference on Fundamental Approaches to Software Engineering - FASE'2006, Mar 2006, Vienna/Austria. Springer, 3922, pp. 373-376, Lecture Notes in Computer Science
Accès au bibtex

Titre: JAG : Génération d'annotations JML pour vérifier des propriétés temporelles
Auteurs: Alain Giorgetti; Julien Groslambert
Détail: Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'06, Mar 2006, Paris, France.
Accès au bibtex

Titre: Automatic Combinability of Rewriting-Based Satisfiability Procedures
Auteurs: Hélène Kirchner; Silvio Ranise; Christophe Ringeissen; Duc-Khanh Tran
Détail: Miki Hermann, Andrei Voronkov. 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR 2006, Nov 2006, Phnom Penh/Cambodia. Springer, Logic for Programming, Artificial Intelligence, and Reasoning, 4246, pp. 542-556, Lecture Notes in Artificial Intelligence
Accès au bibtex

Titre: Decision Procedures for the Formal Analysis of Software
Auteurs: David Déharbe; Pascal Fontaine; Silvio Ranise; Christophe Ringeissen
Détail: Kamel Barkaoui, Ana Cavalcanti, Antonio Cerone. 3rd International Colloquium on Theoretical Aspects of Computing, ICTAC, Nov 2006, Tunis, Tunisia. Springer, Theoretical Aspects of Computing --- ICTAC 2006, 4281, pp. 366-370, Lecture Notes in Computer Science
Accès au bibtex

Titre: Building and Combining Satisfiability Procedures for Software Verification
Auteurs: Hélène Kirchner; Silvio Ranise; Christophe Ringeissen; Duc-Khanh Tran
Détail: Samuel Cruz-Lara, Yih-Kuen Tsay. Third Taiwanese-French Conference on Information Technology (TFIT), Mar 2006, Nancy, France. pp. 125-139
Accès au bibtex

Titre: Producing Conflict Sets for Combination of Theories
Auteurs: Silvio Ranise; Christophe Ringeissen; Duc-Khanh Tran
Détail: Byron Cook, Roberto Sebastiani. Workshop on Pragmatics of Decision Procedures in Automated Reasoning - PDPAR 2006, Aug 2006, Seattle, WA/USA. Proceedings of PDPAR'06
Accès au bibtex

Titre: Automated Boundary Test Generation from JML Specifications
Auteurs: Fabrice Bouquet; Frédéric Dadeau; Bruno Legeard
Détail: Jayadev Misra, Tobias Nipkow and Emil Sekerinski. 14th international symposium on Formal Methods - FM'06, Aug 2006, Hamilton, Canada. Springer Berlin / Heidelberg, FM 2006: Formal Methods, 4085, pp. 428-443, Lecture Notes in Computer Science
Accès au bibtex

Titre: Safety Property Driven Test Generation from JML Specifications
Auteurs: Fabrice Bouquet; Frédéric Dadeau; Jacques Julliand; Julien Groslambert
Détail: Klaus Havelund, Manuel Núñez, Grigore Rosu and Burkhart Wolff. International Workshop on Formal Approaches to Testing and Runtime Verification - FATES/RV'06, Aug 2006, Seattle, United States. Springer Berlin / Heidelberg, Formal Approaches to Software Testing and RuntimeVerification, 4262, pp. 225-239, Lecture Notes in Computer Science
Accès au bibtex

Titre: Tree automata with equality constraints modulo equational theories
Auteurs: Florent Jacquemard; Michael Rusinowitch; Laurent Vigneron
Détail: Ulrich Furbach and Natarajan Shankar. 3d International Joint Conference on Automated Reasoning (IJCAR), Aug 2006, Seattle, United States. Springer, 3d International Joint Conference on Automated Reasoning (IJCAR), 4130, pp. 557-571, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Conférences invitées

Titre: Verification of cryptographic protocols: techniques and link to cryptanalysis
Auteurs: Véronique Cortier
Détail: Stephan Merz and Tobias Nipkow. Sixth International Workshop on Automatic Verification of Critical Systems - AVOCS'06, Sep 2006, Nancy/France.
Accès au texte intégral et bibtex

Chapitres d'ouvrages scientifiques

Titre: Sécuriser les réseaux, les protocoles cryptographiques
Auteurs: Véronique Cortier
Détail: Presses Universitaires de France. Sur les chemins de la découverte, Presses Universitaires de France, 2006
Accès au bibtex

Directions d'ouvrages

Titre: Journal of Automata, Languages and Combinatorics, Vol. 11(1)
Auteurs: Siva Anantharaman; Gaétan Hains; Michael Rusinowitch; Paul Gastin; John Mullins
Détail: Otto-von-Guericke-Universität, D-39016 Magdeburg, pp. 142, 2006
Accès au bibtex

Rapports

Titre: Handling Algebraic Properties in Automatic Analysis of Security Protocols
Auteurs: Yohan Boichut; Pierre-Cyrille Héam; Olga Kouchnarenko
Détail: [Research Report], 2006, pp. 18. RR-5857
Accès au texte intégral et bibtex

Titre: Relating two Standard Notions of Secrecy
Auteurs: Eugen Zalinescu; Véronique Cortier; Michaël Rusinowitch
Détail: [Research Report], 2006, pp. 32. RR-5908
Accès au texte intégral et bibtex

Titre: Explicit Randomness is not Necessary when Modeling Probabilistic Encryption
Auteurs: Véronique Cortier; Heinrich Hördegen; Bogdan Warinschi
Détail: [Research Report], 2006, pp. 12. RR-5928
Accès au texte intégral et bibtex

Titre: JAG : Génération d'annotations JML pour vérifier des propriétés temporelles
Auteurs: Alain Giorgetti; Julien Groslambert
Détail: [Research Report], 2006
Accès au texte intégral et bibtex

Titre: Automatic Abstraction Generation : How to Make an Expert Verification Technique for Security Protocols available to Non-expert Users
Auteurs: Yohan Boichut; Pierre-Cyrille Héam; Olga Kouchnarenko
Détail: [Research Report], 2006, pp. 21. RR-6039
Accès au texte intégral et bibtex

2005

Articles dans des revues avec comité de lecture

Titre: Tree automata with one memory, set constraints and cryptographic protocols
Auteurs: Hubert Comon-Lundh; Véronique Cortier
Détail: Theoretical Computer Science, Elsevier, 2005, 331 (1), pp. 143-214
Accès au bibtex

Titre: An NP Decision Procedure for Protocol Insecurity with XOR
Auteurs: Yannick Chevalier; Ralf Küsters; Michaël Rusinowitch; Mathieu Turuani
Détail: Theoretical Computer Science, Elsevier, 2005, Theoretical Computer Science, 338 (1-3), pp. 247-274
Accès au bibtex

Titre: Vérifier les protocoles cryptographiques
Auteurs: Véronique Cortier
Détail: Techniques et Sciences Informatiquess, Hermes Science, 2005
Accès au bibtex

Communications avec actes

Titre: Validation of the ASW Contract Signing Protocol
Auteurs: Mathieu Turuani; Hoan Vu-Van
Détail: 3rd APPSEM II Workshop, Sep 2005, Frauenchiemsee, Germany.
Accès au bibtex

Titre: The AVISPA Tool for the automated validation of internet security protocols and applications
Auteurs: Alessandro Armando; David Basin; Yohan Boichut; Yannick Chevalier; Luca Compagna; Jorge Cuellar; Paul Hankes Drielsma; Pierre-Cyrille Héam; Olga Kouchnarenko; Jacopo Mantovani; Sebastian Mödersheim; David Von Oheimb; Michaël Rusinowitch; Judson Santos Santiago; Luca Vigano; Mathieu Turuani; Laurent Vigneron
Détail: Kousha Etessami and Sriram K. Rajamani. 17th International Conference on Computer Aided Verification - CAV 2005, Jul 2005, Edinburgh, Scotland/UK, France. Springer, 3576, pp. 281-285, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: Towards Synchronizing Linear Collaborative Objects with Operation Transformation
Auteurs: Abdessamad Imine; Pascal Molli; Gérald Oster; Michaël Rusinowitch
Détail: F. Wang. International Conference on Formal Techniques for Networked and Distributed Systems - FORTE 2005, Oct 2005, Taipei/Taiwan. IFIP International Federation for Information Processing 2005, 3731, pp. 411-427, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: Edition collaborative sur réseau pair-à-pair à large échelle
Auteurs: Gérald Oster; Pascal Urso; Pascal Molli; Abdessamad Imine
Détail: Journées Francophones sur la Cohérence des Données en Univers Réparti - CDUR 2005, Nov 2005, Paris/France. pp. 42-47
Accès au texte intégral et bibtex

Titre: Combining Lists with Non-Stably Infinite Theories
Auteurs: Pascal Fontaine; Silvio Ranise; Calogero Zarba
Détail: Franz Baader; Andrei Voronkov. 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'04), Mar 2005, Montevideo/Uruguay. Springer-Verlag, Logic for Programming, Artificial Intelligence, and Reasoning: 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005. Proceedings, 3452, pp. 51-66, Lecture Notes in Computer Science
Accès au texte intégral et bibtex

Titre: Deciding knowledge in security protocols under (many more) equational theories
Auteurs: Martin Abadi; Véronique Cortier
Détail: 18th IEEE Computer Security Foundations Workshop - CSFW'05, Jun 2005, Aix-en-Provence/France. IEEE Computer Society Press, pp. 62-76
Accès au bibtex

Titre: Computationally Sound Implementations of Equational Theories against Passive Adversaries
Auteurs: Mathieu Baudet; Véronique Cortier; Steve Kremer
Détail: Luís Caires, Giuseppe F. Italiano, Luís Monteiro, Catuscia Palamidessi, Moti Yung. 32nd International Colloquium on Automata, Languages and Programming - ICALP 2005, Jul 2005, Lisbonne/Portugal. Springer-Verlag, 3580, pp. 652-663, Lecture Notes in Computer Science
Accès au bibtex

Titre: Computationally Sound, Automated Proofs for Security Protocols
Auteurs: Véronique Cortier; Bogdan Warinschi
Détail: Mooly Sagiv. 14th European Symposium on Programming - ESOP 2005, Apr 2005, Edinburgh/United Kingdom. Springer-Verlag, 3444, pp. 157-171, Lecture Notes in Computer Science
Accès au bibtex

Titre: A resolution Strategy for Verifying Cryptographic Protocols with CBC Encryption and Blind Signatures
Auteurs: Véronique Cortier; Michaël Rusinowitch; Eugen Zalinescu
Détail: 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming - PPDP'05, Jul 2005, Lisbonne/Portugal. ACM press, pp. 12-22
Accès au bibtex

Titre: Combining data structures with nonstably infinite theories using many-sorted logic
Auteurs: Silvio Ranise; Christophe Ringeissen; Calogero Zarba
Détail: Bernard Gramlich. 5th International Workshop on Frontiers of Combining Systems - FroCoS'05, Sep 2005, Vienna/Austria. Springer, 3717, pp. 48-64, Lecture Notes in Artificial Intelligence
Accès au bibtex

Titre: On Superposition-Based Satisfiability Procedures and their Combination
Auteurs: Hélène Kirchner; Silvio Ranise; Christophe Ringeissen; Duc-Khanh Tran
Détail: Dang Van Hung and Martin Wirsing. 2nd International Colloquium on Theoretical Aspects of Computing - ICTAC'05, Oct 2005, Hanoi/Vietnam. Springer Verlag, 3722, pp. 594-608, Lecture Notes in Computer Science
Accès au bibtex

Titre: Modélisation des propriétés de sécurité de protocoles de groupe
Auteurs: Najah Chridi; Laurent Vigneron
Détail: 1er Colloque sur les Risques et la Sécurité d'Internet et des Systèmes, CRiSIS, Oct 2005, Bourges, France. pp. 119-132
Accès au texte intégral et bibtex

Titre: Study for Automatically Analysing Non-repudiation
Auteurs: Judson Santos Santiago; Laurent Vigneron
Détail: 1er Colloque sur les Risques et la Sécurité d'Internet et des Systèmes- CRiSIS 2005, Oct 2005, Bourges/France. pp. 157-171
Accès au texte intégral et bibtex

Titre: Compositional Analysis of Contract Signing Protocols
Auteurs: Michael Backes; Anupam Datta; Ante Derek; John C. Mitchell; Mathieu Turuani
Détail: 18th IEEE Computer Security Foundations Workshop - CSFW 2005, Jun 2005, Aix-en-Provence/France. IEEE Computer Society, pp. 94-110
Accès au bibtex

Titre: Analysis of Contract Signing Protocols
Auteurs: Mathieu Turuani
Détail: CriSis, Oct 2005, LIFO, ENSI-Bourges, France.
Accès au bibtex

Titre: On Structural Information and the Experimental Evaluation of SMT Tools
Auteurs: Najet Boughanmi; Silvio Ranise; Christophe Ringeissen
Détail: International Workshop on First-Order Theorem Proving - FTP'2005, Sep 2005, Koblenz, Germany.
Accès au texte intégral et bibtex

Titre: Symbolic Animation of JML Specifications
Auteurs: Fabrice Bouquet; Frédéric Dadeau; Bruno Legeard; Marc Utting
Détail: John Fitzgerald, Ian J. Hayes and Andrzej Tarlecki. International Conference on Formal Methods - FM'05, Jul 2005, Newcastle upon Tyne, United Kingdom. Springer Berlin / Heidelberg, FM 2005: Formal Methods, 3582, pp. 75-90, Lecture Notes in Computer Science
Accès au bibtex

Titre: Checking JML Specifications with B Machines
Auteurs: Fabrice Bouquet; Frédéric Dadeau; Julien Groslambert
Détail: Helen Treharne, Steve King, Martin Henson and Steve Schneider. International Conference on Formal Specification and Development in Z and B - ZB'05, Apr 2005, Guildford, United Kingdom. Springer Berlin / Heidelberg, ZB 2005: Formal Specification and Development in Z and B, 3455, pp. 434-453, Lecture Notes in Computer Science
Accès au bibtex

Titre: Using Constraint Logic Programming for the Symbolic Animation of Formal Models
Auteurs: Fabrice Bouquet; Frédéric Dadeau; Bruno Legeard
Détail: J. Marques-Silva and M. Velev. Proceedings of the International Workshop on Constraints in Formal Verification - CFV'05, Jul 2005, Tallinn, Estonia. pp. 32-46
Accès au bibtex

Titre: JML-Testing-Tools: a Symbolic Animator for JML Specifications using CLP
Auteurs: Fabrice Bouquet; Frédéric Dadeau; Bruno Legeard; Marc Utting
Détail: Nicolas Halbwachs and Lenore D. Zuck. International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS'05, Apr 2005, Edinburgh, United Kingdom. Springer Berlin / Heidelberg, 3440, pp. 551-556, Lecture Notes in Computer Science
Accès au bibtex

Conférences invitées

Titre: Probabilistic Polynomial-time Semantics for a Protocol Security Logic
Auteurs: Anupam Datta; Ante Derek; John C. Mitchell; Vitaly Shmatikov; Mathieu Turuani
Détail: Luis Caires et al.. 32nd International Colloquium on Automata, Languages and Programming - ICALP 2005, Jul 2005, Lisbon/Portugal. Springer, 3580, pp. 16-29, Lecture Notes in Computer Science
Accès au bibtex

Directions d'ouvrages

Titre: Proceedings of the 19th International Workshop on Unification
Auteurs: Laurent Vigneron
Détail: A05-R-022, LORIA, pp. 143, Apr. 2005
Accès au texte intégral et bibtex

Autres publications

Titre: Un outil d'aide à la conception de protocoles cryptographiques
Auteurs: Laurent Vigneron
Détail: 2005
Accès au bibtex

Rapports

Titre: A note on maximally repeated sub-patterns of a point set
Auteurs: Véronique Cortier; Xavier Goaoc; Mira Lee; Hyeon-Suk Na
Détail: [Research Report], 2005, pp. 5. RR-5773
Accès au texte intégral et bibtex

Titre: Automatic Verification of Security Protocols Using Approximations
Auteurs: Yohan Boichut; Pierre-Cyrille Héam; Olga Kouchnarenko
Détail: [Research Report], 2005, pp. 27. RR-5727
Accès au texte intégral et bibtex

Titre: Combining Data Structures with Nonstably Infinite Theories using Many-Sorted Logic
Auteurs: Silvio Ranise; Christophe Ringeissen; Calogero Zarba
Détail: [Research Report], 2005, pp. 39. RR-5678
Accès au texte intégral et bibtex

Titre: Combining Intruder Theories
Auteurs: Yannick Chevalier; Michaël Rusinowitch
Détail: [Research Report], 2005, pp. 37. RR-5495
Accès au texte intégral et bibtex

Titre: Proving correctness of transformation functions in collaborative editing systems
Auteurs: Gérald Oster; Pascal Urso; Pascal Molli; Abdessamad Imine
Détail: [Research Report], 2005, pp. 45. RR-5795
Accès au texte intégral et bibtex

Titre: Tree Automata with Equality Constraints Modulo Equational Theories
Auteurs: Florent Jacquemard; Michaël Rusinowitch; Laurent Vigneron
Détail: [Research Report], 2005, pp. 27. RR-5754
Accès au texte intégral et bibtex

Titre: Optimistic Replication for Massive Collaborative Editing
Auteurs: Gérald Oster; Pascal Urso; Pascal Molli; Hala Skaf-Molli; Abdessamad Imine
Détail: [Research Report], 2005, pp. 18. RR-5719
Accès au texte intégral et bibtex

Titre: Real time group editors without Operational transformation
Auteurs: Gérald Oster; Pascal Urso; Pascal Molli; Abdessamad Imine
Détail: [Research Report], 2005, pp. 24. RR-5580
Accès au texte intégral et bibtex

2004

Articles dans des revues avec comité de lecture

Titre: Strategy for Verifying Security Protocols with Unbounded Message Size
Auteurs: Yannick Chevalier; Laurent Vigneron
Détail: Journal of Automated Software Engineering, 2004, 11 (2), pp. 141-166
Accès au bibtex

Titre: Security properties: two agents are sufficient
Auteurs: Hubert Comon-Lundh; Véronique Cortier
Détail: Science of Computer Programming, 2004, 50 (1-3), pp. 51-71
Accès au bibtex

Titre: Unification Modulo ACUI Plus Distributivity Axioms
Auteurs: Siva Anantharaman; Paliath Narendran; Michaël Rusinowitch
Détail: Journal of Automated Reasoning, 2004, 33 (1), pp. 1-28
Accès au bibtex

Titre: On the Fly Pattern Matching For Intrusion Detection with Snort
Auteurs: Tarek Abbes; Adel Bouhoula; Michaël Rusinowitch
Détail: Annales des Télécommunications, 2004, 59 (9-10), pp. 941-967
Accès au bibtex

Communications avec actes

Titre: A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols
Auteurs: Yannick Chevalier; Luca Compagna; Jorge Cuellar; Paul Hankes Drielsma; Jacopo Mantovani; Sebastian Moedersheim; Laurent Vigneron
Détail: Workshop on Specification and Automated Processing of Security Requirements - SAPS'2004, 2004, Linz, Austria. Austrian Computer Society, 13 p
Accès au bibtex

Titre: A Simple Constraint-solving Decision Procedure for Protocols with Exclusive or
Auteurs: Yannick Chevalier
Détail: Kohlhase, Michael. 18th International Workshop on Unification - UNIF'2004, Jul 2004, Cork, Ireland. 15 p
Accès au bibtex

Titre: Rule-based Programs describing Internet Security Protocols
Auteurs: Yannick Chevalier; Laurent Vigneron
Détail: Abdennadher, Slim and Ringeissen, Christophe. 5th International Workshop on Rule-Based Programming - RULE'2004, Jun 2004, Aachen, Germany. pp. 83-97
Accès au bibtex

Titre: Un modèle sûr et générique pour la synchronisation de données divergentes
Auteurs: Gérald Oster; Pascal Molli; Hala Skaf-Molli; Abdessamad Imine
Détail: Premières Journées Francophones : Mobilité et Ubiquité - UbiMob'04, Jun 2004, Nice, France. 9 p
Accès au bibtex

Titre: Deciding knowledge in security protocols under equational theories
Auteurs: Martin Abadi; Véronique Cortier
Détail: Josep Diaz and Juhani Karhumäki and Arto Lepistö and Donald Theodore Sannella. The 31st International Colloquium on Automata, Languages and Programming - ICALP'2004, 2004, Turku, Finland. Springer, 3142, pp. 148-164, Lecture Notes in Computer Science
Accès au bibtex

Titre: Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn
Auteurs: Silvio Ranise; Christophe Ringeissen; Duc-Khanh Tran
Détail: First International Colloquium on Theoretical Aspects of Computing - ICTAC 2004, 2004, Guiyang, Chine. Springer-Verlag, 15 p, Lecture Notes in Computer Science
Accès au bibtex

Titre: Deductive Verification of Distributed Groupware Systems
Auteurs: Abdessamad Imine; Pascal Molli; Gérald Oster; Michaël Rusinowitch
Détail: Charles Rattray and Savitri Maharaj and Carron Shankland. Tenth International Conference on Algebraic Methodology and Software Technology - AMAST 2004, 2004, Stirling, Scotland, United Kingdom. Springer, 3116, pp. 226-240, Lecture Notes in Computer Science
Accès au bibtex

Titre: Automated Reasoning
Auteurs: David Basin; Michaël Rusinowitch
Détail: Basin, David and Rusinowitch, Michael. Second International Joint Conference on Automated Reasoning - IJCAR'2004, 2004, Cork, Irlande. Springer Verlag, 3097, XII-491 p, Lecture Notes in Computer Science
Accès au bibtex

Titre: A Decidable Analysis of Security Protocols
Auteurs: Michaël Rusinowitch
Détail: J.J. Lévy and E. Mayr and J. Mitchell. 18th IFIP World Computer Congress on Theoretical Computer Science - TCS'2004, 2004, Toulouse, France. Kluwer Academic Publishers, 1 p
Accès au bibtex

Titre: Protocol Analysis in Intrusion Detection Using Decision Tree
Auteurs: Tarek Abbes; Adel Bouhoula; Michaël Rusinowitch
Détail: International Conference on Information Technology: Coding and Computing - ITCC'04, Apr 2004, Las Vegas, Nevada, USA. 1, pp. 404-408
Accès au bibtex

Titre: Fast Multipattern Matching for Intrusion Detection
Auteurs: Tarek Abbes; Michaël Rusinowitch
Détail: Urs E. Gattiker. 13th Annual Conference on European Institute for Computer Anti-virus Research - EICAR'2004, May 2004, Luxemburg, Luxembourg. 22 p
Accès au bibtex

Titre: High Performance Intrusion Detection using Traffic Classification
Auteurs: Tarek Abbes; Alakesh Haloi; Michaël Rusinowitch
Détail: International Conference on Advances in Intelligent Systems - Theory and Applications - AISTA 2004, 2004, Luxembourg.
Accès au bibtex

Titre: Deciding the Security of Protocols with Commuting Public Key Encryption.
Auteurs: Yannick Chevalier; Ralf Küsters; Michaël Rusinowitch; Mathieu Turuani
Détail: Workshop on Automated Reasoning for Security Protocol Analysis - ARSPA'2004, Jul 2004, Cork, Ireland. 78, 11 p, Electronic Notes in Theoretical Computer Science - ENTCS
Accès au bibtex

Titre: Proving and Debugging Set-Based Specifications
Auteurs: Jean-François Couchot; Frédéric Dadeau; David Déharbe; Silvio Ranise
Détail: 6th Brazilian Workshop on Formal Methods, May 2004, Campina Grande, Brazil. 95, pp. 189-208, Electronic Notes in Theoretical Computer Science - ENTCS
Accès au bibtex

Conférences invitées

Titre: Automatic Verification of Security Protocols
Auteurs: Laurent Vigneron
Détail: Kohlhase, Michael. 18th International Workshop on Unification - UNIF'2004, Jul 2004, Cork, Ireland. 2 p
Accès au bibtex

Directions d'ouvrages

Titre: Special issue on First-Order Theorem Proving of the Journal of Automated Reasoning
Auteurs: Deepak Kapur; Laurent Vigneron
Détail: Deepak Kapur and Laurent Vigneron. 33 / n°3-4, Kluwer, pp. 219-383, 2004
Accès au bibtex

Autres publications

Titre: How Useful are Dag Automata?
Auteurs: Siva Anantharaman; Paliath Narendran; Michaël Rusinowitch
Détail: 2004, Projet PRV (du LIFO). Rapport de Recherche (LIFO)
Accès au texte intégral et bibtex

Rapports

Titre: Computationally Sound, Automated Proofs for Security Protocols
Auteurs: Véronique Cortier; Bogdan Warinschi
Détail: [Research Report], 2004, pp. 23. RR-5341
Accès au texte intégral et bibtex

Titre: A Decision Procedure for a Fragment of Set Theory Involving Monotone, Additive, and Multiplicative Functions
Auteurs: Calogero G. Zarba; Domenico Cantone; Jacob T. Schwartz
Détail: [Research Report], 2004, pp. 22. RR-5267
Accès au texte intégral et bibtex

Titre: Network Traffic Classification for Intrusion Detection
Auteurs: Tarek Abbes; Michaël Rusinowitch; Alakesh Haloi
Détail: [Research Report], 2004, pp. 20. RR-5230
Accès au texte intégral et bibtex

Titre: C-tableaux
Auteurs: Calogero G. Zarba
Détail: [Research Report], 2004, pp. 31. RR-5229
Accès au texte intégral et bibtex

Titre: A Simple Constraint-solving Decision Procedure for Protocols with Exclusive or
Auteurs: Yannick Chevalier
Détail: [Research Report], 2004, pp. 35. RR-5224
Accès au texte intégral et bibtex

Titre: Verification of Liveness Properties with JML
Auteurs: Françoise Bellegarde; Julien Groslambert; Marieke Huisman; Jacques Julliand; Olga Kouchnarenko
Détail: [Research Report], 2004, pp. 24. RR-5331
Accès au texte intégral et bibtex

Titre: Achieving Convergence with Operational Transformation in Distributed Groupware Systems
Auteurs: Abdessamad Imine; Pascal Molli; Gérald Oster; Michaël Rusinowitch
Détail: [Research Report], 2004, pp. 19. RR-5188
Accès au texte intégral et bibtex

Titre: Deciding knowledge in security protocols under equational theories
Auteurs: Martin Abadi; Véronique Cortier
Détail: [Research Report], 2004, pp. 22. RR-5169
Accès au texte intégral et bibtex

Titre: A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols
Auteurs: Yannick Chevalier; Luca Compagna; Jorge Cuellar; Paul Hankes Drielsma; Jacopo Mantovani; Sebastian Moedersheim; Laurent Vigneron
Détail: [Interne], 2004, 17 p. A04-R-067 || chevalier04b
Accès au bibtex

2003

Articles dans des revues avec comité de lecture

Titre: Protocol insecurity with a finite number of sessions, composed keys is NP-complete.
Auteurs: Michaël Rusinowitch; Mathieu Turuani
Détail: Theoretical Computer Science, Elsevier, 2003, Theoretical Computer Science, 1-3 (299), pp. 451-475
Accès au bibtex

Titre: On the expressivity and complexity of quantitative branching-time temporal logics.
Auteurs: François Laroussinie; Philippe Schnoebelen; Mathieu Turuani
Détail: Theoretical Computer Science, Elsevier, 2003, Theoretical Computer Science, 1-3 (297), pp. 297-315
Accès au bibtex

Communications avec actes

Titre: Proving Correctness of Transformation Functions in Real-Time Groupware
Auteurs: Abdessamad Imine; Pascal Molli; Gérald Oster; Michaël Rusinowitch
Détail: 8th European Conference of Computer-supported Cooperative Work - ECSCW'03, 2003, Helsinki, Finland. 18 p
Accès au bibtex

Titre: Automatic Detection of Copies Divergence in Collaborative Editing Systems
Auteurs: Abdessamad Imine; Pascal Urso
Détail: Eighth International Workshop on Formal Methods for Industrial Critical Systems - FMICS'03, Jun 2003, Trondheim, Norway. 80, pp. 92-108
Accès au bibtex

Titre: ACID-Unification is NEXPTIME-Decidable
Auteurs: Siva Anantharaman; Paliath Narendran; Michaël Rusinowitch
Détail: Branislav Rovan, Peter Vojtáš. 2003. Springer-Verlag, pp. 169-178, Lecture Notes in Computer Science - 2747
Accès au bibtex

Titre: Unification modulo ACUI plus Homomorphisms/Distributivity
Auteurs: Siva Anantharaman; Paliath Narendran; Michaël Rusinowitch
Détail: Franz Baader. 2003. Springer-Verlag, pp. 442-457, Lecture Notes in Artificial Intelligence - 2741
Accès au bibtex

Titre: Filtrage Efficace Pour la Détection d'Intrusions
Auteurs: Tarek Abbes; Adel Bouhoula; Michaël Rusinowitch
Détail: Conférence Francophone sur Sécurité et Architecture Réseaux (SAR'03), Jul 2003, Nancy, France. 10 p
Accès au bibtex

Titre: Extending the Dolev-Yao Intruder for Analyzing an Unbounded Number of Sessions
Auteurs: Yannick Chevalier; Ralf Küsters; Michaël Rusinowitch; Mathieu Turuani; Laurent Vigneron
Détail: M. Baaz and J. A. Makowsky. Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt Güdel Colloquium, KGC 2003, Aug 2003, Vienna, Austria. Springer, 2803, pp. 128-141, Lecture Notes in Computer Science
Accès au bibtex

Titre: VOTE: Group Editors Analyzing Tool
Auteurs: Abdessamad Imine; Pascal Molli; Gérald Oster; Pascal Urso
Détail: Fourth International Workshop on First-Order Theorem Proving - FTP'03, 2003, Valencia, Spain. Elsevier, FTP'2003, 4th International Workshop on First-Order Theorem Proving (in connection with RDP'03, Federated Conference on Rewriting, Deduction and Programming), 86/1, pp. 153-161, Electronic Notes in Theoretical Computer Science
Accès au bibtex

Titre: Using the Transformational Approach to Build a Safe and Generic Data Synchronizer
Auteurs: Pascal Molli; Gérald Oster; Hala Skaf-Molli; Abdessamad Imine
Détail: International Conference on Supporting Group Work - Group 2003, Nov 2003, Sanibel Island, Florida, USA. ACM Press, Proceedings of the 2003 international ACM SIGGROUP conference on Supporting group work, pp. 212-220
Accès au bibtex

Titre: Deciding the Security of Protocols with Diffie-Hellman Exponentiation and Products in Exponents
Auteurs: Yannick Chevalier; Ralf Küsters; Michaël Rusinowitch; Mathieu Turuani
Détail: FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science, 23rd Conference, Dec 2003, Mumbai, India. Springer, 2914, pp. 124-135, Lecture Notes in Computer Science
Accès au bibtex

Titre: An NP Decision Procedure for Protocol Insecurity with XOR
Auteurs: Yannick Chevalier; Ralf Küsters; Michaël Rusinowitch; Mathieu Turuani
Détail: 18th IEEE Symposium on Logic in Computer Science (LICS 2003), Jun 2003, Ottawa, Canada. IEEE Computer Society, pp. 261-270
Accès au bibtex

Directions d'ouvrages

Titre: 4th International Workshop on First-Order Theorem Proving- FTP'2003
Auteurs: Ingo Dahn; Laurent Vigneron
Détail: 1, Elsevier Science Publishers, 2003, Electronic Notes in Theoretical Computer Science
Accès au bibtex

Rapports

Titre: Safe Generic Data Synchronizer
Auteurs: Pascal Molli; Gérald Oster; Hala Skaf-Molli; Abdessamad Imine
Détail: [Interne], 2003, 8 p. A03-R-062 || molli03a
Accès au bibtex

Titre: Extending the Dolev-Yao Intruder for Analyzing an Unbounded Number of Sessions
Auteurs: Yannick Chevalier; Ralf Küsters; Michaël Rusinowitch; Mathieu Turuani; Laurent Vigneron
Détail: [Research Report], 2003, pp. 22. RR-4869
Accès au texte intégral et bibtex

Titre: Refinement and Verification of Synchronized Component-based Systems
Auteurs: Olga Kouchnarenko; Arnaud Lanoix
Détail: [Research Report], 2003, pp. 29. RR-4862
Accès au texte intégral et bibtex

Titre: Computing Approximations of Linear Transition Systems
Auteurs: Julien Musset; Michaël Rusinowitch
Détail: [Research Report], 2003, pp. 20. RR-4774
Accès au texte intégral et bibtex

Titre: Using Acceleration to Compute Parameterized System Refinement
Auteurs: Françoise Bellegarde; Célina Charlet; Olga Kouchnarenko
Détail: [Research Report], 2003, pp. 18. RR-4716
Accès au texte intégral et bibtex

Titre: An NP Decision Procedure for Protocol Insecurity with XOR
Auteurs: Yannick Chevalier; Ralf Küsters; Michaël Rusinowitch; Mathieu Turuani
Détail: [Research Report], 2003, pp. 22. RR-4697
Accès au texte intégral et bibtex

Titre: Efficiency of Automata in Semi-Commutation Verification Techniques
Auteurs: Gérard Cécé; Pierre-Cyrille Héam; Yann Mainier
Détail: [Research Report], 2003, pp. 20. RR-5001
Accès au texte intégral et bibtex

2002

Communications avec actes

Titre: Development of Transformation Functions Assisted by a Theorem Prover
Auteurs: Imine Abdessamad; Pascal Molli; Gérald Oster; Michaël Rusinowitch
Détail: Fourth International Workshop on Collaborative Editing 2002 - ACM CSCW'2002, 2002, Nouvelle-Orléans, USA. 8 p
Accès au bibtex

Titre: The AVISS Security Protocol Analysis Tool
Auteurs: Alessandro Armando; David Basin; Mehdi Bouallagui; Yannick Chevalier; Luca Compagna; Sebastian Moedersheim; Michaël Rusinowitch; Mathieu Turuani; Luca Vigano; Laurent Vigneron
Détail: Ed Brinksma and Kim Guldstrand Larsen. 14th International Conference on Computer Aided Verification - CAV'2002, Jul 2002, Copenhaguen, Denmark. Springer, 2404, pp. 349-353, Lecture Notes in Computer Science
Accès au bibtex

Titre: Automated Unbounded Verification of Security Protocols
Auteurs: Yannick Chevalier; Laurent Vigneron
Détail: Ed Brinksma and Kim Guldstrand Larsen. 14th International Conference on Computer Aided Verification - CAV'2002, 2002, Copenhaguen, Denmark. Springer, 2404, pp. 324-337, Lecture Notes in Computer Science
Accès au bibtex

Titre: Analyse Automatique de Protocoles de Sécurité avec CASRUL
Auteurs: Mehdi Bouallagui; Yannick Chevalier; Michaël Rusinowitch; Mathieu Turuani; Laurent Vigneron
Détail: Sécurité et Architecture Réseaux - SAR'2002, Jul 2002, Marrackech, Maroc, Morocco.
Accès au bibtex

Rapports

Titre: BDD-Driven First-Order Satisfiability Procedures (Extended Version)
Auteurs: David Déharbe; Silvio Ranise
Détail: [Research Report], 2002, pp. 24. RR-4630
Accès au texte intégral et bibtex

Titre: Automatic Approximation for the Verification of Cryptographic Protocols
Auteurs: Frédéric Oehl; Gérard Cécé; Olga Kouchnarenko; David Sinclair
Détail: [Research Report], 2002, pp. 18. RR-4599
Accès au texte intégral et bibtex

En savoir plus

Retrouvez toutes les publications scientifiques de nos équipes de recherche sur HAL Inria

Pierre-Louis Lions : Grand Prix Inria

Francis Bach : Prix Inria du jeune chercheur

Ethique & technologies numériques

Lancement d'Inriality

Informatique au Collège de France

Campagne Internships 2013

Ivan Laptev : Faire progresser la vision par ordinateur

Innover avec les sciences du numérique - Connect n° 3

Rencontre Inria-Industrie - Santé

Pierre-Louis Lions : Grand Prix Inria

Francis Bach : Prix Inria du jeune chercheur

Paul-Louis George : lauréat du Prix de l’innovation Inria - Dassault Systèmes 2012

Favoriser l’accueil des étudiants étrangers

Rencontres Inria - Industrie : Efficacité énergétique

Inria et France-Brevets signent un partenariat

iMatch Bio-Med Tech

iMatch Modèles Statistiques

Publications de l'équipe CASSIS

Archives

En savoir plus

Voir aussi

Siège et centres de recherche Inria

Accès direct

Social

Publications de l'équipe CASSIS

Partager

Archives

En savoir plus

Voir aussi

Siège et centres de recherche Inria

Accès direct

Social