Séminaire PPS: Giuseppe Castagna le 1/12 à 11H

Bonjour à tous,

Jeudi prochain 1er décembre, Giuseppe Castagna nous présentera ses résultats sur le sous-typage sémantique pour le polymorphisme, publiés à ICFP 2011:

Set-theoretic Parametric Polymorphism and Subtyping

Le séminaire débutera à 11H en salle 1D23 et sera précédé, comme c'est la tradition, par un pot informel pour nous retrouver autour de thé, café et croissants.

Plus de détails sur le séminaire à http://www.pps.jussieu.fr/seminaire.

Amicalement,

Alexis

Set-theoretic Parametric Polymorphism and Subtyping
Giuseppe Castagna (PPS)
Jeudi 1er décembre 2011, 11h salle 1D23
(joint work with Zhiwu Xu)

We define and study parametric polymorphism for a type system with recursive, product, union, intersection, negation, and function types. We first recall why the definition of such a system was considered hard —when not impossible— and then present the main ideas at the basis of our solution. In particular, we introduce the notion of "convexity" on which our solution is built up and discuss its connections with parametricity as defined by Reynolds to whose study our might shed new light.

--

Alexis Saurin
Chargé de Recherche CNRS
Laboratoire PPS, UMR 7126
Équipe PiR2
CNRS, Université Paris Diderot et INRIA
alexis.saurin@pps.jussieu.fr
http://www.pps.jussieu.fr/~saurin

Séminaire PPS: Stéphanie Delaune le 17/11 à 11H (demain!)

Bonjour à tous,

Demain jeudi 17 novembre, nous accueillerons Stéphanie Delaune du LSV (ENS Cachan) qui nous présentera un exposé intitulé. Le séminaire débutera à 11H en salle 1D23 et sera précédé, comme c'est la tradition, par un pot informel pour nous retrouver autour de thé, café et croissants.

 

Plus de détails sur le séminaire à http://www.pps.jussieu.fr/seminaire.

Amicalement,

Alexis

Analysing security protocols using process algebra
Stéphanie Delaune
(LSV, ENS Cachan)
Jeudi 17 novembre 2011, 11h salle 1D23

Abstract:
Security is a very old concern, which until quite recently was mostly of interest for military purposes. The deployment of electronic commerce changes this drastically. The security of exchanges is ensured by cryptographic protocols which are  notoriously  error prone. The formal verification of cryptographic protocols is a difficult problem that can be seen as a particular model-checking problem in an hostile environment. Many results and tools have been developed to automatically verify cryptographic protocols.

Recently, new type of applications have emerged, in order to face new technological and societal challenges, e.g. electronic voting protocols,  electronic passport, ... These applications involve some features that are not taken into account by the existing verification tools, e.g. complex cryptographic primitives, privacy-type security properties, ... This prevents us from modelling these protocols in an accurate way. Moreover, protocols are often analysed  in isolation and this is  well-known to be not sufficient. In this talk, I will present you an attack that has been recently discovered on the French version of the e-passport. We will see how formal methods and process algebra can be used to study different aspects concerning the verification of cryptographic protocols.

--
Alexis Saurin
Chargé de Recherche CNRS
Laboratoire PPS, UMR 7126
Équipe PiR2
CNRS, Université paris Diderot et INRIA
alexis.saurin@pps.jussieu.fr
http://www.pps.jussieu.fr/~saurin