|
|
Jean GOUBAULT-LARRECQ
Professeur associé
Laboratoire Spécification et Vérification
CNRS UMR 8643
École Normale Supérieure de Cachan
61, avenue du Président Wilson
94235 CACHAN Cedex - France
|
|
|
- Ma clé publique GPG (mais attention au spoofing...)
- Quelques cours courants:
- L'exposé au séminaire Regards Croisés mathématiques-physique.
En plusieurs parties: d'abord ça; au transparent
13, allez faire un détour via cette belle animation.
J'y ai aussi présenté diverses autres choses, qui ne sont pas sur les
transparents: l'attaque de Joux sur le protocole corrigé de Needham-Schroeder-Lowe (la version corrigée du protocole de Needham-Schroeder, p.40), le protocole de distribution de clé de Diffie-Hellman, comment jouer au poker au téléphone (sans que les interlocuteurs se fassent confiance, bien entendu), les protocoles zero-knowledge, en particulier via 3-coloriage de graphes. Allez
voir le livre
de Goldwasser et Bellare, en particulier les chapitres 10 (Diffie-Hellman), les sections 11.1.3, 11.1.4, et 11.2.
- Autres notes de cours
- La page d'ORCHIDS,
un logiciel de détection d'intrusions temps réel, multi-événements, multi-sources,
fondé sur une approche efficace de model-checking de logique temporelle
(en cours de développement).
- La page de CSur,
un outil en cours de développement d'analyse statique de code C,
dont le but est de détecter des fuites de secrets (comme dans
les protocoles cryptographiques, mais sur du code C réel).
- le langage HimML
- La suite H1: une bibliothèque d'automates d'arbres finis, de contraintes ensemblistes, de démonstration automatique pour la classe décidable H1. Ecrit principalement en HimML.
- L'outil de vérification de protocoles cryptographiques
ISpi
(version préliminaire), avec documentation provisoire.
Développé dans le cadre du projet RNTL Prouvé.
- Quelques exposés récents:
- L'exposé "Cryptographic Protocol Analysis on Real C Code", présenté
à VMCAI'05, 19 février 2005;
- L'exposé "Relations logiques pour types monadiques ... et homologie?" du séminaire CATIA, Université Montpellier II, 14 février 2003 : ps pdf;
- L'exposé "Une fois qu'on n'a pas trouvé de preuve,
comment le faire comprendre
à un assistant de preuve?", journées francophones des langages
applicatifs (JFLA'04),
26 janvier 2004.
Il y est notamment question de protocoles cryptographiques, de logique,
d'automates d'arbres, et de l'outil H1.
Version étendue à SASYFT'2004 (ci-dessous), en anglais.
- L'exposé "On cryptographic protocols,
regular tree languages,
and automated deduction", invité à SASYFT'2004, Orléans, France, 21 juin 2004. Un peu étendu par rapport à celui des JFLA'2004, et en anglais.
- L'exposé "Plate-forme de détection d'intrusions Orchids -
Analyse et corrélation temporelle d'évènements en temps réel",
journées INRIA-industrie 2004, 27 janvier 2004.
- L'exposé "protocoles cryptographiques, analyse de code, détection d'intrusions", séminaire de cryptographie de Rennes, 30 janvier 2004. Un petit survol du précédent et de celui des JFLA, avec en plus l'attaque OpenSSL v2 comme transition habile entre les premier et troisième thèmes de l'exposé. (Où est passé le second? Je n'en ai effectivement pas parlé.)
- Les contrats que je gère au LSV, ou auxquels je participe:
- le projet INRIA Futurs SECSI (responsable scientifique);
- L'ACI NIM GeoCal (Géométrie du Calcul);
- Le projet RNTL Prouvé (membre).
- L'ARA SSIA FormaCrypt (méthodes formelles et cryptologie), accepté (gérée par Bruno
Blanchet)
- Anciens contrats:
- le projet DICO (responsable);
- l'ACI Jeunes Chercheurs Intrusion (titulaire);
- l'ACI cryptologie PSI-robuste (responsable);
- le projet EVA (participant);
- l'ACI cryptologie VERNAM (participant);
- L'atelier "Sécurité des Communications sur Internet" (SECI'02, Tunis, 19-21 septembre 2002), dont je suis président du comité de programme:
- Les actes, en PDF ou en Postscript (un seul gros fichier bien massif);
- Le sommaire, avec pointeurs vers les papiers individuels;
- Les actes, papier par papier comme ci-dessus, mais dans une seule archive gzippée.
|
|