Logique Temporelle Temporisée pour la Vérification de Programmes: Expressivité et Complexité.

     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/).