To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 09/11/07 - Paris - FR

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

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                         Vendredi 9 novembre, 10h30

                               -------------
                               Nataliya Guts
                               -------------

                                 MSR-INRIA

                ===========================================
                A Formal Implementation of Value Commitment
                ===========================================

In an optimistic approach to security, one can often simplify protocol design
by relying on audit logs, which can be analyzed a posteriori. Such auditing is
widely used in practice, but no formal studies guarantee that the log
information suffices to reconstruct past runs of the protocol, to reliably
detect, and provide evidence of, any cheating. We formalize audit logs for a
sample optimistic scheme, the value commitment. It is specified in a pi
calculus extended with committable locations, and compiled using standard
cryptography to implement secure logs. We show that our distributed
implementation either respects the semantics of commitments or, using the
information stored in the logs, detects cheating by a hostile environment.

Joint work with Cédric Fournet (MSR) and Francesco Zappa Nardelli (INRIA).