Salle E12, Bâtiment IIIA-LIFO (1er Etage)
Faculté des Sciences (Univ. d'ORLEANS)
"Common Knowledge: Now You Have it, Now You Don't."
Moshe Y. VARDI (Rice University, USA).
The notion of common knowledge, where everyone knows, everyone knows that everyone knows, etc., has proven to be fundamental in various disciplines, including Artificial Intelligence, Economics, Game Theory, Psychology, and Distributed Computer Systems. Common knowledge seems to present us with a paradox. On one hand, common knowledge is necessary for agreements and for coordination. On the other hand, common knowledge is unattainable in the real world. In this expository talk we describe the paradox and various approaches to its resolution.
This talk represents joint work with R. FAGIN, J.Y. HALPERN, and Y. MOSES.
``Security properties: Two Agents are Sufficient''
Véronique CORTIER, Laboratoire LSV, ENS-Cachan.
The task of automatically verifying cryptographic protocols has now been
undertaken by several research groups, because of its relevance to secure
internet transactions.
We consider arbitrary cryptographic protocols and security properties. We
show that it is always sufficient to consider a bounded number of agents b
(actually b=2 in most of the cases): if there is an attack involving n
agents, then there is an attack involving at most b agents.
Such a result is useful for automatic tools: we may forget the universal
quantifications on agents ids and consider finitely many (4 most of the
time) instances of the protocol roles, without losing information.
This talk represents work done jointly with Hubert COMON.
``Timed Rewrite Systems''
Rachid ECHAHED, IMAG, Grenoble.
We propose an efficient operational semantics for a new class of
rewrite systems, named Timed Rewrite Systems. This class
constitutes a conservative extension of first order conditional term
rewrite systems together with time features such as clocks, signals,
timed terms,timed atoms and timed rules. We define first Timed Rewrite
Systems and illustrate them through some examples. A naive approach to the
operational semantics is very costly in space. We propose, for a large
class of programs, an improved calculus with a linear space
complexity. Finally, we show how our framework compares to related
work.
This talk represents work done jointly with J. BLANC.
``On Model checking durational Kripke structures"
This talk represents work done jointly with Philippe SCHNOEBELEN and
Nicolas MARKEY.
``CASRUL: A Constraint Solver for Detecting Protocol Insecurity''
This talk represents work done jointly with Michael RUSINOWITCH.
``Model-checking Mobile Ambients''
The ambient logic [CardelliGordon00] is a modal logic designed to
specify properties of distributed and mobile computations programmed
in the ambient calculus. As well as standard temporal modalities for
describing the evolution of ambient processes, the logic includes
novel spatial modalities for describing the tree structure of ambient
processes.
In this talk, I will discuss about decidability and complexity issues
for the model-checking problem for fragments of the ambient calculus
wrt the ambient logic.
This talk represents work done jointly with Witold CHARATONIK,
Sivano Dal ZILIO, Andrew D. GORDON, Supratik MUKHOPADHYAY.
``Invariants inductifs dans un système temporisé''
Ce travail a été effectué lors d'un séjour au SRI et a bénéficié de
discussions avec Natarajan SHANKAR, Henny SIPMA et Tomas URIBE.
``Elements for a Reconfigurable Theory for Sat-based Formal Methods''
``SOCLE: Achieving Security using OCL Extensions''
This talk represents work done jointly with Gaétan HAINS.
``Modèle du temps causal et son utilisation dans la spécification
et vérification de systèmes à contraintes temporelles''
Travail en commun avec F.POMMEREAU et C.BUI THANH.
``Analyse de non-interférence pour processus mobiles par abstraction
de sortes''
``Model-checking security requirements of cryptographic protocols''
This talk represents work done jointly with Stéphane LAFRANCE.
François LAROUSSINIE, Laboratoire LSV, ENS-Cachan.
We consider quantitative model checking in durational Kripke structures
(Kripke structures where transitions have integer durations) with
timed temporal logics where subscripts put quantitative constraints on the
time it takes before a property is satisfied.
We investigate the conditions that allow polynomial-time model checking
algorithms for timed versions of CTL and exhibit an important gap between
logics where subscripts of the form ``=c'' (exact duration) are allowed,
and simpler logics that only allow subscripts of the form ``
Mathieu TURUANI, CASSIS, LORIA - INRIA-Lorraine.
Even assuming perfect cryptography, the design of protocols for secure
electronic transactions is highly error-prone and conventional
validation techniques based on informal arguments and/or testing are not
sufficient for meeting the required security level. We present the
CASRUL tools for analyzing cryptographic protocols specifications in a
model where an intruder has complete control of the communications
network. The corresponding protocol insecurity problem will be shown to
be NP-Complete even for one session and one principal.
Jean-Marc TALBOT, Laboratoire LIFL, Université USTL, Lille.
The ambient calculus [CardelliGordon98a] is a formalism for describing
the mobility of both software and hardware. An ambient is a named
cluster of running processes and nested sub-ambients. Each
computation state has a spatial structure, the tree induced by the
nesting of ambients. Mobility is abstractly represented by
re-arrangement of this tree: an ambient may move inside or outside
other ambients or may dissolve another ambient.
Jean-François MONIN, France Télécom R&D.
La séparation entre transitions continues et transitions discrètes,
joue un rôle fondamental dans la manipulation des systèmes
temporisés. Curieusement, il semble qu'on ne puisse pas en général
effectuer complètement cette séparation lorsqu'on cherche à
démontrer des invariants par induction sur les traces. Une solution
minimisant l'interaction entre transitions discrètes et continues
est proposée. L'étude est illustrée sur trois variantes de la preuve
de correction d'un algorithme qui gère un échéancier en temps-réel.
Daniel SINGER, Laboratoire LITA, Université de Metz.
As Sat based methods become more and more popular in a wide range of areas,
it is increasingly necessary to answer some questions in a sytematic way.
This paper presents some elements of the State-of-the-Art Sat solvers and
possible future research directions along with an updated and annotated
bibliography. The recent progress of the enumerative Davis Logemann Loveland,
of the resolution Davis-Putnam, the Stalmarck's method and of the OBDD
based algorithms give some idea of the future platform for Programming
in Propositional Logic.
The translation-encoding, the Data Structures efficiency, the "best"
variables ordering, the learning questions are dicussed with the
Space and Time trade-off for a number of applications such as Bounded Model
Checking or Cryptography.
Mathieu BERGERON, Laboratoire CRAC, Ecole Polytechnique, Montréal (Canada).
The SOCLE project aims at enforcing a security policy expressed in an
extension of OCL (Object Constraint Language) on a UML (Unified Modeling
Language) software design. Formal semantics are given both to UML diagrams
and OCL constraints in such a way that verification is decidable by
model-checking techniques.
At design-time, subtle security properties such as non-interference
are to be verified and diagnosed.
As development is pursued, design is to be enforced by verifying that
an abstraction of the implementation can simulate an annotation version
of the design model where security critical resources (e.g. files,
sockets) are distinguished. We belive that such an approach is
applicable to industrial software development and can significantly
improve software reliability and security.
Hanna KLAUDEL, Université PARIS-XII.
Nous présentons une nouvelle approche pour modéliser des systèmes
à contraintes temporelles (discrètes):
- par des réseaux de Petri sans temps,
- de façon compositionnelle,
- en préservant la concurrence.
Nous comparons (sur un exemple) cette approche à celle
qui utilise les automates temporisés et nous
montrons les résultats de vérification (très encourageants)
obtenus avec des outils fonctionnant sur les automates (Uppaal et Kronos)
et ceux obtenus avec des outils travaillant avec les réseaux
de Petri (PEP et Maria). Nous présentons les perspectives possibles de ce
travail et discutons aussi quelques questions ouvertes.
Frédéric PROST, Laboratoire LEIBNIZ, IMAG-Grenoble.
Nous introduisons un nouveau calcul de processus mobiles inspiré du calcul
bleue de Boudol. Nous lui donnons un système de types dans la droite ligne des
systèmes "standard" des calculs fonctionnels, c'est-à-dire où les types
reflètent la structure des termes. Nous montrons comment utiliser ce système de
types pour obtenir une analyse statique polyvariante, et donnons un résultat de
non-interférence qui peut être utilisé dans de nombreuses applications
(confidentialité, code mort, analyse des temps de liaison etc.).
John MULLINS, Laboratoire CRAC, Ecole Polytechnique, Montréal (Canada).
In this talk, we propose presentations for most of the properties of
information transmitted by cryptographic protocols, in terms of
admissible information flow properties. The novelty of our approach lies
in these security property presentations. This leads to a sound and
complete bisimulation-based verification method of these properties.
We present this method together with illustrations through analyses of
confidentiality, authentication and robustness to denial of service
attacks performed on some paradigmatic protocols.
Programme prévisionnel
Vers la page d'appel à participation