- Contacts/Reaching LIFO
- Teaching
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
Go to Research Reports of Year : 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
Abstract : A process algebra is defined where parallel composition is structured around synchronous communication. Its essential difference with CCS is the hypothesis that internal actions must be observable for the clock; consequently, in our formalism (strong) bisimulation will be the basis for information flow analysis, instead of equivalences based on trace or weak bisimulation. Bisimulation reduces in our formalism to equality modulo an ACUID equational theory extended with prefixes. We show that information flow analysis based on our formalism is finer than analyses based on trace or weak bisimulation.
Keywords : information flow analysis, strong bisimulation, cryptographic protocols
RR-2003-02 AC(U)ID-Unification is NEXPTIME-Decidable
S. ANANTHARAMAN, P. NARENDRAN, M. RUSINOWITCH.
Abstract : 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.
Keywords : 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
Abstract : We address the characterization task that aims at finding properties shared by a given set of objects. This task is interesting for some real applications since it does not require negative examples. We present a general framework for the characterization of a target set of objects by means of their own properties, but also the properties of objects linked to them. According to the kinds of objects, various links can be considered. For instance, in the case of relational databases, associations are the straightforward links between pairs of tables. We propose CaracteriX, a new algorithm for mining characterization rules and we show how it can be used on multi-relational and spatial databases.
Keywords : Machine Learning, Data Mining, Characteristic Rules, Relational Databases, Spatial Databases.
RR-2003-04 Intermediate (Learned) Consistencies
Arnaud Lallouet, Andrei Legtchenko, Thi-Bich-Hanh Dao, AbdelAli Ed-Dbali
Abstract : 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.
Keywords : consistency; solver learning
RR-2003-05 A Synchronous Calculus for Secrecy Analysis
Siva ANANTHARAMAN, Jing CHEN, Gaétan HAINS, Paliath NARENDRAN
Abstract : 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.
Keywords : Process Algebras, Value-Passing, Secrecy Analysis, Cryptography
LIFO Research Report for Year 2003
RR-2003-01
A Synchronous Bisimulation-Based Approach for Information Flow Analysis
S. ANANTHARAMAN, G. HAINS
Date : 2003-02-24
Abstract Download
RR-2003-02
AC(U)ID-Unification is NEXPTIME-Decidable
S. ANANTHARAMAN, P. NARENDRAN, M. RUSINOWITCH.
Date : 2003-04-01
Abstract Download
RR-2003-03
Learning Characteristic Rules Relying on Quantified Paths
Teddy Turmeaux, Ansaf Salleb, Christel Vrain, Daniel Cassard
Date : 2003-05-13
Abstract Download
RR-2003-04
Intermediate (Learned) Consistencies
Arnaud Lallouet, Andrei Legtchenko, Thi-Bich-Hanh Dao, AbdelAli Ed-Dbali
Date : 2003-08-01
Abstract Download
RR-2003-05
A Synchronous Calculus for Secrecy Analysis
Siva ANANTHARAMAN, Jing CHEN, Gaétan HAINS, Paliath NARENDRAN
Date : 2003-10-23
Abstract Download
Abstracts of Research Reports
RR-2003-01 A Synchronous Bisimulation-Based Approach for Information Flow Analysis
S. ANANTHARAMAN, G. HAINS
Abstract : A process algebra is defined where parallel composition is structured around synchronous communication. Its essential difference with CCS is the hypothesis that internal actions must be observable for the clock; consequently, in our formalism (strong) bisimulation will be the basis for information flow analysis, instead of equivalences based on trace or weak bisimulation. Bisimulation reduces in our formalism to equality modulo an ACUID equational theory extended with prefixes. We show that information flow analysis based on our formalism is finer than analyses based on trace or weak bisimulation.
Keywords : information flow analysis, strong bisimulation, cryptographic protocols
RR-2003-02 AC(U)ID-Unification is NEXPTIME-Decidable
S. ANANTHARAMAN, P. NARENDRAN, M. RUSINOWITCH.
Abstract : 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.
Keywords : 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
Abstract : We address the characterization task that aims at finding properties shared by a given set of objects. This task is interesting for some real applications since it does not require negative examples. We present a general framework for the characterization of a target set of objects by means of their own properties, but also the properties of objects linked to them. According to the kinds of objects, various links can be considered. For instance, in the case of relational databases, associations are the straightforward links between pairs of tables. We propose CaracteriX, a new algorithm for mining characterization rules and we show how it can be used on multi-relational and spatial databases.
Keywords : Machine Learning, Data Mining, Characteristic Rules, Relational Databases, Spatial Databases.
RR-2003-04 Intermediate (Learned) Consistencies
Arnaud Lallouet, Andrei Legtchenko, Thi-Bich-Hanh Dao, AbdelAli Ed-Dbali
Abstract : 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.
Keywords : consistency; solver learning
RR-2003-05 A Synchronous Calculus for Secrecy Analysis
Siva ANANTHARAMAN, Jing CHEN, Gaétan HAINS, Paliath NARENDRAN
Abstract : 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.
Keywords : Process Algebras, Value-Passing, Secrecy Analysis, Cryptography
University of Orléans | INSA Centre Val de Loire
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans 