%latex $1.tex % bibtex one % bibtex two % latex $1.tex % latex $1.tex \newif\ifenglish \englishfalse \documentclass[10pt]{article} \usepackage{times} \ifenglish\else \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} \fi \usepackage[francais,english]{babel} \usepackage{multirow} \usepackage{titlesec} \usepackage{url} \usepackage{array} \usepackage{fullpage} \usepackage{multibib} \makeatletter \let\savemultibiblio\thebibliography \let\endsavemultibiblio\endthebibliography \let\@savemultibibitem\@bibitem \let\@lsavemultibibitem\@lbibitem \makeatother \usepackage[export]{splitbib} \newcites{one}{~} \newcites{two}{~} \begin{category}{\franglais{Revues internationales}{International Journals}} \begin{category}{2007} \SBentries{LLT-icomp07} \end{category} \begin{category}{2006} \SBentries{CDL05-survey} \end{category} \end{category} \begin{category}{\franglais{Revue internationale électronique }{International Conferences}} \begin{category}{2007} \SBentries{Laf-secret06} \end{category} \end{category} \begin{category}{\franglais{Conf\'erences internationales}{International Conferences}} \begin{category}{2006} \SBentries{DLLT-ICALP2006} \end{category} \begin{category}{2005} \SBentries{LLT-rta2005} \end{category} \end{category} \begin{category}{\franglais{Th\`ese}{Thesis}} \begin{category}{2006} \SBentries{THESE-lafourcade06} \end{category} \end{category} \begin{category}{\franglais{Autres publications}{Other Publications}} \begin{category}{2007} \end{category} \begin{category}{2006} \SBentries{LLT-unif2006} \end{category} \begin{category}{2005} \SBentries{LSV:05:19,LSV:05:20,LSV:05:21} \end{category} \begin{category}{2004} \SBentries{LSV:04:16} \end{category} \begin{category}{2003} \SBentries{Lafourcade-DEA} \end{category} \end{category} \begin{category}{\franglais{Soumissions à des revues internationales}{International Journals}} \begin{category}{2007} \SBentries{LSV:06:17,KL-eth07} \end{category} \end{category} \begin{category}{\franglais{Rapports de Contrats}{Contract Reports}} \begin{category}{2007} \SBentries{DGA:rap1} \end{category} \begin{category}{2005} \SBentries{Prouve:rap5} \end{category} \begin{category}{2004} \SBentries{Prouve:rap1,Prouve:rap2,Prouve:rap4} \end{category} \end{category} \begingroup \selectlanguage{english} \def\bibname{}\def\chapter#1{} \def\href#1#2{#2} \long\def\franglais#1#2{\ifenglish \selectlanguage{english}#2\else \selectlanguage{francais}#1\fi} \begin{document} \ifenglish \selectlanguage{english} \else \selectlanguage{francais} \fi \newcommand{\ligne}{\vrule width \textwidth height 0.5mm} \newif\ifenglish \englishfalse \thispagestyle{empty} \pagenumbering{roman} \vspace{1em} \begin{center} ~\vfill \bigskip \bigskip {\protect\hbox{\protect\makebox[0pt][l]{\protect\rule{\textwidth}{0.7mm}}}% \protect\vskip -.8\baselineskip\protect\hbox to \textwidth{\hrulefill}} {\LARGE \scshape Dossier de candidature \\ \bigskip aux fonctions de ma\^itre de conférences \\ \bigskip Section : 27 \\ \bigskip Numéro : 0595 \\ \bigskip Etablissement : Université GRENOBLE I \\ \bigskip \bigskip \bigskip \bigskip { \bf Pascal Lafourcade}}\\ {\protect\hbox{\protect\makebox[0pt][l]{\protect\rule{\textwidth}{0.7mm}}} \protect\vskip -1.28\baselineskip\protect\hbox to \textwidth{\hrulefill}} \vfill \end{center} \cleardoublepage{} \newpage \ \newpage \tableofcontents \cleardoublepage{} \newpage \pagenumbering{arabic} \newcommand{\subsectCV}[1]{\section*{#1~\hrulefill}} \newcommand{\mydescr}[1]{\parbox{6em}{\it #1}} \newpage \ \newpage \renewcommand{\subsectCV}[1]{\subsection*{#1~\hrulefill}\addcontentsline{toc}{subsection}{#1}} \section{Curriculum Vitae.} \vspace{-.25cm} \subsectCV{Identité.} \parbox{20em}{\vspace{-.5cm} \begin{description} \item[\hspace{-.5cm}\mydescr{Nom:}] \hspace{-.5cm}\textsc{Lafourcade} \item[\hspace{-.5cm}\mydescr{Prénom:}] \hspace{-.55cm} Pascal \item[\hspace{-.5cm}\mydescr{Né le :}] \hspace{-.55cm} 26 Avril 1977 à Toulouse (31) \item[\hspace{-.5cm}\mydescr{Nationalité:}]\hspace{-.4cm}Fran\c{c}aise \item[\hspace{-.5cm}\mydescr{État civil:}]\hspace{-.4cm}Célibataire \item[\hspace{-.5cm}\mydescr{Émail:}]\hspace{-.4cm}pascal.lafourcade@inf.ethz.ch \item[\hspace{-.5cm}\mydescr{Page web:}]\hspace{-.4cm}www.inf.ethz.ch/personal/pascall/ \end{description}} \hfill \ \hfill\fbox{\parbox{13em}{ {\bf Adresse professionnelle:}\vspace{0ex}\\ Pascal \textsc{Lafourcade}\\ Information Security\\ ETH Zürich, IFW C 46.1\\ Haldeneggsteig 4 \\ CH-8092 Z\"urich, Suisse\\ Téléphone : +41 44 632 72 72\\ Portable \hspace{.25cm} : +41 78 878 83 54\\ Fax \hspace{.88cm} : +41 44 632 11 72 }} \vspace{-.5cm} \subsectCV{Fonctions occupées.} \begin{description} \item[Oct 2006 - :]Boursier DGA/CNRS, post-doctorant à l'ETH Z\"urich, dans l'équipe Information Security de D.~\textsc{Basin}. \item[Oct 2003 - Oct 2006 :]Moniteur à l'université Paris XII (C.I.E.S. de Jussieu) et allocataire de recherche au Laboratoire Spécification et Vérification de Cachan (LSV, 2 ans) et au Laboratoire d'Informatique Fondamentale de Marseille (LIF, 1 an), dans le cadre de l'ACI Sécurité Rossignol. \item[Sept 2001 - Ao\^ut 2003 :] Emploi jeune au sein du Basket Labège Auzeville Club (temps plein en parallèle du cursus universitaire). \end{description} \vspace{-.3cm} \subsectCV{Diplômes.} \begin{description} \item[Doctorat de l'École Normale Supérieure de Cachan :] Débuté le 1er Octobre 2003, soutenu le 25 Septembre 2006 à Cachan, mention {\it Très Honorable}. \item[\emph{Sujet :}]{\it<< Vérification de protocoles cryptographiques en présence de théories équationnelles.>> } \item[\emph{Président}] \hspace{.45cm} Claude \textsc{Kirchner}, Directeur de recherche au LORIA (Nancy). \item[\emph{Rapporteurs}] \hspace{0cm} Luca \textsc{Viganò}, Chercheur à l'ETH (Zürich, Suisse). \item[~]\hspace{1.7cm} Yassine \textsc{Lakhnech}, Professeur à l'Université Joseph Fourier (Grenoble). \item[\emph{Examinateur}] Yannick \textsc{Chevalier}, Maître de conférence à l'UPS (Toulouse III). \item[\emph{Directeurs}] \hspace{.35cm} Denis \textsc{Lugiez}, Professeur à l'Université Aix-Marseille I. \item[~] \hspace{1.8cm} Ralf \textsc{Treinen}, Maître de Conférence à l'ENS Cachan. \end{description} \begin{description} \item[Jan 2006 - Sept 2006 :] Diplôme Universitaire \textbf{NTCA} (Nouvelles Techniques Cognitives d'Apprentissage) de l'École Normale Supérieure de Cachan, soutenu le 29 Septembre 2006, mention {\it Assez-Bien}. \item[1998-2003 :] Étudiant à l'Université Paul Sabatier (Toulouse III). \begin{itemize} \item[2003 :] \textbf{D.E.A.} Représentation de la Connaissance et Formalisation du Raisonnement. Stage de recherche effectué à l'IRIT, sur ``\emph{l'application de la résolution de conflits ``logiques'', à l'aide à la décision pour la résolution de conflits des problèmes d'ordonnancement}''. Co-encadré par Claudette \textsc{Cayrol}, Hélène \textsc{Fargier} et Marie-Christine \textsc{Lagasquie-Schiex}, mention \emph{Assez-Bien}. \item[2002 :] \textbf{Ma\^itrise} d'informatique, mention \emph{Bien} (option : analyse d'images et intelligence artificielle). \item[2001 :] \textbf{Ma\^itrise} de mathématiques fondamentales (mémoire sur la théorie des n{\oe}uds). \item[] \hspace{.6cm} \textbf{Licence} d'informatique, mention \emph{Bien}. \item[1999 :] \textbf{Licence} de mathématiques fondamentales. \item[1997:] \textbf{DEUG} MIAS, option informatique. \end{itemize} \item[1995:] Baccalauréat Scientifique, spécialité mathématiques, mention \emph{Assez-Bien}. \end{description} \vspace{-.3cm} \subsectCV{Compétences.} \begin{description} \item[{\bf \franglais{Langues : }{Languages:} }] Fran\c{c}ais langue maternelle, anglais courant, espagnol scolaire et allemand d\'ebutant. \item[{\bf \franglais{Langages de programmation :}{Programming Languages:} }] C, Pascal, Java, Prolog, Scheme, SQL, PHP, HTML, ADA95, Maple. \item[{\bf Outils de vérification de protocoles :}] Cl-Atse, OFMC, TA4SP, SATMC, Proverif, Scyther, Hermes, Coprove. \item[{\bf Divers : }] Joueur et entraîneur de basket-ball, pilote de montgolfière, danseur (salsa, rock,...). \end{description} \newpage \section{Activités d'enseignement.} Je présente ici une vue synthétique des enseignements effectués et mon projet d'enseignement. Dans la suite de cette section, je détaille le contenu de chaque enseignement par matière et par année. \subsectCV{Assistant à l'ETH Zürich.} J'enseigne dans les cours suivants en anglais : \begin{itemize} \item << Information \& Security >> du professeur David \textsc{Basin} (24h de TD) \item << Modeling \& Simulation >> du professeur Gaston \textsc{Gonnet} (24h de TD) \end{itemize} \subsectCV{Moniteur au CIES de Jussieu, Université Paris XII.} {\bf Tutrice de monitorat} : Danièle \textsc{Beauquier}, LACL, Université Paris XII. {\bf Période} : Années universitaires 2003-2006. {\bf Durée} : 3 $\times$ 64h = 192h équivalent TD. \begin{center} Résumé des enseignements dispensés par niveaux dans le cadre du monitorat.\\ \ \\ \begin{tabular}{|c|c|c|c|} \hline Public & Intitulé & Nature & Eq TD \\ \hline 1ère Année DEUG & Initiation à la Programmation en C & TD/TP & 64h \\ \hline \multirow{4}{3cm}{ 1ère Année IUT} & Bases de données & TD & 12h \\ \cline{2-4} & Php \& Mysql & Projet & 20h \\ \cline{2-4} & Base de la Programmation en C & TD & 32h \\ \cline{2-4} & Bases de données & TD & 32h \\ \hline 2ème Année IUT & Système \& Réseau & TP & 32h \\ \hline \multicolumn{2}{c|}{~} & Total & 192h \\ \cline{3-4} \end{tabular} \end{center} \subsectCV{Autres activités d'enseignement.} \begin{description} \item[Assistant en techniques d'apprentissage : ] \ \\ \vspace{-.4cm} \begin{itemize} \item 8h TD, en 2ème Année à l'IUT d'Orsay 2006: {\it Motivation et mémorisation}. \item 8h TD, pour les moniteurs des C.I.E.S. Jussieu, Versailles et Sorbonne : {\it Émotions et motivation}, lors des Journées Apprentissage de Cachan 2006. \item 8h TD, pour les moniteurs des C.I.E.S. de Marseille : {\it Représentations mentales et motivation}, lors des Journées Apprentissage de Marseille 2006. \item 8h TD, en 1ère année de l'ESO : {\it Représentations mentales, mémorisation, émotions et motivations} 2006. \end{itemize} \item[Vacations :] 20h de TP, en 1ère Année à l'INSA Toulouse : Programmation en ADA95 (2002-2003). \item[Soutien scolaire :] professeur particulier de mathématiques pour tous les niveaux du collège au lycée, 2h à 4h par semaine (1995 - 2001). \end{description} \subsectCV{Projet d'enseignement. } Mes expériences d'enseignement m'ont permis d'aborder de nombreux sujets : sécurité informatique, modélisation et simulation, initiation à la programmation, système et réseau, bases de données. Lors de ces expériences, je me suis intégré dans plusieurs équipes pédagogiques, et j'ai pu découvrir différents fonctionnements et méthodes d'enseignement. Fort de ces expériences, j'aimerais enseigner les matières suivantes, réparties en trois catégories : \begin{itemize} \item[$\bullet$] D'une part, je suis attaché aux domaines proches de mes thèmes de recherche que sont la sécurité informatique et la vérification formelle. Actuellement, à l'ETH Z\"urich, j'enseigne avec grand plaisir dans le module ``Information Security'' à des étudiants de troisième année. Je suis prêt à m'investir dans l'élaboration d'enseignements sur des sujets connexes à mon domaine de recherche pour des étudiants de L3 ou de Master. \item[$\bullet$] D'autre part, j'ai particulièrement apprécié enseigner à un public de <<~non informaticiens~>> et leur apprendre les bases d'un langage de programmation, le fonctionnement du système et du réseau, ou encore les bases de données. Cela m'a permis de me confronter aux problèmes qu'ils rencontrent et ce défi pédagogique me passionne. Je suis donc pr\^et à enseigner l'ensemble des bases de l'informatique à des étudiants débutants en première année. \item[$\bullet$] Finalement, fort de mes expériences d'enseignement et de mes différentes interventions en techniques d'apprentissage, j'aimerais à plus long terme élaborer un projet permettant d'aider les étudiants à mieux réussir leurs études. Pour ce faire, j'envisage de construire un cours sur les techniques d'apprentissage (mémorisation, motivation...) en me basant sur les progrès scientifiques des neuro-sciences de ces dernières années. \end{itemize} Néanmoins, je suis ouvert à toutes autres propositions d'enseignement, car fort de mes diverses expériences à différents niveaux : vacations, monitorat, assistanat, j'ai appris à enseigner de nombreuses matières. Je reste donc pr\^et à m'adapter aux besoins d'enseignement de mon futur établissement. \renewcommand{\subsectCV}[1]{\subsection*{#1~\hrulefill}} \newcommand{\subsectionN}[1]{\section*{#1}\addcontentsline{toc}{subsection}{#1}} \section*{Détails des enseignements dispensés par matière et par année :}\label{sec:detail} \subsectionN{En informatique.} J'ai effectué mes enseignements en informatique en tant que : vacataire à l'INSA Toulouse durant l'année scolaire 2002-2003 et moniteur à l'université Paris XII Créteil de 2003 à 2006. Ma tutrice de monitorat était Danièle \textsc{Beauquier}, professeur à l'université Paris XII. Comme le spécifiè mon contrat de moniteur, ma première année s'est déroulée à l'université de Créteil Paris XII avec un public de DEUG MIAS 1ère année et les deux autres années ont été effectuées à l'Institut Universitaire Technologique de Fontainebleau avec des étudiants de première et deuxième année. Actuellement j'enseigne en anglais dans le cadre d'un poste d'assistant à l'ETH Z\"urich pour les cours de << Modeling \& Simulation >> et de << Information Security >>. \subsectCV{Année 2002-2003 : Vacataire à l'INSA Toulouse.} \noindent \emph{ Programmation en ADA95}~: \begin{itemize} \item \emph{Durée}~: 20 heures de TP. \item \emph{Public}~: 2 groupes de 14 étudiants en première année à l'INSA Toulouse . \item \emph{Responsable}~: Gilles \textsc{Motet} : motet@insa.univ-tlse.fr \item \emph{Description}~: Grâce au langage ADA95, les étudiants découvrent les bases de la programmation, à travers les tableaux, les conditions, les itérations, les fonctions et les procédures. \item \emph{Réalisation}~: Préparation des sujets d'examen sur machines et corrections des programmes rendus. \end{itemize} \subsectCV{Année 2003-2004 : Moniteur à l'université Paris XII Créteil.} \noindent \emph{Initiation à la Programmation en C}~: \begin{itemize} \item \emph{Durée}~: 32 heures de TD et 32 heures (eq. TD) de TP. \item \emph{Public}~: 2 groupes de 40 étudiants en première année de DEUG MIAS. \item \emph{Responsable}~: Danièle \textsc{Beauquier} : beauquier@univ-paris12 \item \emph{Description}~: Ce module a pour but d'apprendre les bases de la programmation à travers le langage C à des étudiants qui n'avaient jamais programmé et sans aucune connaissance en informatique. Les étudiants apprennent les principales notions de la programmation en informatique. En particulier, ils manipulent les notions de tableaux, itérations (boucles), conditions, chaînes de caractères et pointeurs. \item \emph{Réalisation}~: Site Web pour les étudiants avec les sujets et corrigés des TD et TP. Aide à la préparation des sujets de TP, TD et du sujet d'examen, surveillance d'examen. \end{itemize} \subsectCV{Année 2004-2005: Moniteur à l'IUT de Fontainebleau.} \noindent \emph{Bases de Données}~: \begin{itemize} \item \emph{Durée}~: 32 heures de TD. \item \emph{Public}~: 2 groupes de 22 étudiants en première année d'IUT informatique. \item \emph{Responsable}~: Régine \textsc{Laleau} : laleau@univ-paris12.fr \item \emph{Description}~: Ce module présente les bases de données grâce au langage SQL. Les étudiants abordent les concepts de clé primaire, clé étrangère, jointure naturelle, entité relation, requête, dépendance fonctionnelle, forme normale et normalisation. \item \emph{Réalisation}~: participation à l'élaboration des sujets de TP, de TD et du sujet d'examen. \end{itemize} \ \\ \noindent \emph{Système et Réseaux}~: \begin{itemize} \item \emph{Durée}~: 32 heures (eq TD) de TP. \item \emph{Public}~: 2 groupes de 16 étudiants en seconde année d'IUT informatique. \item \emph{Responsable}~: Konstantin \textsc{Verchinine} : verko@capet.iut-fbleau.fr \item \emph{Description}~: Nous introduisons les concepts de système de fichiers, tube de communication, fork, socket. Ces éléments sont ensuite utilisés pour mieux comprendre les notions de réseau. \item \emph{Réalisation}~: participation à la correction et l'évaluation des partiels sur machine. \end{itemize} \subsectCV{Année 2005-2006: Moniteur à l'IUT de Fontainebleau.} \noindent \emph{Base de la programmation en C}~: \begin{itemize} \item \emph{Durée}~: 32 heures de TD. \item \emph{Public}~: 4 groupes de 20 étudiants en première année IUT informatique. \item \emph{Responsables}~: Patrick \textsc{Ciegelski} et Luc \textsc{Hernandez}. \item \emph{Description}~: Comme son nom l'indique, il s'agit d'initier les étudiants à la programmation et à l'algorithmique via le langage C. Ils abordent ainsi les notions de tableaux, fonctions, boucles, conditions, chaînes de caractères et pointeurs. \item \emph{Réalisation}~: réalisation de l'ensemble des séances de TD. \end{itemize} \ \\ \noindent \emph{Base de données}~: \begin{itemize} \item \emph{Durée}~: 12 heures de TD. \item \emph{Public}~: 2 groupes de 20 étudiants en première année d'IUT informatique. \item \emph{Responsable}~: Régine \textsc{Laleau} : laleau@univ-paris12.fr \item \emph{Description}~: Ce module s'adresse à des étudiants de l'IUT en première année ayant déjà abordé lors du premier semestre les systèmes de gestions de bases de données en SQL et Oracle. La dépendance fonctionnelle et la normalisation sont les deux notions que nous \'etudions avec ces étudiants. \item \emph{Réalisation}~: participation à l'élaboration des TDs. \end{itemize} \ \\ \noindent \emph{Projet en Mysql \& Php}~: \begin{itemize} \item \emph{Durée}~: 20 heures (eq TD) Projet Mysql \& Php. \item \emph{Public}~: 2 groupes de 20 étudiants en première année d'IUT informatique. \item \emph{Responsables}~: Régine \textsc{Laleau} et Farida \textsc{Semmak} : laleau@univ-paris12.fr \item \emph{Description}~: Après avoir appris les bases de la programmation en Php et en base de données, les étudiants appliquent concrètement ces notions en réalisant un projet. Dans le cadre de ce projet, ils ont conçu et développé un site pour la gestion d'achat de livres en ligne. Cela va de l'analyse du problème jusqu'à la réalisation, sous forme de projet, du site. \item \emph{Réalisation}~: participation à l'élaboration du sujet du projet, encadrement des projets en TD et TP, et évaluation finale des projets lors de présentations orales avec démonstration du produit fini. \end{itemize} \subsectCV{Année 2006-2007: Assistant en anglais à l'ETH Z\"urich.} \noindent \ \\ \noindent \emph{Modeling \& Simulation}~: \begin{itemize} \item \emph{Durée}~: 24 heures TD. \item \emph{Public}~: 1 groupe de 20 étudiants en troisième année d'université à l'ETH Z\"urich. \item \emph{Responsable}~: Gaston \textsc{Gonnet} : gonnet@inf.ethz.ch \item \emph{Description}~: Ce module d'informatique et mathématiques propose d'abord une modélisation de différents problèmes concrets, comme la localisation par GPS, la structure de protéines, etc ... Ensuite nous introduisons les outils mathématiques nécessaires à la résolution efficace de ces problèmes, telles les méthodes des moindres carrés, de décomposition en vecteurs propres etc... Nous appliquons alors ces méthodes à la résolution aux problèmes introduits. \item \emph{Réalisation}~: participation à l'élaboration des sujet de TD et TP, surveillance d'examen et correction des copies. \end{itemize} \ \\ \noindent \emph{Information Security}~: \begin{itemize} \item \emph{Durée}~: 24 heures TD. \item \emph{Public}~: 1 groupe de 20 étudiants en 4ème année d'université à l'ETH Z\"urich. \item \emph{Responsable}~: David \textsc{Basin} : basin@inf.ethz.ch \item \emph{Description}~: Ce module donne une vue générale des principes et méthodes de sécurité de l'information à travers de nombreuses applications. Nous abordons les notions relatives aux fondements de la cryptographie, aux échanges de clefs, à la sécurité des protocoles, aux méthodes de contrôles et de politiques d'accès ainsi qu'aux notions d'anonymat et de confidentialité. \item \emph{Réalisation}~: participation à l'élaboration des sujets de TD, TP, et coordination des assistants. \end{itemize} \subsectionN{En technique d'apprentissage.} J'ai eu l'occasion d'assister Alain \textsc{Finkel} lors de ses cours sur les techniques d'apprentissage destinées au public universitaire. J'ai également obtenu le Diplôme Universitaire de l'École Normale Supérieure de Cachan : Nouvelles Techniques Cognitives d'Apprentissage (NTCA) en Septembre 2006, pour parfaire mes compétences dans ce domaine. \\ \subsectCV{Assistant aux journées apprentissage de Marseille 2005.} \ \\ \noindent \emph{Représentations mentales et motivation}~: \begin{itemize} \item \emph{Durée}~: 8 heures de TD. \item \emph{Public}~: 2 groupes de 15 moniteurs en deuxième année au C.I.E.S. de Marseille. \item \emph{Responsable}~: Alain \textsc{Finkel} \& Yves \textsc{Mathey} directeur du CIES Provence-Côte d'Azur-Corse : finkel@lsv.ens-cachan.fr \item \emph{Description}~: Tout d'abord les moniteurs découvrent et explorent leurs représentations mentales. On s'aperçoit ainsi que chacun possède sa propre représentation mentale de notion aussi simple que le point en géométrie. Ensuite les moniteurs apprennent à expliciter une prise de décision anodine. Finalement ils découvrent comment motiver leurs élèves en se servant des techniques de prise de décision, d'explicitation et des notions apprises sur les représentations mentales. \item \emph{Réalisation}~: participation à l'élaboration des séances de TD. \end{itemize} \subsectCV{Année 2005-2006: Assistant en TD à l'IUT d'Orsay. } \ \\ \noindent \emph{Mémoires et motivation}~: \begin{itemize} \item \emph{Durée}~: 8 heures de TD. \item \emph{Public}~: 4 groupes de 20 étudiants en première année d'IUT informatique à Orsay. \item \emph{Responsable}~: Alain \textsc{Finkel} : finkel@lsv.ens-cachan.fr \item \url{http://www.lsv.ens-cachan.fr/~finkel/ja2006} \item \emph{Description}~: Dans un premier temps les étudiants découvrent comment mémoriser et quelles stratégies mettre en place pour une meilleure mémorisation. Ensuite ils cherchent quel objectif envisager pour leur cursus futur. Nous vérifions avec eux que cet objectif est un ``bon'' objectif, car avoir un bon objectif aide à être motivé. \item \emph{Réalisation}~: participation à l'élaboration des séances de TD. \end{itemize} \subsectCV{Assistant aux journées apprentissage de Cachan, Mai 2006.} \ \\ \noindent \emph{Émotions et motivation}~: \begin{itemize} \item \emph{Durée}~: 8 heures de TD. \item \emph{Public}~: 2 groupes de 20 enseignants. \item \emph{Responsable}~: Alain \textsc{Finkel} : finkel@lsv.ens-cachan.fr \item \emph{Description}~: Dans un premier temps les participants découvrent grâce à une technique d'explicitation quels besoins sont cachés derrière leurs émotions. Ensuite ils apprennent à expliciter une prise de décision anodine. Finalement ils découvrent comment motiver leurs élèves. \item \emph{Réalisation}~: participation à l'élaboration des séances de TD. \end{itemize} \subsectCV{Assistant aux journées de formation de l'École Supérieure d'Ostéopathie, Novembre 2006.} \ \\ \noindent \emph{Représentations mentales \& mémorisation}~: \begin{itemize} \item \emph{Durée}~: 8 heures de TD. \item \emph{Public}~: 1 groupe de 20 ostéopathes en formation. \item \emph{Responsable}~: Alain \textsc{Finkel} : finkel@lsv.ens-cachan.fr \item \emph{Description}~: Dans un premier temps les participants découvrent grâce à des exemples leurs propres modes de représentations mentales. Ensuite ils apprennent comment le travail sur ces représentations mentales leur permet de mieux comprendre certains mécanismes d'apprentissage. Lors de la seconde séance, nous proposons d'explorer les différentes facettes de la mémoire et d'acquérir des méthodes de mémorisation. Ensuite nous explorons les émotions et besoins des participants pour renforcer leurs motivations. \item \emph{Réalisation}~: participation à l'élaboration des séances de TD. \end{itemize} \subsectionN{Documents pédagogiques réalisés.} \begin{itemize} \item[$\bullet$] Réalisation des sujets de TD et TP du module ``Information \& Security'' à l'ETH Z\"urich. \item[$\bullet$] Réalisation des TD, élaboration de l'examen du module ``Modeling \& Simulation'' à l'ETH Z\"urich. \item[$\bullet$] Site Web sur l'initiation à la programmation. \item[$\bullet$] Surveillance d'examen en DEUG MIAS 1. \item[$\bullet$] Aide à la réalisation des contrôles continus, sujet de projet et élaboration des TD et TP en Base de données. \item[$\bullet$] Grille de correction de copies d'examen des partiels sur machine de système. \item[$\bullet$] Grille d'évaluation des projets de Php \& Mysql \item[$\bullet$] Réalisation des sujets de TD en base de la programmation en C. \item[$\bullet$] Réalisation des séances de TD sur la motivation lors des journées apprentissage de Marseille. \item[$\bullet$] Réalisation des séances de TD sur les émotions lors des journées apprentissage de Cachan. \item[$\bullet$] Réalisation des séances de TD sur la mémorisation, la définition d'un bon objectif pour des étudiants de l'IUT d'Orsay. \end{itemize} \ \\ Le site Web pour les étudiants de DEUG première année ainsi que quelques-uns des autres supports pédagogiques réalisés se trouvent à l'adresse suivante : \url{http://www.lsv.ens-cachan.fr/~lafourca/enseignement.php}\\ \newpage \section{Activités administratives. } \subsectCV{Organisation de colloques.} \begin{itemize} \item Participation au comité d'organisation de la conférence internationale FORMATS 2006 à Paris du 25 au 28 Septembre 2006, 80 participants (Webmaster du site d'inscription).\\ \url{http://www.lsv.ens-cachan.fr/formats06/} \item Participation au comité d'organisation des Journées Apprentissage 2006 à Paris du 17 au 19 Mai 2006. Journées destinées aux moniteurs et enseignants, avec une centaine de participants (Webmaster du site d'inscription et assistant en TD). \\ \url{http://www.lsv.ens-cachan.fr/~finkel/ja2006.html} \item Membre du comité organisateur des Rencontres Emplois pour les Doctorants (RED) de l'École Doctorale Sciences Pratiques (EDSP) à l'École Normale Supérieure de Cachan en Mai 2005, manifestation de 3 jours organisée tous les 18 mois. Cette manifestation a pour but de donner aux doctorants des informations sur les possibilités de carrières à la fois publiques et privées qui leur sont offertes après leur doctorat. Nous avons réuni lors des ces rencontres une centaine de doctorants et une vingtaine d'intervenants extérieurs (industriels, universitaires, anciens doctorants, chasseurs de têtes ...). \end{itemize} \subsectCV{Charges administratives.} \begin{itemize} \item Membre de l'équipe SOS, mailing liste d'aide pour les utilisateurs de Linux au Laboratoire Spécification et Vérification (LSV). \item Membre de l'équipe INSTSOFT, groupe d'installation du LSV pour des logiciels sous Linux. \item Responsable de la mise à jour de la page web interne de recherche bibliographique pour les membres du LSV. Cette page récapitule l'ensemble des moyens existants pour rechercher une référence bibliographique à l'ENS Cachan. Et responsable des pages web internes d'aide pour l'utilisation du graveur et du scanner. \end{itemize} \subsectCV{Évaluation d'articles.} \begin{itemize} \item {\it Information and Computation}, revue internationale. \item 34th International Colloquium on Automata, Languages and Programming ({\it ICALP 2007}). \item 16th International Conference on Rewriting Techniques and Applications ({\it RTA 2006}). \item 20th International Conference on Automated Deduction ({\it CADE 2005}). \end{itemize} \newpage \section{Activités de recherche.} Je présente une vue synthétique de mes travaux de recherche et la liste de mes publications. Je récapitule ensuite mes différentes activités de recherche, de communications et de formations à travers les différents projets, écoles d'été, conférences et séminaires auxquels j'ai participé. Je présente enfin mon projet de recherche dans la section~\ref{sec:prog_rech}. \subsectCV{Travaux effectués lors du DEA RCFR, à l'IRIT Toulouse.} J'ai effectué mon stage de recherche de DEA Représentation de la Connaissance et Formalisation du Raisonnement (RCFR) à l'Institut de Recherche en Informatique de Toulouse (IRIT), dans l'équipe Raisonnements Plausibles, Décisions, Méthodes de Preuve (RPDMP). Mon travail portait sur l'aide à la décision pour la résolution de conflits dans l'ordonnancement de t\^aches sous la direction de Claudette \textsc{Cayrol}, Hélène \textsc{Fargier} et Marie-Christine \textsc{Lagasquie-Schiex}. Lorsqu'il n'existe pas de solution à un problème d'ordonnancement, le calcul des conflits, ensembles minimaux de contraintes «~incohérents~», donne les explications de cet échec. Cette notion de conflits existe aussi en logique propositionnelle (ensembles minimaux de formules inconsistantes). Dans ce travail~\citetwo{Lafourcade-DEA}, nous adaptons de nombreux critères de préférences locales issus de la résolution de conflits en logique propositionnelle, à la résolution de conflits dans un problème d'ordonnancement. Nous introduisons également de nouveaux critères «~colorés~» spécifiques aux problèmes d'ordonnancement. Ce cadre formel d'aide à la décision permet de transformer un problème d'ordonnancement sans solution en un problème d'ordonnancement avec solution, en respectant les préférences locales. Nous spécifions pour tous nos critères des algorithmes de type «~Branch-and-Bound~» pour la recherche de solutions optimales. L'implémentation de certains critères nous montre que l'ordre de résolution des conflits est crucial et confirme que la résolution de tels conflits est un problème qui a une complexité en temps exponentielle. \subsectCV{Travaux effectués pendant ma thèse, à l'ENS de Cachan.} Ces travaux portent sur un tout autre domaine que le travail réalisé en DEA. Dans le cadre de l'ACI Sécurité Rossignol, j'ai obtenu une bourse de thèse entre le Laboratoire Spécification et Vérification de Cachan (LSV) et le Laboratoire d'Informatique Fondamentale de Marseille (LIF), sous la direction de Ralf \textsc{Treinen} (LSV) et Denis \textsc{Lugiez} (LIF). Mon travail de thèse porte sur les méthodes formelles, la sécurité informatique et plus particulièrement sur la vérification de protocoles cryptographiques en présence de propriétés algébriques. \subsubsection*{Vérification de protocoles cryptographiques.} La démocratisation de l'ordinateur et l'essor d'internet impliquent un changement considérable de nos modes de consommation et de communication. Ainsi nous pouvons gérer nos comptes bancaires, acheter un billet d'avion, payer nos imp\^ots depuis notre ordinateur relié à internet ou directement sur notre téléphone mobile. Ces transactions utilisent des protocoles de communication complexes qui transmettent des données confidentielles. Toutes ces applications nécessitent des garanties de sécurité élevées, portant à la fois sur les propriétés de secret et d'authenticité des participants, mais aussi de nombreuses autres propriétés parmi lesquelles l'anonymat (des votants lors d'élections), l'équité (pour les signataires d'un contrat), la non-révocation (des commandes pour un commerçant), etc... Les concepteurs de ces protocoles de communication utilisent des primitives cryptographiques pour sécuriser les échanges de messages entre les différents participants. Depuis les années 1980, les progrès en matière de cryptographie nous assurent l'existence d'algorithmes de chiffrement suffisamment s\^urs. Mais même en supposant que les algorithmes utilisés, typiquement le chiffrement, les fonctions à sens unique ou les générateurs aléatoires soient parfaits, i.e. inviolables, la plupart des protocoles publiés comportent des failles, comme le montre le fameux protocole de Needham-Schroeder~\citeone{NS78} considéré s\^ur jusqu'à ce qu'une attaque <<~logique~>> fut découverte par G.~Lowe~\citeone{Lowe95_NSPK} $15$ ans après la publication du protocole. Une attaque logique consiste à jouer le protocole de différentes manières pour en extraire des informations supposées secrètes, par opposition à une attaque par cryptanalyse qui va chercher à déchiffrer les messages cryptés échangés par les participants. Depuis la découverte de cette faille, la vérification formelle de protocoles cryptographiques a pris une importance considérable dans le domaine de la sécurité informatique. \subsubsection*{Formalisation des protocoles cryptographiques : le modèle de Dolev-Yao.} En 1983, Dolev et Yao~\citeone{dolev83security} proposent une des premières formalisations des protocoles cryptographiques, utilisée depuis comme base à de nombreuses méthodes de vérification de protocoles cryptographiques~\citeone{NRL96,paulson97mechanized,Monniaux99,GK00,Goubault00,blanchet01,amadio02concur,RT03csl,BEL04concur,DBLP:conf/ppdp/CortierRZ05}. Dolev et Yao supposent dans leur modèle <<~l'hypothèse de chiffrement parfait~>> : le seul moyen d'obtenir le contenu d'un message chiffré est de connaître la clef de déchiffrement. Ils abstraient également le réseau de communication entre deux participants en supposant que les messages sont échangés instantanément entre les différents participants via un réseau idéalisé quel que soit le type de connexion utilisé. Dans ce modèle, les messages envoyés et reçus ne sont pas des nombres, ni des suites de bits, ni des signaux électriques, mais des éléments d'une algèbre de termes, éventuellement modulo une théorie équationnelle. Cette approche considère aussi le cas le plus pessimiste en modélisant un intrus omniprésent, i.e. un intrus qui contr\^ole le réseau et peut donc intercepter, bloquer, modifier les messages échangés sur le réseau, et aussi jouer des sessions du protocole avec les autres participants. Les capacités de cet intrus sont modélisées par un système de déduction, lui permettant par exemple de déchiffrer un message s'il en connaît la clef de déchiffrement. Cette modélisation permet de représenter facilement une ou plusieurs exécutions du protocole. Gr\^ace à ce modèle, il a été prouvé~\citeone{durgin99undecidability,RT03csl} que si le nombre de sessions est non-borné, alors le problème de secret i.e. savoir si une donnée secrète entre deux participants peut être découverte par un intrus, est un problème indécidable. Se restreindre à un nombre borné de sessions rend le problème décidable~\citeone{RT01}. \subsubsection*{Mes travaux.} En considérant le modèle de Dolev-Yao pour un nombre borné de sessions, je me suis intéressé à l'affaiblissement de l'hypothèse de chiffrement parfait pour la propriété de secret. Remarquons d'abord que les algorithmes de chiffrement sont construits à partir de fonctions mathématiques qui possèdent certaines propriétés algébriques. Notons également que les protocoles eux-mêmes sont souvent construits à partir de certaines propriétés algébriques. Pour analyser de manière plus réaliste les protocoles, il est donc important de prendre en compte les propriétés algébriques lors de la vérification. En effet, il est possible qu'un intrus utilise ces propriétés pour obtenir une information secrète. J'ai donc cherché au cours de ma thèse à affaiblir l'hypothèse du chiffrement parfait en prenant en compte les propriétés algébriques de certains opérateurs cryptographiques. \paragraph{Les propriétés algébriques : } J'ai, dans un premier temps, répertorié et classé les protocoles utilisant dans leurs spécifications une propriété algébrique soit dans les méthodes de chiffrement utilisées soit de part leurs conceptions même. J'ai cherché à présenter, chaque fois que possible, une attaque sur le protocole utilisant ces propriétés algébriques. Ce premier travail~\citetwo{Prouve:rap2} dans le cadre du projet RNTL Prouvé a donné lieu à une publication~\citetwo{CDL05-survey} dans la revue internationale << Journal of Computer Security >>. Dans cette étude, nous présentons l'ensemble des propriétés algébriques utilisées par les protocoles cryptographiques actuels et l'ensemble des résultats de vérification existants pour ces propriétés. Suite à cette étude, j'ai porté mon attention sur les propriétés algébriques dites <<~d'homomorphismes~>> jusqu'alors vérifiées formellement. Ces propriétés sont représentées par la théorie équationnelle suivante $h(a+b)=h(a)+h(b)$. Cette propriété d'homomorphisme permet, comme l'a montré G.J.~Simmons~\citeone{Simmons94cacm}, à un intrus de découvrir de l'information confidentielle sur le protocole d'échange de clef TMN~\citeone{TMN89}. J'ai d'abord étendu le modèle de l'intrus de Dolev-Yao pour prendre en compte des propriétés algébriques pertinentes lors de la vérification de protocoles cryptographiques. Dans le cadre du projet RNTL Prouvé~\citetwo{Prouve:rap4}, nous avons également dégagé à partir d'un modèle étendu de l'intrus des conditions suffisantes pour la vérification automatique. Je me suis d'abord concentré sur l'intrus {\it passif} pour cette propriété d'homomorphisme. L'intrus passif est la première étape de la vérification des protocoles cryptographiques : un tel intrus écoute uniquement les messages échangés sur le réseau et cherche à en déduire de l'information confidentielle grâce à ces capacités. Ensuite je me suis intéressé à l'intrus {\it actif} qui en plus d'écouter tous les messages du réseau comme son homologue passif, peut intercepter, modifier, bloquer des messages et jouer des sessions du protocole avec d'autres participants. \paragraph{L'intrus passif :} Dans le cadre d'un intrus passif, j'ai élaboré un premier ensemble de résultats de décidabilité pour la propriété de secret en présence d'un opérateur homomorphique ($h$) sur un opérateur associatif et commutatif ($ACh$), sur l'opérateur du {\it ou-exclusif} ($ACUNh$) ou sur l'opérateur des groupes abéliens ($AGh$). Ces résultats sont basés sur une extension du résultat de localité de Mac Allester~\citeone{allester93} et des techniques de normalisation d'arbres de preuves développées dans le système déductif de Dolev-Yao étendu par une théorie équationnelle. J'ai présenté ce travail lors de la conférence internationale RTA 2005~\citetwo{LLT-rta2005}. Nous avons ensuite résolu le cas d'un chiffrement distributif, représenté par la théorie équationnelle $\{a+b\}_k = \{a\}_k +\{b\}_k$, où $\{m\}_k$ dénote le chiffrement du message $m$ par la clef $k$. Dans ce cas, nous avons autant de symboles homomorphiques que de clefs possibles, ce qui rend la tâche plus complexe. Nous avons donc construit une nouvelle procédure dans un premier temps pour un chiffrement distributif sur l'opérateur sur {\it ou-exclusif} ($ACUN$)~\citetwo{LSV:05:19} et ensuite sur l'opérateur des groupes abéliens ($AG$)~\citetwo{THESE-lafourcade06}. L'ensemble de ces résultats a été accepté pour publication dans la revue internationale << Information and Computation >>~\citetwo{LLT-icomp07}. Enfin j'ai considéré le cas d'un chiffrement distributif et commutatif pour l'opérateur du {\it ou-exclusif} ($ACUN$) ce qui consiste à enrichir le modèle de l'équation $\{\{m\}_{k1}\}_{k2} = \{\{m\}_{k2}\}_{k1}$. Cette nouvelle théorie équationnelle, dénotée par <<~$ACUN\{.\}_.$~Commutatif~>>, demande une étude plus minutieuse des arbres de preuves et de nouvelles caractérisations pour obtenir une normalisation de preuves adéquate. J'ai présenté ce travail lors du workshop international SecRet 2006. Une version longue de ce résultat a été accepté pour publication dans la revue électronique ENTCS~\citetwo{Laf-secret06}. Dans mon manuscrit de thèse~\citetwo{THESE-lafourcade06}, j'étends ce résultat au groupe abélien. J'ai également proposé, dans un chapitre de ma thèse, des exemples de théories équationnelles montrant que dans le cas d'un intrus passif la décidabilité du problème de secret et celle du problème d'unification sont indépendants, contrairement au cas de l'intrus actif, o\`u l'indécidabilité du problème d'unification implique l'indécidabilité du problème de secret. \paragraph{L'intrus actif :} J'ai résolu pour un nombre borné de sessions le problème du secret pour la théorie équationnelle $ACUNh$ constituée d'un opérateur homomorphique ($h$) distributif par rapport à l'opérateur du {\it ou-exclusif} ($ACUN$). J'ai présenté ce travail à la conférence internationale ICALP 2006~\citetwo{DLLT-ICALP2006}. Lors de cette étude nous avons suivi l'approche de J.~Millen et V.~Shmatikov~\citeone{MS02,MS03} qui modélisent les protocoles par des systèmes de contraintes {\it bien définis}. Nous avons proposé une nouvelle caractérisation algébrique des systèmes de contraintes bien définis. Cela nous a permis de transformer les systèmes de contraintes bien définis en systèmes d'équations diophantiennes quadratiques. Grâce à cette nouvelle caractérisation, nous avons pu développer une méthode de résolution de ces systèmes d'équations quadratiques particuliers, problème indécidable en général. Par la suite nous avons étendu ce travail difficile et complexe à d'autres théories équationnelles~\citetwo{LSV:06:17} .Ce travail nous a aussi amené à développer un algorithme d'unification complet pour cette théorie équationnelle~\citetwo{LLT-unif2006}. \paragraph{Bilan :} Dans le tableau suivant, je résume les principaux résultats obtenus lors de mon doctorat sur la vérification de protocoles cryptographiques en présence de théories équationnelles. \begin{figure}[htbp] \begin{center} \begin{tabular}{|>{\centering}p{3.8cm}|>{\centering}p{3cm}|>{\centering}p{3cm}|} \cline{2-3} \multicolumn{1}{l|}{} & \multicolumn{2}{c|}{\textbf{Complexité}}\tabularnewline \cline{2-3} \multicolumn{1}{l|}{} & \vfill \textbf{Intrus passif} \vfill&\vfill \textbf{Intrus actif}\vfill \tabularnewline \hline \vfill \textbf{ACUNh} \vfill & \vfill \textit{P-TIME} \citetwo{LLT-rta2005},\citeone{SD-ipl05} \vfill & \vfill \textit{Décidable} \vfill \citetwo{DLLT-ICALP2006} \vfill \tabularnewline\hline \vfill \textbf{AGh} \vfill& \vfill {\textit P-TIME} \citetwo{LLT-rta2005},\citeone{SD-ipl05} \vfill & \vfill \textit{Indécidable} \citeone{LSV:06:02} \vfill \tabularnewline\hline \vfill \textbf{ACUN$\{.\}_.$ \& AG$\{.\}_.$} \vfill & \vfill {\textit EXP-TIME} \vfill \citetwo{LLT-icomp07} \vfill & \vfill \textit{?} \vfill \tabularnewline\hline \vfill \textbf{ACUN$\{.\}_.$ \& AG$\{.\}_.$ Commutatif} \vfill & \vfill {\textit 2EXP-TIME} \citetwo{Laf-secret06,THESE-lafourcade06} \vfill & \vfill \textit{?} \vfill\tabularnewline\hline \end{tabular} \end{center} \end{figure} \subsectCV{Travaux effectués aprés ma thèse, à l'ETH Z\"urich.} La Direction Générale de l'Armement (DGA) a retenu mon dossier pour une bourse post-doctorale d'un an à l'ETH Z\"urich dans l'équipe <<~Information and Security~>> de David Basin. Mon post-doctorat en Suisse me permet d'élargir mes connaissances en vérification formelle de protocoles cryptographiques et de commencer de nouvelles collaborations sur d'autres sujets. Je présente ici les travaux que j'ai commencés à Z\"urich depuis le 1$^{er}$ Octobre 2006. Suite à notre publication à la conférence ICALP 2006, nous avons dégagé les critères nécessaires à notre procédure pour la théorie de l'homomorphisme et du {\it ou-exclusif} et avons étendu notre résultat de décidabilité pour un nombre borné de sessions à l'ensemble des théories mono\"idales. Ce travail est en cours de soumission à une revue internationale~\citetwo{LSV:06:17}. J'ai commenc\'e une collaboration avec Yannick Chevalier (IRIT, Toulouse) pour résoudre les problèmes laissés ouverts à la suite de mes travaux de thèse présentés dans le tableau r\'ecapitulatif ci-dessus. Cette collaboration porte plus pr\'ecisement sur le cas d'un intrus actif en présence d'une méthode de chiffrement commutative et distributive sur l'opérateur du {\it ou-exclusif} dans un premier temps et ensuite le cas de l'opérateur des groupes abéliens. De plus, dans le cadre du projet VerSePro (Provably Secure Protocols for Wireless Networks) entre l'EPFL et l'ETH Z\"urich, je m'intéresse à une modélisation des réseaux sans fil afin de pouvoir vérifier formellement les protocoles développés dans ce domaine en plein essor, ces dernières années. J'ai \'egalement commencé une collaboration avec Ralf Kuesters dans l'équipe <<~Foundations of Computer and Network Security~>> sur la v\'erificaion formelle des protocoles de groupe. Enfin, j'ai commencé une collaboration avec Bogdan Ksi{\k e}{\. z}opolski, Université de Lublin Pologne, sur la vérification de protocoles de vente aux enchères électroniques. Ce travail~\citetwo{KL-eth07}, nous a permis, grâce à la modélisation dans l'outil OFMC~\citeone{vigano:ofmc:2005}, de trouver une faille sur un protocole de vente aux enchères. Nous proposons aussi une nouvelle version corrigée et vérifiée par cet outil de ce protocole. \subsectCV{Liste de publications.} L'ensemble de mes publications est disponible électroniquement à l'adresse suivante : \begin{center} \url{http://www.lsv.ens-cachan.fr/~lafourca/publis.php} \end{center} \def\refname{} \vspace{-1cm} \nocitetwo{LLT-unif2006} \nocitetwo{Laf-secret06} \nocitetwo{LSV:05:19} \nocitetwo{LSV:04:16} \nocitetwo{LSV:06:17} \nocitetwo{Prouve:rap4} \nocitetwo{Prouve:rap2} \nocitetwo{Lafourcade-DEA} \nocitetwo{KL-eth07} \nocitetwo{DGA:rap1} \nocitetwo{THESE-lafourcade06} \makeatletter \let\NMSB@valuelist\relax \makeatother \bibliographystyletwo{abbrv} \bibliographytwo{lafourca-1997.bib,lafourca-1998.bib,lafourca-1999.bib,lafourca-2000.bib,lafourca-2001.bib,lafourca-2002.bib,lafourca-2003.bib,lafourca-2004.bib,lafourca-2005.bib,lafourca-2006.bib,lafourca-2007.bib,lafourca-autres.bib} \subsectCV{Projets.} \begin{description} \item[{\bf ACI Sécurité Rossignol }] (Action Concertée Incitative 2003 - 2006). Projet soutenu par le ministère fran\c{c}ais de la recherche, réunissant les équipes de recherche suivantes : \begin{itemize} \item LIF de Marseille \item INRIA Futurs, LIX \item LSV, ENS Cachan \item Verimag (Grenoble) \end{itemize} Sur le thème : \emph{Sémantique de la vérification de protocoles cryptographiques : théorie et applications.} (\url{www.cmi.univ-mrs.fr/~lugiez/aci-rossignol.html}). Ma thèse fut financé par l'ACI Rossignol pour renforcer la collaboration entre les différents laboratoires et plus particulièrement entre le LSV et le LIF. L'ensemble de mes travaux s'inscrit donc dans cette ACI. \item[{\bf Projet RNTL PROUVÉ}] (Réseau National des Technologies Logicielles 2003-2006). Projet soutenu par le ministère fran\c{c}ais de la recherche, réunissant les partenaires suivants : \begin{itemize} \item CRIL Technology Systèmes Avancés \item France Télécom R\&D \item INRIA Lorraine (Nancy) \item LSV, ENS de Cachan \item Verimag (Grenoble) \end{itemize} Sur le thème : \emph{PRotocoles cryptographiques : OUtils de VÉrification.}\\ (\url{www.lsv.ens-cachan.fr/prouve/}). Mes travaux sur les propriétés algébriques constituent une partie importante des avancées effectuées dans ce projet. Ce projet a permis de nombreuses collaborations entre les différents partenaires et l'élaboration d'un langage commun de spécification pour la vérification de protocoles. \item[{\bf Projet VerSePro}] (Provably Secure Protocols for Wireless Networks). Projet entre l'École Polytechnique Fédérale de Lausanne (EPFL) et l'Eidgenössische Technische Hochschule Z\"urich (ETH Z\"urich), soutenu par le gouvernement suisse, faisant partie du projet Mobile and Information Communication Systems (MISC : \url{www.mics.org/}). Dans ce projet, nous cherchons à modéliser les propriétés induites par les réseaux sans fil et à prendre en compte la mobilité des entités dues à ce nouveau mode de communication afin de vérifier de nouveaux protocoles. \end{description} \subsectCV{Écoles internationales.} \begin{description} \item[2006] École d'été de Marktoberdorf sur la sûreté et la sécurité des systèmes logiciels, 1-13 août 2006, Marktoberdorf, Allemagne. \url{http://asimod.in.tum.de/} \item[2005] École de printemps sur la sécurité 25-29 Avril 2005 Marseille, France. \url{www.cmi.univ-mrs.fr/~secur05/} \item[2004] École d'été ICCL : Théorie de la preuve et preuve automatique de théorème, 14-26 Juin 2004, Technische Universität Dresden. \url{www.computational-logic.org/iccl/events/SA-2004/} \end{description} \subsectCV{\franglais{Communications.}{Talks}} \begin{description} \item[{\bf Exposé invité : }] \ \begin{itemize} \item Conférence internationale IBIZA 2007, 9 Février 2007, Pologne. \end{itemize} \item[{\bf Présentations d'articles à des conférences internationales : }] \ \begin{itemize} \item 33rd International Colloquium on Automata, Languages and Programming ({\it ICALP 2006}), 10 Juillet 2007, Venise Italie. \item 16th International Conference on Rewriting Techniques and Applications ({\it RTA 2005}), 20 Avril 2005, Nara Japon. \end{itemize} \item[{\bf Présentations d'article à un workshop international : }]\ \begin{itemize} \item 1st International Workshop on Security and Rewriting Techniques ({\it SecReT 2006}), 15 Juillet 2006, Venise Italie. \end{itemize} \item[{\bf Séminaires et exposés : }]\ \begin{itemize} \item Séminaire du groupe ``Information Security'' à l'ETH Z\"urich, Suisse, 9 Septembre 2006. \item Séminaire 68NQRT à Rennes à l'IRISA, France, 27 Juin 2006. \url{http://www.irisa.fr/NQRT/} \item École de printemps internationale sur la sécurité à Marseille, France, 25-29 Avril 2005. \item Séminaire de l'équipe Information Security de l'ETH Z\"urich, le 8 Septembre 2006. \item Plusieurs exposés à différents groupes de travail et rencontres de projet : groupe de travail de l'équipe SECurité des Systèmes d'Information (SECSI) au LSV, équipe MOdelisation VErification (LIF Marseille), ACI Sécurité Rossignol à Cachan, à Grenoble et à l'école poytechnique, projet RNTL PROUVé à Nancy. \end{itemize} \item[{\bf Participations aux conférences et workshops internationaux : }]\ \begin{itemize} \item 2nd Workshop on Formal and Computational Cryptography ({\it FCC 2006}), Venise Italie. \item 6th International Workshop on Issues in the Theory of Security ({\it WITS 2006}), Vienne Autriche. \item 18th IEEE Computer Security Foundations Workshop ({\it CSFW 2005}), Aix-en-Provence France. \item 19th International Workshop on Unification ({\it UNIF 2005}), Nara Japon. \item European Joint Conferences on Theory and Practice of Software ({\it ETAPS 2004}), Barcelone Espagne. \end{itemize} \end{description} \subsectCV{Collaborations.} Actuellement, j'ai commencé des travaux sur les thèmes suivants : \begin{itemize} \item[{\it Les réseaux sans fil}, avec :] \ \begin{itemize} \item David Basin, ETH Z\"urich Suisse. \item Srdjan Capkun, ETH Z\"urich Suisse. \item Patrick Schaller, ETH Z\"urich Suisse. \end{itemize} \item[{\it Les protocoles de groupes}, avec :] \ \begin{itemize} \item Ralf Kuesters, ETH Z\"urich Suisse. \end{itemize} \item[{\it Les propriétés algébriques}, avec :]\ \begin{itemize} \item Yannick Chevalier, IRIT Toulouse. \end{itemize} \item[{\it La vérification de protocoles de vote et de vente aux enchères}, avec :]\ \begin{itemize} \item Cas Cremers, ETH Z\"urich Suisse. \item Luca Viganò, Université de Verone Italie. \item Sebatian Mödersheim, IBM Z\"urich Suisse. \item Bogdan Ksi{\k e}{\. z}opolski, Université de Lublin Pologne. \end{itemize} \end{itemize} \newpage \section{Programme de recherche détaillé.}\label{sec:prog_rech} \begin{center} {\Large \it Analyse automatique et formelle des propriétés \\ des protocoles de nouvelle génération.} \end{center} Assurer la confidentialité des données est un enjeu majeur des systèmes informatiques actuels, compte tenu de la prolifération des échanges sécurisés d'information sur internet. La plupart des appareils électroniques sont désormais connectés entre eux et interagissent pour proposer de nouveaux services aux utilisateurs. Dans ce nouvel environnement, les concepteurs de tels systèmes créent des protocoles cryptographiques de plus en plus complexes ayant pour but d'assurer la confidentialité des informations échangées ainsi que de nouvelles propriétés, comme l'anonymat, l'équité... En raison de la complexité croissante de ces protocoles, il apparaît clairement qu'une analyse manuelle n'est pas suffisante. Une telle approche avait par exemple vérifié le célèbre protocole de Needham-Schroeder~\citeone{NS78} avant qu'une analyse automatique et formelle quinze ans plus tard ne révèle l'existence d'une faille~\citeone{Lowe95_NSPK}. En conséquence, il est indispensable aujourd'hui de développer des méthodes formelles et automatiques de vérification pour les propriétés des protocoles cryptographiques de nouvelle génération : en particulier les protocoles régissant les Web Services, les communications sans fil, le commerce électronique... L'analyse de ces protocoles spécialisés est difficile car elle met en {\oe}uvre les quatre aspects suivants : \begin{itemize} \item l'{\it environnement} dans lequel le protocole est exécuté. \item l'{\it implantation} même des protocoles. \item les {\it opérateurs algébriques} utilisés dans la spécification même du protocole. \item les {\it propriétés globales} que doivent garantir les protocoles. \end{itemize} Mon projet de recherche consiste donc à analyser de la manière la plus réaliste possible les protocoles suivant ces quatre axes. Pour faciliter cette analyse, je compte étudier pour chacun de ces aspects une classe de protocoles particulièrement représentative. Mon projet de recherche concerne l'analyse automatique et formelle des propriétés des protocoles de nouvelle génération et s'articule autour des thèmes suivants : \begin{itemize} \item[$\bullet$] {\it Étude de nouvelles propriétés des réseaux sans fil.} \item[$\bullet$] {\it Modélisation et vérification des Web Services.} \item[$\bullet$] {\it Analyse formelle des protocoles de groupe.} \item[$\bullet$] {\it Vérification des protocoles de vote et de vente aux enchères.} \end{itemize} \subsectCV{Étude de nouvelles propriétés des réseaux sans fil.} \paragraph{Objectif :}Le premier aspect de mon programme de recherche vise à étudier les protocoles cryptographiques en prenant en compte l'environnement dans lequel ils sont exécutés. \paragraph{Problématique :} Compte tenu de l'émergence de l'intelligence ambiante (objets intelligents, sensibles à leur environnement et capables d'interagir) il est important de modéliser, d'analyser et de vérifier les protocoles cryptographiques dans un réseau sans fil. Ces dernières années, les connexions sans fil ({\it wireless}) entre les différents composants d'un réseau se sont développées grâce à la multiplication des systèmes embarqués. Ces avancées technologiques modifient considérablement les hypothèses faites habituellement dans la vérification de protocoles cryptographiques. Nous ne pouvons plus considérer que les messages sont échangés instantanément entre deux agents et les connexions sans fil permettent aux agents de se déplacer tout en restant connectés. Par exemple, le système de navigation embarqué dans un véhicule s'informe de l'état du réseau routier (accident, embouteillages...) en communiquant avec les autres véhicules. Tout cela donne naissance à de nouveaux protocoles et à de nouvelles propriétés qu'il faut alors vérifier : propriété de voisinage, de borne sur la distance entre les participants, de localisation des agents... Ces propriétés sont cruciales pour établir une connexion sans fil sécurisée entre deux agents. Récemment plusieurs protocoles ont été développés pour découvrir si deux agents ont la possibilité de communiquer directement : dans ce cas, les deux agents sont voisins, ils possèdent la propriété de <<~voisinage~>>. Je souhaite proposer un modèle permettant l'analyse la plus réaliste possible de ces nouvelles propriétés spatiales et temporelles pour les protocoles de nouvelle génération pour un réseau sans fil. \paragraph{État de l'art :} Les concepteurs de ces protocoles garantissent la propriété de voisinage par une analyse informelle. Actuellement il n'existe que quelques tentatives d'analyse formelle pour des protocoles particuliers~\citeone{Meadows2007} et aucune de ces approches, à ma connaissance, n'a réussi à formaliser de façon satisfaisante la propriété de voisinage. \paragraph{Proposition d'étude :} Dans le cadre de mon stage post-doctoral à l'ETH de Zürich, je participe au projet VerSePro (Verification of Security and privacy Protocols for wireless networks) faisant partie du projet MICS (Mobile and Information Communication Systems). Dans ce projet, à partir des protocoles et des technologies de communication sans fil existants, nous avons proposé une modélisation pour la propriété de voisinage entre deux agents. Cette modélisation inspirée par le modèle de traces de L.~Paulson~\citeone{paulson97mechanized} permettra de vérifier automatiquement et formellement si un protocole garantit la propriété de voisinage. Ensuite, en fonction des caractéristiques du médium utilisé dans la communication, il faut modéliser les capacités d'un intrus de nouvelle génération. En effet, dans les communications sans fil l'intrus est capable de relayer un message pour faire croire à un agent qu'il est voisin d'un autre alors qu'en réalité les deux agents ne le sont pas. Tout l'intérêt de ce nouveau thème de recherche consiste à modéliser de la façon la plus réaliste possible les échanges de messages entre les participants. Mes travaux antérieurs, en particulier l'augmentation du pouvoir de l'intrus par de nouvelles propriétés algébriques~\citetwo{LLT-rta2005}, me permettront par conséquent de modéliser les capacités de ce dernier afin de capturer les spécificités introduites par les réseaux de communication sans fil. \subsectCV{Modélisation et vérification des Web Services.} \paragraph{Objectif :} Le second axe de mon programme de recherche consiste à prendre en compte l'implantation des protocoles. Je prévois de modéliser et d'analyser l'interaction entre plusieurs services proposés sur internet, appelés <<~Web Services~>>, généralement implantés en XML. \paragraph{Problématique :} Lors d'un achat en ligne, la communication entre l'acheteur et le site internet s'effectue grâce à un protocole cryptographique afin de sécuriser les échanges de données confidentielles. De plus, après avoir demandé les coordonnées de l'utilisateur, le site internet contacte l'organisme bancaire indiqué par le client via un autre protocole cryptographique afin d'effectuer la transaction. L'exécution finale de ce protocole doit être paramétrée d'une part par les politiques de sécurité de chaque service et d'autre part par la politique de sécurité globale attendue. Car, même si les différents protocoles employés lors de cet échange sont sûrs et vérifiés indépendamment, une faille peut appara\^itre lors de leur combinaison et des données confidentielles peuvent \^etre découvertes par l'intrus. Ces attaques reposent sur le fait que les protocoles sont implantés en XML et que les différents services utilisent les mêmes clefs dans différents protocoles. Il est donc important de vérifier automatiquement et formellement l'interaction de ces protocoles. \paragraph{État de l'art :} Peu de travaux jusqu'à présent ont réussi de façon satisfaisante à modéliser et à vérifier l'interaction des Web Services. Cette interaction entre les différents services est une composante importante des protocoles développés de nos jours qui sont de plus en plus complexes et spécialisés utilisant principalement le format XML dans leur implantation. \paragraph{Proposition d'étude :} Fort de mes études sur les protocoles cryptographiques en présence de théories équationnelles, j'envisage d'étudier les Web Services pour assurer aux utilisateurs une plus grande sécurité. Dans mes travaux~\citetwo{THESE-lafourcade06,DLLT-ICALP2006}, j'ai analysé l'interaction de différentes théories équationnelles, j'ai montré de quelle façon les opérateurs algébriques s'appliquent et j'ai proposé une procédure de vérification formelle des protocoles cryptographiques en présence de ces théories équationnelles. Les interactions entre les différents Web Services en XML se modélisent de façon naturelle grâce à de telles théories. C'est pourquoi, les objectifs majeurs dans l'étude des Web Services sont d'abord d'arriver à comprendre et à formaliser les interactions qui les composent puis de développer à partir de cette modélisation une procédure automatique de vérification. \subsectCV{Analyse formelle de protocoles de groupe.} \paragraph{Objectif :} Ce thème de recherche couvre deux des aspects des protocoles cryptographiques que je souhaite explorer : le premier est de vérifier une propriété du protocole (le secret), et le second est de prendre en compte l'environnement dans lequel il est exécuté (le nombre de participants). \paragraph{Problématique :} Les protocoles de groupe sont utilisés pour distribuer une clef entre les différents participants du groupe. Ils permettent d'introduire un nouveau participant au sein d'un groupe existant, ou d'en exclure un des membres. La spécificité de ces protocoles vient de leur conception même car ils sont élaborés pour un nombre quelconque d'agents. Ces protocoles fonctionnent grâce à un échange de messages récursifs entre les différents participants. C'est-à-dire que les différents traitements sur les messages sont effectués de manière récursive. Ce procédé permet au protocole d'être applicable quel que soit le nombre d'agents. Il est donc particulièrement important de vérifier ces protocoles pour un nombre quelconque de participants. \paragraph{État de l'art :} Ces protocoles ne sont vérifiés pour le moment que pour un nombre fixé de participants~\citeone{KuestersTruderung-TR-STACS-2007,DBLP:conf/cade/SteelBM04} alors qu'ils sont conçus pour un nombre arbitraire d'agents. Les nombreux outils et méthodes de vérification développés jusqu'à présent analysent ces protocoles pour un nombre fixé de participants, souvent deux ou trois. Ces techniques ne sont pas adaptées à la vérification pour un nombre quelconque d'agents en raison de leur conception même : elles nécessitent de définir le rôle de chacun des participants. \paragraph{Proposition d'étude :} Je souhaite donc étudier les protocoles de groupe afin d'en dégager une classe de protocoles <<~récursifs~>>. A cet égard, une modélisation en clauses de Horn me permettra de déterminer une sous-classe de protocoles <<~récursifs~>> pour laquelle la vérification de la propriété de secret sera décidable. Cette abstraction par les clauses de Horn permettra de capturer le caractère récursif de ces protocoles cryptographiques. J'envisage dans un deuxième temps de regarder s'il n'est pas suffisant de vérifier les protocoles <<~récursifs~>> pour un nombre borné d'agents en m'inspirant du résultat obtenu par V.~Cortier et H.~Comon~\citeone{ComonLC-SCP04} selon lequel il suffit d'un seul intrus en plus des participants honnêtes pour analyser les protocoles. \subsectCV{Vérification de protocoles de vote et de vente aux enchères.} \paragraph{Objectif :} Les protocoles de vote et de vente aux enchères utilisent souvent, pour garantir certaines propriétés, des opérateurs algébriques munis de théories équationnelles particulières. Ces deux classes de protocoles peuvent être analysées du point de vue des opérateurs algébriques utilisés ainsi qu'au travers des nouvelles propriétés qu'ils visent à garantir. \subsection*{Protocoles de vente aux enchères.} \paragraph{Problématique :} Les protocoles de vente aux enchères ({\it e-auction}) fleurissent de nos jours sur internet. Ces protocoles doivent garantir de nombreuses propriétés comme l'anonymat des acheteurs et des vendeurs, l'équité entre les acheteurs, la confidentialité des propositions d'achat et de vente, l'authentification des participants et la bonne conformité de la procédure de vente. Toutes ces propriétés sont garanties par différentes étapes du protocole et par des opérateurs algébriques dans la spécification même du protocole. \paragraph{État de l'art :} Je n'ai recensé aucune analyse formelle et vérification automatique dans la littérature concernant les propriétés que doivent assurer les protocoles de ventes aux enchères. \paragraph{Proposition d'étude :} En conséquence, fort d'un premier travail~\citetwo{KL-eth07} dans lequel nous avons trouvé une faille sur un protocole d'enchère électronique, je me propose d'explorer cette nouvelle famille de protocoles. Je pense utiliser le Pi-calcul pour modéliser les propriétés spécifiques que doivent garantir les protocoles de vente aux enchères électroniques, comme l'équité entre les participants ou encore l'anonymat des vendeurs. Ensuite, de nombreuses phases de ces protocoles utilisent des opérateurs algébriques pour assurer certaines de ces propriétés. Mes travaux de thèse~\citetwo{THESE-lafourcade06} sur les théories équationnelles seront de la plus grande utilité pour commencer la vérification de ces protocoles. \subsection*{Protocoles de vote.} \paragraph{Problématique :} Avec la démocratisation d'internet, de nombreux pays songent à employer des protocoles de vote électronique pour leurs élections. Il existe d'ores et déjà de nombreux protocoles de vote électronique. La peur des électeurs face aux fraudes éventuelles dues à ce nouveau système de vote est réelle : comment garantir qu'une personne ne vote qu'une seule fois, l'anonymat des électeurs, la confidentialité des bulletins de vote... Ces propriétés sont assurées dans de nombreux protocoles de vote proposées par des opérateurs cryptographiques, comme le chiffrement de Naccache et Stern~\citeone{Naccache:1997:NPK}. Une analyse formelle permettrait de garantir la sécurité de cette nouvelle procédure électorale et contribuerait sans doute à augmenter la confiance des citoyens. \paragraph{État de l'art :} \`A ma connaissance, quelques travaux~\citeone{KremerRyan2005,DKR-csfw06} effectuent une analyse formelle des propriétés que doivent assurer les protocoles de vote. Cependant aucun d'entre eux ne prend en compte les propriétés algébriques des opérateurs employés dans la spécification du protocole. \paragraph{Proposition d'étude :} Fort de mon travail de thèse sur les opérateurs homomorphiques et les chiffrements distributifs~\citetwo{THESE-lafourcade06,Laf-secret06,LLT-icomp07}, j'envisage d'étudier les protocoles de vote qui, pour satisfaire la confidentialité des bulletins de vote, utilisent souvent des fonctions de chiffrement dites <<~homomorphiques~>>. Je pense alors proposer une analyse des propriétés requises par un protocole de vote, comme l'anonymat des votants ou la confidentialité des votes, ceci en prenant en compte les propriétés algébriques utilisées. Car, comme mes travaux l'ont démontré, il se peut qu'un protocole soit prouvé sûr et qu'une faille existe en prenant en compte une propriété algébrique utilisée par la spécification du protocole. Il est donc nécessaire d'effectuer une telle analyse pour vérifier correctement les protocoles de vote électronique. \subsectCV{Intégration dans un laboratoire de recherche.} Mon programme de recherche correspond aux thèmes étudiés par l'équipe Verimag à Grenoble. Plusieurs chercheurs de ce laboratoire travaillent sur la sécurité informatique et la vérification formelle de protocoles cryptographiques (Liana \textsc{Bozga}, Judicaël \textsc{Courant}, Yassine \textsc{Lakhnech}, Jean-François \textsc{Monin}, Michael \textsc{Périn}). Le second et le quatrième volet de mon projet de recherche qui visent respectivement à analyser l'interaction entre plusieurs Web Services et les protocoles de vote et de vente aux enchères, impliquent l'utilisation de notions temporelles, domaine auquel Yassine \textsc{Lakhnech} et son équipe s'intéresse. De plus, Jean-François \textsc{Monin} et Judicaël \textsc{Courant} s'intéressent aux propriétés algébriques des protocoles cryptographiques en utilisant COQ~\citeone{courantmonin06wits}. Enfin l'outil Hermes~\citeone{bozga03cav} développé par l'équipe Verimag est un des seuls outils à l'heure actuelle permettant de considérer un nombre non-bornés de sessions. Il est donc naturel d'essayer d'implanter dans cet outil mes travaux de thèse sur l'interaction d'un symbole homomorphique et le <<~ou-exclusif~>>. Mon programme de recherche s'inscrit bien dans la thématique de l'équipe Verimag, tout en apportant de nouveaux axes de recherche sur la modélisation et la vérification des nouvelles propriétés des protocoles de communication sans fil, de ventes aux enchères et de vote élecrtonique. \subsectCV{Références.} \vspace{-1cm} \makeatletter \let\thebibliography\savemultibiblio \let\endthebibliography\endsavemultibiblio \let\@bibitem\@savemultibibitem \let\@lbibitem\@lsavemultibibitem \makeatother \bibliographystyleone{abralpha} \bibliographyone{biblio} \newpage \section{Listes des pièces jointes.} \begin{description} \item[Piéces administratives :]\ \begin{itemize} \item Photocopie de la carte d'identité. \item Déclaration ANTARES. \item Copie de l'attestation de délivrance de doctorat. \item Copies des deux rapports de pré-soutenance (Lucas \textsc{Vigan\`o} et Yassine \textsc{Lakhnech}). \item Copie du rapport de soutenance. \end{itemize} \item[Enseignements :]\ \begin{itemize} \item Lettre de recommandation de ma tutrice de monitorat (Danièle \textsc{Beauquier}). \item Lettre de recommandation de ma responsable d'enseignement à l'IUT (Régine \textsc{Laleau}). \item Copie de l'attestation de monitorat du C.I.E.S. de Jussieu. \end{itemize} \item[Recherche :]\ \begin{itemize} \item Lettre de recommandation de Michael \textsc{Rusinowitch}. \item Lettre de recommandation de mon responsble de post-doctorat (David \textsc{Basin}). \item Lettre de recommandation de mes directeurs de thèse (Denis \textsc{Lugiez} et Ralf \textsc{Treinen}). \item Lettre de recommandation d'une de mes co-directrices de DEA (Marie-Christine \textsc{Lagasquie-Schiex}). \end{itemize} \item[Publications jointes lors de l'audition:]\ \def\refname{~} \begin{thebibliography}{4} \vspace{-1.5cm} \bibitem[1]{LLT-icomp07} P.~Lafourcade, D.~Lugiez, and R.~Treinen. \newblock Intruder deduction for the equational theory of abelian groups with distributive encryption. \newblock {\em Information and Computation}, 205(4):581--623, Apr. \bibitem[2]{CDL05-survey} V.~Cortier, S.~Delaune, and P.~Lafourcade. \newblock A survey of algebraic properties used in cryptographic protocols. \newblock {\em Journal of Computer Security}, 14(1):1--43, 2006. \bibitem[4]{DLLT-ICALP2006} S.~Delaune, P.~Lafourcade, D.~Lugiez, and R.~Treinen. \newblock Symbolic protocol analysis in presence of a homomorphism operator and {\emph{exclusive~or}}. \newblock In M.~Buglesi, B.~Preneel, V.~Sassone, and I.~Wegener, editors, {\em {P}roceedings of the 33rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'06)~--- {P}art~{II}}, volume 4052 of {\em Lecture Notes in Computer Science}, pages 132--141, Venice, Italy, July 2006. Springer. \bibitem[6]{THESE-lafourcade06} P.~Lafourcade. \newblock {\em V{\'e}rification des protocoles cryptographiques en pr{\'e}sence de th{\'e}ories {\'e}quationnelles}. \newblock Th{\`e}se de doctorat, Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France, Sept. 2006. \newblock 209~pages. \end{thebibliography} \item[Adresses des personnes m'ayant recommandé :]\ \begin{tabular}[t]{l} \bf Prof. Michael RUSINOWITCH \\ LORIA-INRIA-Lorraine \\ 615, rue du Jardin Botanique, BP 101, \\ 54602 Villers les Nancy Cedex, France \\ Phone: +33 3 83 59 30 20\\ Email: {\tt Michael.Rusinowitch@loria.fr}\\ \end{tabular} \begin{tabular}[t]{l} \bf Prof. David BASIN\\ ETH Z\"urich, IFW C 49.2 \\ Haldeneggsteig 4 / Weinbergstrasse\\ 8092 Zürich, SWITZERLAND \\ Phone: +41 44 632 72 45\\ Email: {\tt basin@inf.ethz.ch} \end{tabular} \begin{tabular}[t]{ll} \bf Prof. Denis LUGIEZ &\bf Ralf TREINEN, Maître de Conférences \\ Université de Provence Marseille &Laboratoire Spécification et Vérification\\ Centre de Mathématiques et d'Informatique & École Normale Supérieure de Cachan \\ 39 rue Joliot Curie,&61, avenue du Président Wilson \\ 13453 MARSEILLE, FRANCE & 94235 CACHAN Cedex - France \\ Phone: (+33) 4 91 11 36 23& Phone: +33 1 47 40 75 67\\ Email: {\tt lugiez@cmi.univ-mrs.fr}& Email: {\tt treinen@lsv.ens-cachan.fr} \end{tabular} \begin{tabular}[t]{l} \bf Marie-Christine LAGASQUIE-SCHIEX, Maître de Conférences \\ Institut de recherche en informatique de Toulouse,\\ 118 route de Narbonne, \\ 31062 Toulouse Cedex 4, France. \\ Phone: +33 (0)5 61 55 64 51\\ Email: {\tt Philippe.Balbiani@irit.fr} \end{tabular} \begin{tabular}[t]{l} \bf Prof. Danièle BEAUQUIER\\ Département d'Informatique \\ Université Paris 12 \\ Bat P2 - 2e étage - Bureau 220 \\ 61 Avenue du Général de Gaulle \\ 94010 Créteil CEDEX, France\\ Phone: +33 01 45 17 16 44 \\ E-mail: {\tt beauquier@univ-paris12.fr} \end{tabular} \begin{tabular}[t]{l} \bf Prof. Régine LALEAU \\ Université Paris 12-IUT \\ Département Informatique \\ Route forestière Hurtault \\ F-77300 Fontainebleau, France \\ Phone: +33 (0)1 60 74 68 40 \\ E-mail: {\tt laleau@univ-paris12.fr} \end{tabular} \end{description} \end{document}