To: seminaire@pauillac.inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Cristal - 03/12/04 - Paris - FR

           Vous pouvez 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 conférences du bâtiment 7

                         Vendredi 3 decembre, 14h00

                               --------------
                               Cédric Fournet
                               --------------

                             Microsoft Research

                      ===============================
                      Verifying Web Services Security
                      ===============================


We consider the problem of verifying cryptographic security protocols
in the context of Web Services. The WS-Security standard specifies a
range of XML security elements, such as username tokens and digital
signatures, amounting to a flexible vocabulary for expressing
protocols.  This flexibility is problematic for security: home-grown
protocols often go wrong.

To describe the messages exchanged by these protocols, we extend the
usual XML data model with symbolic cryptography, and develop a series
of predicates that reflect their processing. By combining these
predicates, we precisely model protocols distributed with the
Microsoft WSE implementation of WS-Security. By embedding our data
model in the applied pi calculus, we formulate security properties
against a standard Dolev-Yao attacker that can intercept and rewrite
all XML messages. We automatically check these properties using
protocol verifiers.

Relying on WS-Security, the WS-SecurityPolicy specification provides a
declarative configuration language for selecting security mechanisms
in web services implementations. Accordingly, we develop a formal
semantics for WS-SecurityPolicy, propose a more abstract link language
for specifying security goals for web services and their clients, and
establish the correctness of families of policies. We finally present
a series of automatic tools for WSE that can (1) produce policy files
from link specifications, and (2) verify whether a set of policy files
correctly implements the goals of a link specification.

This is joint work with Karthikeyan Bhargavan and Andrew D. Gordon.

Papers, details, and tools available from http://securing.ws and
http://research.microsoft.com/~fournet