********************************************************************* *                       Ecole Normale Supe'rieure                   * *                                                                   * *                              Se'minaire                           * *                SEMANTIQUE ET INTERPRETATION ABSTRAITE             * *                              P. Cousot                            * *                                                                   * *                        Vendredi, 14h00--16h00                     * *                           Salle Celan                     * *                  DI  ENS  45 rue d'Ulm  75005 Paris               * ********************************************************************* ***  Vendredi 05 Juin 2009, 14h00-15h00 ***************************** Type Inference for Safety Type Systems with Opponent Typing Morten Dahl, Aalborg University joint work with Hans Huettel, Aalborg University Re'sume'/ Abstract: The use of safety type systems for static verification of cryptographic protocols has seen widespread use in recent years; the approach has been that of type checking. To facilitate proof generation, type inference is also a desirable property of these type systems and has been studied by a number of authors. However, it is popular for safety type systems with symmetric cryptography to employ two sets of typing rules in order to also capture the behaviour and interaction of an adversary. This complicates type inference, since there now is a choice of which rule to use. A possible approach is to redesign the type system so that the choice disappears but in this talk we show that this is not necessary: we construct a polynomial time algorithm for choosing which rule to apply in the original type system. We present our approach in the setting of the type system of Authenticity by Typing for Security Protocols by Gordon and Jeffrey, but it can be successfully applied to several safety type systems with symmetric cryptography and opponent typing. ********************************************************************* Pour recevoir l'annonce par courrier electronique: WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************