- Renseignements pratiques
- Enseignement
Contact
LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2
Email:
contact.lifo
Tel: +33 (0)2 38 41 99 29
Fax: +33 (0)2 38 41 71 37
Accéder aux Rapports de l'année : 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018
RR-2003-01 A Synchronous Bisimulation-Based Approach for Information Flow Analysis
S. ANANTHARAMAN, G. HAINS
Résumé : Nous définissons une algèbre de processus dont la composition parallèle réalise une communication synchrone. Elle diffère de CCS essentiellement par l'hypothèse d'observabilité de la durée des actions internes. L'analyse de flot d'information dans notre formalisme est donc centrée sur la bisimulation forte plutôt que sur l'équivalence de traces ou sur la bisimulation faible. Dans notre théorie la bisimulation se réduit à l'égalité dans une théorie ACUID étendue avec un opérateur de préfixe. Nous montrons que l'analyse de flot d'information dans ce formalisme est plus fine que celles fondées sur les traces ou la bisimulation faible.
Mot(s) Clé(s) : flot d'information, bisimulation forte, protocoles cryptographiques
RR-2003-02 AC(U)ID-Unification is NEXPTIME-Decidable
S. ANANTHARAMAN, P. NARENDRAN, M. RUSINOWITCH.
Résumé : In an earlier work, we considered the theory AC(U)ID_l obtained by adjoining a binary symbol `*' which is assumed left-distributive over a basic AC(U)I-operator `+'; we showed there that AC(U)ID_l-unification is NEXPTIME-decidable and DEXPTIME-hard. In this paper we consider unification over AC(U)ID, where the the binary symbol adjoined `*' is assumed two-sided distributive over the AC(U)I-operator `+'. We formulate the problem as one of solving a particular class of set constraints, and propose a method for solving it in terms of the language of a labeled dag automaton associated to the problem. AC(U)ID-unification is thus shown to be NEXPTIME-decidable; it is also shown to be DEXPTIME-hard via other considerations.
Mot(s) Clé(s) : E-Unification, Complexity, Set constraints, Tree automata, Dag automata, Labeled dag automata.
RR-2003-03 Learning Characteristic Rules Relying on Quantified Paths
Teddy Turmeaux, Ansaf Salleb, Christel Vrain, Daniel Cassard
Résumé : La caractérisation est une tâche supervisée de fouille de données qui permet de résumer de manière succincte et concise un ensemble de données. Cette tâche est intéressante dans la mesure où elle ne nécessite pas de contre exemples. Nous proposons un cadre général pour la caractérisation d'un ensemble d'objets, appelé ensemble 'cible', en nous basant non seulement sur leurs propriétés propres mais aussi sur les propriétés des objets qui leur sont liés. Selon le type des objets considérés, différents liens peuvent être envisagés. Dans le cas de bases de données géographiques, ce sont les relations spatiales qui expriment des liens entre objets géoréférencés. Nous proposons 'Caracterix' un nouvel algorithme d'extraction de règles de caractérisation et nous montrons son application à des données géographiques réelles fournies par le BRGM.
Mot(s) Clé(s) : Aprentissage; fouille de données; règles caractéristiques; bases de données relationnelles; bases de données spatiales
RR-2003-04 Intermediate (Learned) Consistencies
Arnaud Lallouet, Andrei Legtchenko, Thi-Bich-Hanh Dao, AbdelAli Ed-Dbali
Résumé : What makes a good consistency ? Depending on the constraint, it may be a good pruning power or a low computational cost. By using machine learning techniques (search in an hypothesis space and clustering), we propose to define new automatically generated solvers which form a sequence of consistencies intermediate between bound- and arc-consistency. By associating to a consistency its quality, we define a method which allows, from a set of consistencies, to determine the best one to enforce for a given constraint. We apply this method on our generated intermediate consistencies. Surprisingly, traditional consistencies are not always the best choice and experiments show that learned intermediate consistencies sometimes outperform standard ones on various benchmarks according to the prediction.
Mot(s) Clé(s) : consistency; solver learning
RR-2003-05 A Synchronous Calculus for Secrecy Analysis
Siva ANANTHARAMAN, Jing CHEN, Gaétan HAINS, Paliath NARENDRAN
Résumé : Protocols are often modeled as value-passing processes in parallel composition, and their analysis based on CCS's interleaving semantics. The synchronous branches are the ones which are crucial in these models for analyzing issues of confidentiality. It turns out that process algebras themselves can be designed with synchronous parallel composition as the central notion. In such a vision, the choice operator `$+$' is an $ACUID$-operator, parallel synchronous composition will be distributive over choice, and process algebras can be specified over a $PACUID$ signature obtained by augmenting $ACUID$ with action prefixes. Bisimulation between processes reduces then to congruence over the $PACUID$-equational theory. Information flow analysis is finer when based on bisimulation on such a synchronous algebra, than when it is based on trace or weak bisimulation equivalence. Issues such as confidentiality can be formulated exclusively in terms of synchronous composition, in the $PACUID$-syntax. We present a DEXPTIME algorithm in this synchronous syntax for deciding such problems.
Mot(s) Clé(s) : Process Algebras, Value-Passing, Secrecy Analysis, Cryptography
Les rapports de recherche du LIFO en 2003
RR-2003-01
A Synchronous Bisimulation-Based Approach for Information Flow Analysis
S. ANANTHARAMAN, G. HAINS
Date : 2003-02-24
Résumé Télécharger
RR-2003-02
AC(U)ID-Unification is NEXPTIME-Decidable
S. ANANTHARAMAN, P. NARENDRAN, M. RUSINOWITCH.
Date : 2003-04-01
Résumé Télécharger
RR-2003-03
Learning Characteristic Rules Relying on Quantified Paths
Teddy Turmeaux, Ansaf Salleb, Christel Vrain, Daniel Cassard
Date : 2003-05-13
Résumé Télécharger
RR-2003-04
Intermediate (Learned) Consistencies
Arnaud Lallouet, Andrei Legtchenko, Thi-Bich-Hanh Dao, AbdelAli Ed-Dbali
Date : 2003-08-01
Résumé Télécharger
RR-2003-05
A Synchronous Calculus for Secrecy Analysis
Siva ANANTHARAMAN, Jing CHEN, Gaétan HAINS, Paliath NARENDRAN
Date : 2003-10-23
Résumé Télécharger
Résumés des rapports de recherche
RR-2003-01 A Synchronous Bisimulation-Based Approach for Information Flow Analysis
S. ANANTHARAMAN, G. HAINS
Résumé : Nous définissons une algèbre de processus dont la composition parallèle réalise une communication synchrone. Elle diffère de CCS essentiellement par l'hypothèse d'observabilité de la durée des actions internes. L'analyse de flot d'information dans notre formalisme est donc centrée sur la bisimulation forte plutôt que sur l'équivalence de traces ou sur la bisimulation faible. Dans notre théorie la bisimulation se réduit à l'égalité dans une théorie ACUID étendue avec un opérateur de préfixe. Nous montrons que l'analyse de flot d'information dans ce formalisme est plus fine que celles fondées sur les traces ou la bisimulation faible.
Mot(s) Clé(s) : flot d'information, bisimulation forte, protocoles cryptographiques
RR-2003-02 AC(U)ID-Unification is NEXPTIME-Decidable
S. ANANTHARAMAN, P. NARENDRAN, M. RUSINOWITCH.
Résumé : In an earlier work, we considered the theory AC(U)ID_l obtained by adjoining a binary symbol `*' which is assumed left-distributive over a basic AC(U)I-operator `+'; we showed there that AC(U)ID_l-unification is NEXPTIME-decidable and DEXPTIME-hard. In this paper we consider unification over AC(U)ID, where the the binary symbol adjoined `*' is assumed two-sided distributive over the AC(U)I-operator `+'. We formulate the problem as one of solving a particular class of set constraints, and propose a method for solving it in terms of the language of a labeled dag automaton associated to the problem. AC(U)ID-unification is thus shown to be NEXPTIME-decidable; it is also shown to be DEXPTIME-hard via other considerations.
Mot(s) Clé(s) : E-Unification, Complexity, Set constraints, Tree automata, Dag automata, Labeled dag automata.
RR-2003-03 Learning Characteristic Rules Relying on Quantified Paths
Teddy Turmeaux, Ansaf Salleb, Christel Vrain, Daniel Cassard
Résumé : La caractérisation est une tâche supervisée de fouille de données qui permet de résumer de manière succincte et concise un ensemble de données. Cette tâche est intéressante dans la mesure où elle ne nécessite pas de contre exemples. Nous proposons un cadre général pour la caractérisation d'un ensemble d'objets, appelé ensemble 'cible', en nous basant non seulement sur leurs propriétés propres mais aussi sur les propriétés des objets qui leur sont liés. Selon le type des objets considérés, différents liens peuvent être envisagés. Dans le cas de bases de données géographiques, ce sont les relations spatiales qui expriment des liens entre objets géoréférencés. Nous proposons 'Caracterix' un nouvel algorithme d'extraction de règles de caractérisation et nous montrons son application à des données géographiques réelles fournies par le BRGM.
Mot(s) Clé(s) : Aprentissage; fouille de données; règles caractéristiques; bases de données relationnelles; bases de données spatiales
RR-2003-04 Intermediate (Learned) Consistencies
Arnaud Lallouet, Andrei Legtchenko, Thi-Bich-Hanh Dao, AbdelAli Ed-Dbali
Résumé : What makes a good consistency ? Depending on the constraint, it may be a good pruning power or a low computational cost. By using machine learning techniques (search in an hypothesis space and clustering), we propose to define new automatically generated solvers which form a sequence of consistencies intermediate between bound- and arc-consistency. By associating to a consistency its quality, we define a method which allows, from a set of consistencies, to determine the best one to enforce for a given constraint. We apply this method on our generated intermediate consistencies. Surprisingly, traditional consistencies are not always the best choice and experiments show that learned intermediate consistencies sometimes outperform standard ones on various benchmarks according to the prediction.
Mot(s) Clé(s) : consistency; solver learning
RR-2003-05 A Synchronous Calculus for Secrecy Analysis
Siva ANANTHARAMAN, Jing CHEN, Gaétan HAINS, Paliath NARENDRAN
Résumé : Protocols are often modeled as value-passing processes in parallel composition, and their analysis based on CCS's interleaving semantics. The synchronous branches are the ones which are crucial in these models for analyzing issues of confidentiality. It turns out that process algebras themselves can be designed with synchronous parallel composition as the central notion. In such a vision, the choice operator `$+$' is an $ACUID$-operator, parallel synchronous composition will be distributive over choice, and process algebras can be specified over a $PACUID$ signature obtained by augmenting $ACUID$ with action prefixes. Bisimulation between processes reduces then to congruence over the $PACUID$-equational theory. Information flow analysis is finer when based on bisimulation on such a synchronous algebra, than when it is based on trace or weak bisimulation equivalence. Issues such as confidentiality can be formulated exclusively in terms of synchronous composition, in the $PACUID$-syntax. We present a DEXPTIME algorithm in this synchronous syntax for deciding such problems.
Mot(s) Clé(s) : Process Algebras, Value-Passing, Secrecy Analysis, Cryptography
Université d'Orléans | INSA Centre Val de Loire
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans 