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
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