TURUANI Mathieu
Fulltime INRIA researcher (CR2) at the LoriaINRIA laboratory, Nancy,
France.
eMail
:
Office : A 211


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.

School graduates : 
Entry in the "Ecole Normale Superieure de Cachan"
school. (ENSCachan)
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)
 Terms in Firstorder Logic.
 Calculus of inductive Constructions.
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, LORIAINRIA (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 fulltime INRIA researcher (CR2) at the LoriaINRIA laboriatory, team CASSIS, Nancy, France.

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 DolevYao model to acquire some secret message or to be
authenticated in place of someone else. The DolevYao 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 NPcomplete. 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 NPComplete 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 DolevYao model of intuder with the DiffieHellman properties of exponentiations. This will be presented in FSTCS'2003, and shows that the insecurity problem with DH properties of exponentiation is NPcomplete. 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 NPcomplete. Also, I have proved that Insecurity is decidable (and NPcomplete) for simple PingPong protocols but with infinite sessions and commuting encryption operators. This result can be contrasted with the noncommuting 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 NPcomplete. 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.avispaproject.org/). 
International
Journals : 
On
the expressivity and complexity of the quantitative branchingtime
temporal logic. Theoretical Computer Science, Volume 297, Issues 13, Pages 1510 (17 March 2003). Joint work with F.Laroussinie and Ph.Schnoebelen, Protocol
Insecurity with Finite Number of Sessions is NPcomplete. 
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 branchingtime temporal logic Latin American Theoretical INformatics, April 1014, 2000 Punta del Este, Uruguay. F.Laroussinie, Ph.Schnoebelen, and M.Turuani. Protocol
Insecurity with Finite Number of Sessions is NPcomplete The
AVISS Security Protocols Analysis Tool. An
NP
Decision Procedure for Protocol Insecurity with XOR. Extending
the DolevYao Intruder for Analysing an Unbounded Number of Sessions.
Technical Report : pdf
Deciding
the Security of Protocols with DiffieHellman Exponentiation and
Product
in Exponents. References a bit outdated, i.e. 
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 NPComplete. Deciding insecurity for nonatomic
keys. The CASRUL tool and the Protocol Insecurity Problem. Verification of Cryptographic protocols with the Xor
operator. 