*********************************************************************
* 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
*********************************************************************