Jean Goubault-Larrecq
Full Professor
A one-year software engineer position at INRIA, in Cachan, to work on our open source intrusion detection tool
Orchids
(login: guest, password: guest).
Click here for a description (in Word format)
Apply now!
- My GPG public key (but beware of spoofing...)
- I'm rarely putting any lecture note here, see the French version of this Web page instead.
One exception: the homework assignment in Advanced Complexity, to turn in
by November 24, 2010.
- Some ongoing projects. Beware! I've got
a tendency to try and write a few pages on a given topic
to get things straight, then it ends as a book...
- The Pavé ("cobblestone"): A wonderful theory of games, belief functions, plausibilities,
and previsions in a topological setting: as
pdf.
Current version is 8, and it is big (641 pages, June 28, 2007).
It should have been called version 7, but then it seems that I cannot count after all.
Version 6 was already pretty big (514 pages as of
January 16, 2007). And it's not over yet. I thought that roughly, the first
8 chapters should have remained more or less as they were.
But I still made many changes between January and June 2007.
Note in particular the introduction
of the notion of hemi-distance, and a theorem a la Kantorovitch-Rubinstein
(which I'll use later to do things like bisimulation distances...) In French.
Developed as part of the
ARC ProNoBis.
- A study of geometry of interaction as a foundation for
categorical models of the whole of classical linear logic:
as pdf. 229 pages. Chapter 3 should
be pursued, Chapter 4 is yet to finish, and similarly for
Section 6.4. In English. Developed as part of the
ACI NIM GeoCal.
- The ORCHIDS page.
ORCHIDS is a real-time, multi-event, multi-source intrusion detection tool
based on efficient temporal model-checking algorithms (in
development).
- The CSur page.
CSur is a tool under development that analyzes C programs statically,
in order to detect confidentiality leaks (as in cryptographic
protocols, but on actual C code).
- the HimML language
- The H1 tool suite: a set of tools for handling finite tree automata,
set constraints, doing automated deduction in the decidable class H1.
Written mostly in HimML.
- The ISpi
protocol verification tool (preliminary version), with provisional documentation.
Developed as part of projet RNTL Prouvé.
- A few recent talks:
- "A Few Pearls in the Theory of Quasi-Metric Spaces\
", TACL'11.
- "Logic Wins!", given at ASIAN'09 and at SECCO'10.
- My talk at the Domains IX Workshop on
convex-concave duality, a trick that I often use in the Pavé (see above).
- A talk on Orchids at the RV'08 (Runtime Verification) Workshop (slightly more geared towards algorithmic issues than the related talk at the AARCS'06 workshop, Santa Fe, NM, Nov. 2006). Orchids is our
real-time, multi-event, multi-source intrusion detection system.
- The invited talk "A Biased Survey of Models and Methods for Verifying Cryptographic Protocols", presented at the
Workshop on
Classical and Quantum Information Security, CalTech, Los Angeles, CA,
Decembre 15, 2005.
- The talk "Cryptographic Protocol Analysis on Real C Code", presented
at VMCAI'05, February 19, 2005.
- The talk "On cryptographic protocols,
regular tree languages,
and automated deduction", invited talk at SASYFT'2004, Orléans, France, June 21, 2004.
- The contracts I manage at LSV, or which I am participating in:
- the INRIA Futurs project-team SECSI (scientific director);
- The projet RNTL Prouvé (member).
- The INRIA ARC ProNobis;
- The ARA SSIA FormaCrypt (Formal Methods and Cryptology), accepted (managed by Bruno
Blanchet).
- Old contracts:
- the DICO project (head);
- the "ACI Jeunes Chercheurs" Intrusion (recipient);
- the ACI cryptologie PSI-robuste (head);
- the EVA project (participant);
- the ACI cryptologie VERNAM (participant);
- The ACI NIM GeoCal ("geometry of computation");
- The Workshop "Security of Communications over the Internet" (SECI'02, Tunis, September 19-21 2002), of which I am program committee chairman:
