. Preuve, La preuve est analogue à la preuve du lemme 18

. Preuve, Soit s ? S un site qui n'apparaît pas dans une transition corrupt d'une trace tr ?

?. ?????-?, Sec, H ) de tr , si nous n'avons pas Msg

. La-preuve-de-l, intégrité forte en avant Nous prouvons maintenant que le protocole P1ter satisfait la propriété de l'intégrité forte en avant de la dénition 43. La preuve suit essentiellement la preuve donnée pour le protocole

. Preuve, La preuve est analogue à la preuve du lemme 18

{. Chaînage-est-valide, length(m 3 ) et SITE l (m 3 ) = SITE l (m 3 ), 0 ? l ? length(m 3 ) Étant donné que les sites s 1 , . . . , s n ne sont pas corrompus , length(m 3 )}, tel que OFF j (m 3 ) = OFF j (m 3 ), mais avec j = k + 1 nous avons trouvé des ores telles que OFF j (m 3 ) = OFF j (m 3, parce que nous avons choisi dans la deuxième session un site u = u. Nous concluons que le protocole P1quater ne satisfait pas la propriété de l'intégrité forte en avant

L. Auteurs-du-protocole-p1-ont-armé-que-le-protocole-p1-satisfait-la-propriété-de-l-'intégrité-forte-en-avant, Cette armation est basée sur la croyance qu'une relation de chaînage valide implique qu'un intrus ne peut pas changer les maillons ajouté par des sites non corrompus. Cette croyance s'est avérée fautive avec la découverte de l'attaque mentionnée. Néanmoins, il reste une question intéressante : comment pouvons-nous nous servir d'une relation de chaînage pour garantir des propriétés d'un protocole, si possible ecacement ? En proposant trois protocoles à l'instar du protocole P1, nous avons abordé cette question d'une manière pratique, Nous avons montré que notre modèle formel peut être utilisé à cet égard avec prot

M. Abadi, Security protocols and their properties In Foundations of Secure Computation, Int. Summer School, 1920.

A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna et al., The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, Proc. of the 17th International Conference on Computer Aided Verication, CAV'2005
DOI : 10.1007/11513988_27

URL : https://hal.archives-ouvertes.fr/inria-00000408

L. [. Armando and . Compagna, SATMC: A SAT-Based Model Checker for Security Protocols, Logics in Articial Intelligence, 2004.
DOI : 10.1007/978-3-540-30227-8_68

P. [. Abadi and . Rogaway, Reconciling two views of cryptography (the computational soundness of formal encryption), Proc. of the 2000 International Conference IFIP on Theoretical Computer Science (TCS00, 2000.

M. [. Ateniese, G. Steiner, and . Tsudik, New multiparty authentication services and key agreement protocols, IEEE Journal on Selected Areas in Communications, vol.18, issue.4, 2000.
DOI : 10.1109/49.839937

A. [. Bellare, D. Desai, P. Pointcheval, and . Rogaway, Relations among notions of security for public-key encryption schemes, Proc. of the 18th Annual International Cryptology Conference on Advances in Cryptology (CRYPTO98), 1998.
DOI : 10.1007/BFb0055718

S. [. Blum and . Goldwasser, An ecient probabilistic public key encryption scheme which hides all partial information, Proc. of CRYPTO 84 on Advances in cryptology, 1985.
DOI : 10.1007/3-540-39568-7_23

P. [. Boichut, O. Héam, F. Kouchnarenko, and . Oehl, Improvements on the Genet and Klay technique to automatically verify security protocols, Proc. of the 2004 International Workshop on Automated Verication of Innite-State Systems (AVIS04), Electronic Notes in Theoretical Computer Science, 2004.

C. [. Backes and . Jacobi, Cryptographically sound and machine-assisted verication of security protocols, Proc. of the 20th International Symposium on Theoretical Aspects of Computer Science, STACS '03, 2003.

]. B. Bla01 and . Blanchet, An ecient cryptographic protocol verier based on prolog rules

S. [. Blum and . Micali, How to generate cryptographically strong sequences of pseudo random bits, 23rd Annual Symposium on Foundations of Computer Science (sfcs 1982), 1982.
DOI : 10.1109/SFCS.1982.72

S. [. Basin, L. Mödersheim, and . Viganò, OFMC: A symbolic model checker for security protocols, International Journal of Information Security, vol.7, issue.3, 2005.
DOI : 10.1109/CSFW.2001.930145

URL : https://www.research-collection.ethz.ch/bitstream/20.500.11850/69243/1/eth-4775-01.pdf

R. V. Book and F. Otto, The veriability of two-party protocols, Advances in Cryptology : Proc. of a Workshop on the Theory and Application of Cryptographic Techniques (EUROCRYPT85), Lecture Notes in Computer Science, 1986.

D. [. Bull and . Otway, The authentication protocol

M. Backes and B. Ptzmann, Relating symbolic and cryptographic secrecy, Proc. of the 2005 IEEE Symposium on Security and Privacy, p.0, 2005.
DOI : 10.1109/tdsc.2005.25

URL : http://eprint.iacr.org/2004/300.ps.gz

P. [. Bellare and . Rogaway, Random oracles are practical, Proceedings of the 1st ACM conference on Computer and communications security , CCS '93, 1993.
DOI : 10.1145/168588.168596

K. J. Compton and S. Dexter, Proof Techniques for Cryptographic Protocols, Proc. of the 26th International Colloquium on Automata, Languages and Programming (ICALP99), 1999.
DOI : 10.1007/3-540-48523-6_3

I. Cervesato, N. A. Durgin, P. D. Lincoln, J. C. Mitchell, and A. Scedrov, A metanotation for protocol analysis, Proc. of the 12th IEEE workshop on Computer Security Foundations (CSFW99), 1999.

S. [. Cortier, P. Delaune, and . Lafourcade, A survey of algebraic properties used in cryptographic protocols, Journal of Computer Security, vol.14, issue.1, 2006.
DOI : 10.3233/JCS-2006-14101

URL : https://hal.archives-ouvertes.fr/inria-00000552

O. [. Canetti, S. Goldreich, and . Halevi, The random oracle methodology, revisited, Journal of the ACM, vol.51, issue.4, 2004.
DOI : 10.1145/1008731.1008734

URL : http://arxiv.org/pdf/cs/0010019

]. V. Chw06a, H. Cortier, B. Hördegen, and . Warinschi, Explicit randomness is not necessary when modeling probabilistic encryption, Workshop on Information and Computer Security Electronic Notes in Theoretical Computer Science, 2006.

]. V. Chw06b, H. Cortier, B. Hördegen, and . Warinschi, Explicit randomness is not necessary when modeling probabilistic encryption, Research Report, vol.5928, 2006.

V. Cortier, S. Kremer, R. Küsters, and B. Warinschi, Computationally Sound Symbolic Secrecy in the Presence of Hash Functions, Proc. of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06), 2006.
DOI : 10.1007/11944836_18

URL : https://hal.archives-ouvertes.fr/inria-00108386

V. [. Comon-lundh and . Cortier, New decidability results for fragments of rstorder logic and application to cryptographic protocols, Proc. 14th International Conference on Rewriting Techniques and Applications (RTA03), volume 2706 of Lecture Notes in Computer Science, 2003.

P. [. Chavez and . Maes, Kasbah : An agent marketplace for buying and selling goods, First International Conference on the Practical Application of Intelligent Agents and Multi-Agent Technology (PAAM'96). Practical Application Company, 1996.

C. [. Cervesato, D. Meadows, and . Pavlovic, An Encapsulated Authentication Logic for Reasoning about Key Distribution Protocols, 18th IEEE Computer Security Foundations Workshop (CSFW'05), 2005.
DOI : 10.1109/CSFW.2005.7

URL : http://repository.cmu.edu/cgi/viewcontent.cgi?article=1012&context=compsci

[. Chevalier and L. Vigneron, Automated unbounded verication of security protocols, Proc. of the 14th International Conference on Computer Aided Verication (CAV'02), volume 2404 of Lecture Notes in Computer Science, 2002.

B. [. Cortier and . Warinschi, Computationally Sound, Automated Proofs for Security Protocols, Proc. the 14th European Symposium on Programming (ESOP'05), 2005.
DOI : 10.1007/978-3-540-31987-0_12

URL : https://hal.archives-ouvertes.fr/inria-00000556

S. [. Dolev, R. M. Even, and . Karp, On the security of ping-pong protocols, Proc of CRYPTO 82, 1982.

O. [. Doorenbos, D. S. Etzioni, and . Weld, A scalable comparison-shopping agent for the World-Wide Web, Proceedings of the first international conference on Autonomous agents , AGENTS '97, 1997.
DOI : 10.1145/267658.267666

W. Die and M. E. Hellman, New directions in cryptography, IEEE Transactions on Information Theory, issue.6, p.22, 1976.

R. [. Dang and . Kemmerer, Using the ASTRAL model checker for cryptographic protocol analysis, 1997.

G. Denker and J. Millen, CAPSL integrated protocol environment, Proceedings DARPA Information Survivability Conference and Exposition. DISCEX'00, 2000.
DOI : 10.1109/DISCEX.2000.824980

URL : http://www.csl.sri.com/~millen/capsl/cipe.ps

D. Dolev and A. C. Yao, On the security of public key protocols, Proc. of the 22nd IEEE Symposium on Foundations of Computer Science, 1981.

A. [. Fiat and . Shamir, How To Prove Yourself: Practical Solutions to Identification and Signature Problems, Proc. on Advances in cryptologyCRYPTO '86
DOI : 10.1007/3-540-47721-7_12

URL : http://dsns.csie.nctu.edu.tw/research/crypto/HTML/PDF/C86/186.PDF

S. Goldwasser and S. Micali, Probabilistic encryption, Journal of Computer and System Sciences, vol.28, issue.2, 1984.
DOI : 10.1016/0022-0000(84)90070-9

URL : https://doi.org/10.1016/0022-0000(84)90070-9

]. O. Gol93 and . Goldreich, A uniform-complexity treatment of encryption and zero-knowledge

D. Harkins and D. Carrel, The Internet Key Exchange (IKE). The Internet Society, 1998.
DOI : 10.17487/rfc2409

J. Herzog, A computational interpretation of Dolev???Yao adversaries, Theoretical Computer Science, vol.340, issue.1, 2005.
DOI : 10.1016/j.tcs.2005.03.003

M. [. Jacquemard, L. Rusinowitch, and . Vigneron, Compiling and Verifying Security Protocols, Logic for Programming and Automated Reasoning (LPAR'00), volume 1955 of Lecture Notes in Computer Science, 2000.
DOI : 10.1007/3-540-44404-1_10

URL : https://hal.archives-ouvertes.fr/inria-00099161

N. [. Karjoth, C. Asokan, . [. Gülcü, T. Küsters, and . Truderung, Protecting the computation results of free-roaming agents On the automatic analysis of recursive security protocols with XOR, Proc. the 2nd International Workshop on Mobile Agents Proc. of the 24th Symposium on Theoretical Aspects of Computer Science, 1998.

]. R. Küs05 and . Küsters, On the decidability of cryptographic protocols with open-ended data structures, 2005.

T. [. Küsters, C. Wilke, and . Kiel, Automata-Based Analysis of Recursive Cryptographic Protocols, 2003.
DOI : 10.1007/978-3-540-24749-4_34

T. [. Küsters and . Wilke, Automata-Based Analysis of Recursive Cryptographic Protocols, 21st Symposium on Theoretical Aspects of Computer Science, 2004.
DOI : 10.1007/978-3-540-24749-4_34

]. K. Kür06 and . Kürtz, Automatic analysis of recursive cryptographic protocols. Master's thesis, Christian-Albrechts, 2006.

]. G. Low95 and . Lowe, An attack on the needham-schroeder public-key authentication protocol, Information Processing Letters, vol.56, issue.3, 1995.

]. G. Low96 and . Lowe, Breaking and xing the Needham-Schroeder public-key protocol using FDR, Proc. of Tools and algoritms for the construction and analysis of systems (TACAS'96, 1996.

. Lowe and . Casper, A compiler for the analysis of security protocols, Proc. of The 10th Computer Security Foundations Workshop (PCSFW97), 1997.

G. Lowe, Casper : A compiler for the analysis of security protocols, Proc. of the 10th Computer Security Foundations Workshop (CSFW'97, 1997.

G. Lowe, A hierarchy of authentication specications, Proc. of the 10th Computer Security Foundations Workshop (CSFW'97, 1997.

C. Meadows, The NRL protocol analyzer : An overview, Journal of Logic Programming, vol.26, issue.2, 1996.
DOI : 10.1016/0743-1066(95)00095-x

URL : https://doi.org/10.1016/0743-1066(95)00095-x

]. C. Mea00 and . Meadows, Extending formal cryptographic protocol analysis techniques for group protocols and low-level cryptographic primitives, First Workshop on Issues in the Theory of Security WITS'00, 2000.

]. C. Mea01 and . Meadows, Open issues in formal methods for cryptographic protocol analysis

V. [. Millen and . Shmatikov, Constraint solving for bounded-process cryptographic protocol analysis, Proceedings of the 8th ACM conference on Computer and Communications Security , CCS '01, 2001.
DOI : 10.1145/501983.502007

URL : http://www.cs.utexas.edu/~shmat/shmat_ccs01.pdf

D. Maughan, M. Schneider, M. Schertler, and J. Turner, Security Association and Key Management Protocol (ISAKMP) The Internet Society, 1998.
DOI : 10.17487/rfc2408

A. J. Menezes, P. C. Van-oorschot, and S. Vanstone, Handbook of Applied Cryptography, 1996.
DOI : 10.1201/9781439821916

B. [. Micciancio and . Warinschi, Soundness of Formal Encryption in the Presence of Active Adversaries, Theory of cryptography conference -Proceedings of TCC 2004, p.133151, 2004.
DOI : 10.1007/978-3-540-24638-1_8

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

M. [. Naor and . Yung, Public-key cryptosystems provably secure against chosen ciphertext attacks, Proceedings of the twenty-second annual ACM symposium on Theory of computing , STOC '90, 1990.
DOI : 10.1145/100216.100273

URL : http://www.wisdom.weizmann.ac.il/~naor/PAPERS/cca.ps.gz

L. Paulson, Mechanized proofs for a recursive authentication protocol, Proceedings 10th Computer Security Foundations Workshop, 1997.
DOI : 10.1109/CSFW.1997.596790

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

L. C. Paulson, The inductive approach to verifying cryptographic protocols, Journal of Computer Security, vol.6, issue.1-2, 1998.
DOI : 10.3233/JCS-1998-61-205

URL : http://www.cl.cam.ac.uk/~lp15/papers/Auth/jcs.pdf

R. [. Perrig, J. Canetti, D. Tygar, and . Song, Ecient authentication and signing of multicast streams over lossy channels, Proc. of the 2000 IEEE Symposium on Security and Privacy, 2000.

J. [. Pereira and . Quisquater, Security Analysis of the Cliques Protocols Suites: First Results, Proc. of the IFIP TC11 16th Annual Working Conference on Information Security, 2001.
DOI : 10.1007/0-306-46998-7_11

J. [. Pointcheval and . Stern, Security Arguments for Digital Signatures and Blind Signatures, Journal of Cryptology, vol.13, issue.3, 2000.
DOI : 10.1007/s001450010003

URL : http://www.di.ens.fr/~stern/data/St75.ps

]. V. Rot01 and . Roth, On the robustness of some cryptographic protocols for mobile agent protection, Mobile Agents

S. [. Ryan and . Schneider, An attack on a recursive authentication protocol A cautionary tale, Information Processing Letters, vol.65, issue.1, 1998.
DOI : 10.1016/S0020-0190(97)00180-4

]. R. Rsa78a, A. Rivest, L. Shamir, and . Adelman, A method for obtaining digital signatures and public-key cryptosystems, Communications of the ACM, vol.21, issue.2, 1978.

]. R. Rsa78b, A. Rivest, L. Shamir, and . Adleman, A method for obtaining digital signatures and public-key cryptosystems, Communication of the ACM, vol.21, issue.2, 1978.

M. [. Rusinowitch and . Turuani, Protocol insecurity with nite number of sessions is NP-complete, Proc. of the 14th Computer Security Foundations Workshop (CSFW01), 2001.

]. D. Son99 and . Song, Athena : A new ecient automatic checker for security protocol analysis

G. [. Steiner, M. Tsudik, and . Waidner, Die-Hellman key distribution extended to group communication, ACM Conference on Computer and Communications Security, 1996.
DOI : 10.1145/238168.238182

URL : http://www.isi.edu/~gts/CLIQUES/paper/stw96.ps.gz

G. [. Steiner, M. Tsudik, and . Waidner, CLIQUES: a new approach to group key agreement, Proceedings. 18th International Conference on Distributed Computing Systems (Cat. No.98CB36183), 1998.
DOI : 10.1109/ICDCS.1998.679745

URL : http://www.zurich.ibm.com/security/publications/./1997/STW97.ps.gz

J. [. Thayer, J. Herzog, and . Guttman, Strand spaces : Proving security protocols correct, IEEE Journal of Computer Security, vol.7, 1999.

T. Truderung, Selecting Theories and Recursive Protocols, 2005.
DOI : 10.1007/11539452_19

URL : http://www.ii.uni.wroc.pl/~tt/papers/concur05.pdf

C. Theory, Lecture Notes in Computer Science, 2005.

A. C. Yao, Theory and application of trapdoor functions, 23rd Annual Symposium on Foundations of Computer Science (sfcs 1982), 1982.
DOI : 10.1109/SFCS.1982.45

L. Chevalier, J. Compagna, P. Cuellar, J. Hankes-drieslma, S. Mantovani et al., A high level protocol specication language for industrial security-sensitive protocols, Proc. of the Workshop on Specication and Automated Processing of Security Requirements, 2004.

]. B. Yee97 and . Yee, A sanctuary for mobile agents, 1997.