TURUANI Mathieu

          Full-time INRIA researcher (CR2) at the Loria-INRIA laboratory, Nancy, France.

          eMail :         eMail               Office : A 211
          Tel work :    (+33 / +0)  35 495-8526     Tel home :  (+0) 38 325-4598
          Address :     LORIA - Campus Scientifique - BP 239 - 54506 Vandoeuvre-lès-Nancy Cedex - France

Research
Interests :
 Automatic Verification performed in the CASSIS team, under the direction of  Michaël RUSINOWITCH
 My work has many connections with the CASRUL automatic verification system and the AVISPA European Project.
 
Downloads :

 These files are in french language.
  •  My thesis : "Security of Cryptographic Protocols: Decidability and Complexity" in ps or pdf
  •  A detailed summary of my thesis, with publications and references (for AFIT)

School
graduates :
Entry in the "Ecole Normale Superieure de Cachan" school.  (ENS-Cachan)

Licence and Master of Mathematics.

Magistere of Mathematics and Computer Science. (Mention Très Honorable)

DEA of Computer Science :  "Semantic, Proof, Language", Paris VII Jussieu. (Mention Très Bien)

  • Standard Lessons :
- Terms in First-order Logic.
- Lambda-calculus.
- Constructive Proofs.
- Semantic of sequencial programs.
- Typing and Programation
  • Optional Lessons :
- Calculus of inductive Constructions.
- Verification of Concurent systems.
- Linear Logic and pattern calculus.
  • Stage : at the LSV research lab (Laboratoire de Spécification et Vérification), ENS-Cachan. Under the direction of Ph. Schnoebelen and F. Laroussinie : 
Logique Temporelle Temporisée pour la Vérification de Programmes: Expressivité et Complexité.
My DEA Report is available at the LSV research center.

PhD of Computer Sciences :

Security of Cryptographic Protocols: Decidability and Complexity

in the CASSIS team, LORIA-INRIA (Nancy), under the direction of Michaël Rusinowitch. Presented on Dec. 11, 2003. See above for a detailed summary.

PostDoc in the Computer Science Department of the Stanford University, USA..

Now full-time INRIA researcher (CR2) at the Loria-INRIA laboriatory, team CASSIS, Nancy, France.

Thesis
description :

(short version)
     My thesis is focused on the theoretical aspects of the Protocol Insecurity Problem. This problem consists in deciding if a given cryptographic protocol, which is basically an exchange of messages between clients and servers, admits an "attack" or not. An attack is the possibility for an intruder following the Dolev-Yao model to acquire some secret message or to be authenticated in place of someone else. The Dolev-Yao model allows the intruder to intercept or send messages, to use the standard operators like encryption or decryption operators, but he cannot decrypt a message without the needed key. This is the "Perfect Encryption Hypothesis".
     I have first studied the theoretical complexity of this problem when the number of sessions is finite (but without any other constraint, i.e. with unbounded message sizes). I have proved that this is NP-complete. This result was presented in CSFW'14 and has been published in TCS. This work has been extended to improve the intruder and protocol models in different ways. For example, it is proved that the Protocol Insecurity Problem is still NP-Complete if we add the XOR operator (many of its properties). This work relaxes the too restrictive "Perfect Encryption" hypothesis: we can now model protocols using the XOR operator and find attacks w.r.t the XOR properties. Moreover, this result considers the XOR properties as a particular case of a more general set of additional intruder properties, called oracle rules, and prove that the complexity is still NP in this case. This result has been presented in LICS'03.
     In the same way, the initial result is extended to cover operators with Abelian Group properties, when the intruder can build the inverse in the abelian group. The main difficulty in this problem is bounding the message integer coefficients used in any minimal attack. This was used to improve the Dolev-Yao model of intuder with the Diffie-Hellman properties of exponentiations. This will be presented in FSTCS'2003, and shows that the insecurity problem with DH properties of exponentiation is NP-complete.
     In this work, the intruder was allowed to compute the inverse of any term (for a product operator). We have also considered the case where the intruder cannot compute such an inverse. This allow us to describe some cases where the encryption operator is commutative (or any other operator with the same structure). As for XOR and for DH, this result weakens the perfect encryption hypothesis. This shows that the insecurity problem with commutative encryption is NP-complete. Also, I have proved that Insecurity is decidable (and NP-complete) for simple Ping-Pong protocols but with infinite sessions and commuting encryption operators. This result can be contrasted with the non-commuting case studied by Dolev and Yaho which is polynomial.
     But it is also possible to extend the protocol model in different ways. An extension of the oracle rules allows the use of Y. Chevalier's so called Parallel rules, which modelise an approximation of infinite concurrent runs of a protocol (in our model, infinite number of sessions is undecidable). This result proves that the Insecurity problem with such parallel rules is still NP-complete. Even if some models equivalent to Y.C.'s parallel rules have already be studied, it is the first time that the lower bound complexity is proved.
     Finally, I report an implementation of an efficient decision procedure for finite sessions (free algebra) in the protoype ATSE, developed in the context of the AVISPA european project  (homepage: http://www.avispa-project.org/).
 
 International
Journals :
On the expressivity and complexity of the quantitative branching-time temporal logic.
Theoretical Computer Science, Volume 297, Issues 1-3, Pages 1-510 (17 March 2003).
Joint work with F.Laroussinie and Ph.Schnoebelen,

Protocol Insecurity with Finite Number of Sessions is NP-complete.
Theoretical Computer Science, Volume 299 (2003), Pages 451-475.
Joint work with M.Rusinowitch.
 

International
Conferences :

with selection and proceeding

An extension of my DEA has been published in LATIN'2000 :
On the expressivity and complexity of the quantitative branching-time temporal logic
Latin American Theoretical INformatics, April 10-14, 2000  Punta del Este, Uruguay.
F.Laroussinie, Ph.Schnoebelen, and M.Turuani.

Protocol Insecurity with Finite Number of Sessions is NP-complete
14th IEEE Computer Security Foundations Workshop June 11-13, 2001 Cape Breton, Nova Scotia, Canada

joint work with M. Rusinowitch. 

The AVISS Security Protocols Analysis Tool.
Conference on Computer-Aided Verification, Jully 27-31, 2002, Copenhagen, Danmark.

From all the AVISS team.

An NP Decision Procedure for Protocol Insecurity with XOR.
Logic In Computer Science (LICS), June 22-25, 2003, Ottawa, Canada.

joint work with Y.Chevalier, R.Küsters, and M.Rusinowitch.

Extending the Dolev-Yao Intruder for Analysing an Unbounded Number of Sessions.   Technical Report : pdf
Accepted to Computer Science Logic (CSL'2003), Vienna, Austria. Joint work with Y.Chevalier, R.Küsters, M.Rusinowitch, and L.Vigneron.
joint work with Y.Chevalier, R.Küsters, M.Rusinowitch, and L.Vigneron.

Deciding the Security of Protocols with Diffie-Hellman Exponentiation and Product in Exponents.
Accepted to Foundations of Software Technology and Theoretical Computer Science (FSTTCS'2003).

joint work with Y.Chevalier, R.Küsters, and M.Rusinowitch.

References a bit outdated, i.e. Under (Re)construction 

Draft :

Deciding the Security of Protocols with Commuting Public Key Encryption.
joint work with Y.Chevalier, R.Küsters, and M.Rusinowitch.

Seminars : Security Verification of Cryptographic Protocols.
at the Polytechnic School of Montréal, invited by John Mullins.

Protocol Insecurity with Finite Number of Sessions but Unbounded Message Sizes is NP-Complete.
at the Concordia University of Montréal, invited by Sofiene Tahar.

Deciding insecurity for non-atomic keys.
In Dagstuhl Seminar on Specification and Analysis of Secure Cryptographic Protocols. (Dagstuhl, RFA). 2001. 

The CASRUL tool and the Protocol Insecurity Problem.
during the Doctorat Honoris Causa of M.Vardi at Orléans.

Verification of Cryptographic protocols with the Xor operator.
at the Polytechnic School of Montréal, invited by John Mullins.

Valid HTML 4.01!