********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle W, 4e`me e'tage, toits du DMI * * DMI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 4 juin 1999 **** 14h00 ********************************* Methodes semantiques pour l'analyse de protocoles cryptographiques David MONNIAUX (LIENS) Re'sume' : De plus en plus de services reseau comprennent des procedures plus ou moins importantes pour assurer la securite des communications. Meme si les composants de base de ces procedures (primitives cryptographiques) sont corrects, des attaques astucieuses peuvent parfois mettre en echec la securite. Le concepteur de systemes distribues doit donc prendre en compte la possibilite de telles attaques; parallelement, pour des raisons d'efficacite, il ne doit pas surcharger le systeme par une trop grande quantite de calculs. Differentes approches de demonstration formelle ont ete proposees: certaines visent a formaliser les "demonstrations intuitives" qui justifient le fonctionnement de tel ou tel protocole; d'autres definissent un modele ideal et demontrent des proprietes sur celui-ci, plus ou moins automatiquement. J'evoquerai pour la premiere approche une methode entierement automatique de demonstration des proprietes dans les systemes formels de type BAN ou GNY, deja operationnel; pour la seconde approche, il sera presente une analyse par interpretation abstraite, pour laquelle subsistent des problemes d'implementation. *** Vendredi 11 juin 1999 **** 14h00 ******************************** Binary Decision Graphs: "BDDs" for Infinite Functions Laurent MAUBORGNE (LIENS) Re'sume' : Binary Decision Graphs are a new extension of Binary Decision Diagrams that can represent some infinite boolean functions. Three refinements of BDGs corresponding to classes of infinite functions of increasing complexity are presented. The first one is closed by intersection and union, the second one by intersection, and the last one by all boolean operations. The first two classes give rise to a canonical representation, which, when restricted to finite functions, are the classical BDDs. Those classes are described in detail to be actually implemented. The last class just shows the scope of the representations. To achieve the representation, new insights on the notion of variable names and the possibility of sharing variable names are given. These insights can be of interest in the case of finite functions. *** Vendredi 18 juin 1999 **** 14h00 ******************************** Quelques idees en verification de protocoles cryptographiques Jean GOUBAULT-LARRECQ et Nabil EL KADHI (Dyade) Re'sume' : Apres une rapide presentation de la problematique de la verification de protocoles cryptographiques, et apres avoir rappele l'approche Bolignano-Paulson en ce domaine, on donnera deux pistes permettant de l'automatiser. La premiere utilise des automates d'arbre pour representer l'etat de connaissance possible de l'intrus. Ceci se rapproche de la proposition recente de David Monniaux, avec quelques differences cependant. Bien que la complexite dans le pire des cas soit exponentielle en la taille du protocole de depart, les protocoles usuels semblent suffisamment petits pour passer sans probleme majeur de performance. La deuxieme utilise une adaptation d'une approche deductive, mais ou le treillis des etats possibles de connaissance de l'intrus est beaucoup plus contraint, et ou l'analyse du protocole est en consequence beaucoup moins exacte. L'optique dans laquelle cette approche est envisagee est l'analyse automatique d'applets JavaCard dans le but d'assurer la preservation de confidentialite de donnees sensibles. *** Vendredi 18 juin 1999 **** 14h00 ******************************** Program Analysis in (Narrowing-Based) Functional Logic Languages Salvador LUCAS ALBA (Departamento de Sistemas Informaticos y Computacion Universidad Politecnica de Valencia, Espagne) Re'sume' : The analysis of functional logic programs is one of the most challenging problems in declarative programming. We discuss a general approach for formulating and analyzing arbitrary properties of functional logic programs. We provide a semantics for the denotational description of narrowing-based functional logic programs which can be used for analyzing properties of functional logic programs in an arbitrary (narrowing-based) operational framework. *** Vendredi 25 juin 1999 **** 14h00 ******************************** relache (IFIP WG 2.3) ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr WWW: http://www.dmi.ens.fr/~cousot/annonceseminaire.html *********************************************************************