M. and E. En-particulier, attaques telles que l'attaque par confusion de types et l'attaque par rejeu, qui ne peuvent pasêtrepasêtre abordées avec l'approche de Compa- gna. Nous devons expérimenter d'autres systèmes de planification (e.g. SATPLAN [14] et FF [12]) supportant la spécification PDDL 2.0 (et donc les axiomes), et voir s'ils sont meilleurs que Blackbox avec son codagècodagè a base de Graphplan, Notre approche fournit de nouvelles possibilités pour vérifier des protocoles cryptographiques. Les protocoles industriels tels que le SSL contiennent divers opérateurs algébriques qui devraientêtredevraientêtre considérés. Nous pensons que nous devonsétudierdevonsétudier la coopération avec d'autres approches telles que SATPLAN ou GP- CSP [13]

]. A. Références1, L. Armando, P. Compagna, and . Ganty, Satbased model-checking of security protocols using planning graph analysis, Lecture Notes in Computer Science, vol.2805, pp.875-893, 2003.

B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., 2001.
DOI : 10.1109/CSFW.2001.930138

B. Blanchet, From Secrecy to Authenticity in Security Protocols, SAS '02 : Proceedings of the 9th International Symposium on Static Analysis, pp.342-359, 2002.
DOI : 10.1007/3-540-45789-5_25

L. Compagna, SAT-based Model-Checking of Security Protocols, 2005.

V. Cortier, J. Millen, and H. Rueß, Proving secrecy is easy enough, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., pp.97-108, 2001.
DOI : 10.1109/CSFW.2001.930139

S. Delaune, Vérification des protocoles cryptographiques et propriétés algébriques, 2006.

S. Delaune and F. Klay, Vérification automatique appliquéè a un protocole de commercé electronique, Actes des 6` emes Journées Doctorales Informatique et Réseau, pp.260-269, 2004.

W. Diffie and E. Hellman, New directions in cryptography, IEEE Transactions on Information Theory, vol.22, issue.6, pp.22644-654, 1976.
DOI : 10.1109/TIT.1976.1055638

D. Dolev and A. Yao, On the security of public key protocols, IEEE Transactions on Information Theory, vol.29, issue.2, pp.198-208, 1981.
DOI : 10.1109/TIT.1983.1056650

M. Fox and D. Long, PDDL2.1 : An Extension to PDDL for Expressing Temporal Planning Domains, Journal of Artificial Intelligence Research, 2003.

J. Hoffmann, The Deterministic Part of IPC-4 : An Overview, Journal of Artificial Intelligence Research, vol.24, pp.519-579, 2005.

J. Hoffmann and B. Nebel, The FF planning system : Fast plan generation through heuristic search, Journal of Artificial Intelligence Research, vol.14, pp.253-302, 2001.

S. Kambhampati, Planning graph as a (dynamic ) CSP : Exploiting EBL, DDB and other CSP search techniques in graphplan, Journal of Artificial Intelligence Research, vol.12, pp.1-34, 2000.

H. Kautz, D. Mcallester, and B. Selman, Encoding plans in propositional logic, Proceedings of the Fifth International Conference on the Principle of Knowledge Representation and Reasoning (KR'96), pp.374-384, 1996.

H. Kautz and B. Selman, Unifying SAT-Based and Graph-Based Planning, Based Artificial Intelligence, 1999.

G. Lowe, An attack on the Needham-Schroeder public-key authentication protocol, Information Processing Letters, vol.56, issue.3, pp.131-136, 1995.
DOI : 10.1016/0020-0190(95)00144-2

M. Needham and D. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, vol.21, issue.12, pp.993-999, 1978.
DOI : 10.1145/359657.359659

L. Paulson, Proving properties of security protocols by induction, Proceedings 10th Computer Security Foundations Workshop, pp.70-83, 1997.
DOI : 10.1109/CSFW.1997.596788