| TURUANI Mathieu
Full-time INRIA researcher (CR2) at the Loria-INRIA laboratory, Nancy,
| Automatic Verification performed in the CASSIS team, under the
direction of Michaël
My work has many connections with the CASRUL automatic verification system and the AVISPA European Project.
These files are in french language.
|Entry in the "Ecole Normale Superieure de 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)
- Terms in First-order 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
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.
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.
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/).
the expressivity and complexity of the quantitative branching-time
Theoretical Computer Science, Volume 297, Issues 1-3, Pages 1-510 (17 March 2003).
Joint work with F.Laroussinie and Ph.Schnoebelen,
Insecurity with Finite Number of Sessions is NP-complete.
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.
Insecurity with Finite Number of Sessions is NP-complete
AVISS Security Protocols Analysis Tool.
Decision Procedure for Protocol Insecurity with XOR.
the Dolev-Yao Intruder for Analysing an Unbounded Number of Sessions.
Technical Report : pdf
the Security of Protocols with Diffie-Hellman Exponentiation and
References a bit outdated, i.e.
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
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.
Deciding insecurity for non-atomic
The CASRUL tool and the Protocol Insecurity Problem.
Verification of Cryptographic protocols with the Xor