********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle U/V, etage -2 * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 20 fevrier 2004 **** 9h00 --18h00 ********************** Se'minaire d'une journee sur la securite, voir le programme en : http://www.di.ens.fr/~cousot/seminaire/2004/seminaire.securite-04-02-fev.txt *** Vendredi 20 fevrier 2004 **** 9h00 ****************************** Bruno BLANCHET (ENS) Automatic Proof of Strong Secrecy for Security Protocols Re'sume': We present a new automatic technique for proving strong secrecy for security protocols. Strong secrecy means that an adversary cannot see any difference when the value of the secret changes. Our technique relies on an automatic translation of the protocol into Horn clauses, and a resolution algorithm on the clauses. It requires important extensions with respect to previous work for the proof of (standard) secrecy and authenticity. This technique can handle a wide range of cryptographic primitives, and yields proofs valid for an unbounded number of sessions and an unbounded message space; it is also flexible and efficient. We have proved its correctness and implemented it. *** Vendredi 20 fevrier 2004 **** 10h30 ***************************** Ce'dric FOURNET (Microsoft Cambridge) A Semantics for Web Services Authentication Re'sume': We consider the problem of specifying and verifying cryptographic security protocols for XML web services. The security specification WS-Sec describes a range of XML security tokens, such as username tokens, public-key certificates, and digital signature blocks, amounting to a flexible vocabulary for expressing protocols. To describe the syntax of these tokens, we extend the usual XML data model with symbolic representations of cryptographic values. We use predicates on this data model to describe the semantics of security tokens and of sample protocols distributed with the WSE implementation of WS-Sec. By embedding our data model within Abadi and Fournet's applied pi calculus, we formulate and prove security properties with respect to the standard Dolev-Yao threat model. Moreover, we informally discuss issues not addressed by the formal model. To the best of our knowledge, this is the first approach to the specification and verification of security protocols based on a faithful account of the XML wire format. Joint work with Karthikeyan BHARGAVAN and Andrew D. GORDON Slides and draft papers are available from http://securing.ws and http://research.microsoft.com/~fournet *** Vendredi 20 fevrier 2004 **** 14h00 ***************************** Roberto GIACOBBAZZI & Isabella MASTROENI (Universita` di Verona) Abstract non-interference Re'sume': We generalize the notion of non-interference making it parametric relatively to what an attacker can analyze about the input/output information flow. The idea is to consider attackers as data-flow analyzers, whose task is to reveal properties of confidential resources by analyzing public ones. This means that no unauthorized flow of information is possible from confidential to public data, relatively to the degree of precision of an attacker. In this way we make the security degree a program a property of its semantics. We introduce systematic methods for extracting attackers from programs, providing domain-theoretic characterizations of the most precise attackers which cannot violate the security of a given program. These methods allow us both to compare attackers and program secrecy by comparing the corresponding abstractions in the lattice of abstract interpretations, and to design automatic program certification tools for language-based security by abstract interpretation. Moreover we introduce a compositional proof-system for certifying abstract non-interference in programming languages. Assertions specify the secrecy of a program relatively to the given attacker and the proof-system specifies how these assertions can be composed in a syntax-directed a la Hoare deduction of secrecy. We prove that the proof-system is sound relatively to the standard semantics of an imperative programming language with non-deterministic choice. *** Vendredi 20 fevrier 2004 **** 15h30 ***************************** Jean GOUBAULT-LARRECQ (LSV/ENS Cachan & CNRS UMR 8643 & INRIA projet SECSI) A few points related to cryptographic protocols and automated deduction. Re'sume' : As the talk by B. Blanchet should have convinced you already, cryptographic protocols can be modeled using Horn clause formats. I'll explain how sets of general Horn clauses can be abstracted to specific decidable formats (I'll take Nielson, Nielson and Seidl's H1 class as my preferred format), and how such clause formats can be decided using automated deduction techniques, namely ordered resolution with selection and splittingless splitting---yielding optimal decision procedures; e.g., this variant of resolution runs in DEXPTIME for H1, which is known to be DEXPTIME-complete. Resolution actually provides streamlined ways of showing that several decidable classes indeed are so. I'll demonstrate the h1 tool, which decides H1 using resolution. I'll also describe various results (joint work with K.N. Verma and M. Roger) on extensions modulo equational theories, which have recently allowed us to verify the IKA.1 initial key agreement protocol of the CLIQUES protocol suite, automatically. A novelty here is that abstraction is not just effected prior to applying a resolution prover, but also during the very deduction process. If time permits, I'll also address the question of certifying cryptographic protocols, and producing actual evidence, in the form of an independently checkable Coq proof, of the security of protocols. While talking, I'll actually run h1, h1mc and some other tools of the h1 tool suite to support my claims. ********************************************************************* Pour recevoir l'annonce par courrier electronique: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************