Lifo - Laboratoire d'Informatique Fondamentale d'orléans INSA Centre Val de Loire Université d'Orléans Université d'Orléans

Lifo > Research Actions at LIFO > Research Action : ACI SATIN

 Site en Français


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 70 11
Fax: +33 (0)2 38 41 71 37

ACI SATIN : Security Analysis for Trusted Infrastructures and Network protocols

Designing secure communication systems is a challenging problem. Severe attacks can be conducted just by exploiting the inherent weakness of communication protocols themselves. Such attacks are simply overlooked at the design level, as it is difficult to determine even after careful inspection all the complex ways in which different agents could be interleaved with the infering actions of a malicious intruder. This pinpoints the need for expressive tools capable of analysing efficiently the information flow distributed between the different interacting agents. Process algebras and related rewriting techniques are well-suited formalism for such a purpose. For instance, the confidentiality and authentification analysis of cryptographic protocols can be based on suitable observation criteria, such as the large scale distribution of dynamic access control policies over trusted operating systems. Several interesting security analysis results have recently been obtained in these directions, but some fundamental issues remain before these results can be applied to practical problems of industrial type: more efficient decision procedures and closer approximation results, taking into account the incidence of time, modeling imperfect cryptographic primitives and the notion of denial of service suitability to consider attacks based on them.

The SATIN project is presented by researchers with complementary competences in security and formal methods. Our intention is to take up the challenge of formal analysis and design of secure distributed systems, by taking advantage of the recent advances in algebraic modeling techniques, constraint solving, tree automata, and observation criteria for concurent systems. The feedbacks from our industrial partners, namely CEA-DAM and France Telecom RD, will naturally be of importance in validating the results obtained at very stage of the project.

Participating Members



Gaétan HAINS

Pierre RETY

Christian TOINARD

Action's Web Page