To: seminaire@pauillac.inria.fr
From: Bruno.Barras@inria.fr
Subject: SEM - INRIA : LogiCal - 17/01/03 - Paris - FR

      Vous pouvez maintenant vous abonner à nos annonces de séminaires
             http://pauillac.inria.fr/seminaires/subscribe.html


                             S E M I N A I R E
                                         . ___ 
                           /   _   _      /   _   /
                          /   / \ / \  / /   __| /
                         |___ |_/ |_/ / |__ |_/ |_
       ___      .                  /    
      /    ___   __  /_  _   /   _/        /| /|  _   __ __ _       _ 
     /    /   / /_  /   __| /             / |/ | / \ /_ /  / \ | / __|
    |___ /   / __/ |_  |_/ |_            /     | |_/__/ |_ |_/ |/ |_/
                                                
                          I N R I A - Rocquencourt
                       Salle de conference du Bat 11

                         Vendredi 17 janvier, 10h30

                                -----------
                                Dale Miller
                                -----------

                    INRIA/FUTURS and Ecole Polytechnique

                     ==================================
                     Encryption as an Abstract Datatype
                     ==================================

    Specifying  and   analyzing  security  protocols   is  notoriously
    difficult on many levels.  One approach to dividing up the work of
    such analysis uses what is  commonly called the Dolev-Yao model of
    security execution  and attack.  It  has been observed  by various
    people recently,  that this abstraction  can be captured  in large
    part  by  multiset  rewriting   augmented  with  a  mechanism  for
    generating new symbols  to be used for new  nonces and session and
    encryption keys.  Proof search (logic programming) in linear logic
    can  capture both  multiset rewriting  and the  generation  of new
    symbols via  the proof  theoretical device of  eigenvariables.  We
    shall examine  such encodings  into linear logic  and look  at how
    encryption can  be viewed  as an abstract  data type and  what the
    meta-theory of linear logic can tell us about protocols.