M. Abadi and V. Cortier, Deciding knowledge in security protocols under equational theories, Theoretical Computer Science, vol.387, issue.12, pp.2-32, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000554

M. Abadi and C. Fournet, Mobile values, new names, and secure communication, Proc. 28th ACM Symposium on Principles of Programming Languages (POPL'01, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01423924

S. Anantharaman, P. Narendran, and M. Rusinowitch, Intruders with Caps, Proc. 18th International Conference on Term Rewriting and Applications (RTA'07), 2007.
DOI : 10.1007/978-3-540-73449-9_4
URL : https://hal.archives-ouvertes.fr/hal-00144178

A. Armando, The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, Proc. 17th Int. Conference on Computer Aided Verification (CAV'05), pp.281-285, 2005.
DOI : 10.1007/11513988_27
URL : https://hal.archives-ouvertes.fr/inria-00000408

M. Arnaud, V. Cortier, and S. Delaune, Combining Algorithms for Deciding Knowledge in Security Protocols, Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS'07), pp.103-117, 2007.
DOI : 10.1007/978-3-540-74621-8_7
URL : https://hal.archives-ouvertes.fr/inria-00129418

M. Backes, C. Hritcu, and M. Maffei, Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus, 2008 21st IEEE Computer Security Foundations Symposium, 2008.
DOI : 10.1109/CSF.2008.26

M. Backes, M. Maffei, and D. Unruh, Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol, 2008 IEEE Symposium on Security and Privacy (sp 2008), 2008.
DOI : 10.1109/SP.2008.23

M. Baudet, Deciding security of protocols against off-line guessing attacks, Proceedings of the 12th ACM conference on Computer and communications security , CCS '05, 2005.
DOI : 10.1145/1102120.1102125

M. Baudet, YAPA (Yet Another Protocol Analyzer), 2008.

M. Baudet, V. Cortier, and S. Delaune, YAPA, Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA'09), pp.148-163, 2009.
DOI : 10.1145/2422085.2422089
URL : https://hal.archives-ouvertes.fr/inria-00426624

M. Berrima, N. B. Rajeb, and V. Cortier, Deciding knowledge in security protocols under some e-voting theories, RAIRO - Theoretical Informatics and Applications, vol.45, issue.3, 2009.
DOI : 10.1051/ita/2011119
URL : https://hal.archives-ouvertes.fr/inria-00638515

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

B. Blanchet, M. Abadi, and C. Fournet, Automated Verification of Selected Equivalences for Security Protocols, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), pp.331-340, 2005.
DOI : 10.1109/LICS.2005.8

Y. Chevalier, Résolution deprobì emes d' accessibilité pour la compilation et la validation de protocoles cryptographiques, 2003.

Y. Chevalier and M. Kourjieh, Key Substitution in the Symbolic Analysis of Cryptographic Protocols, Proc. 27th International Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS'07), pp.121-132, 2007.
DOI : 10.1007/978-3-540-77050-3_10
URL : https://hal.archives-ouvertes.fr/hal-00183337

S. ¸. Ciobâc?-a, S. Delaune, and S. Kremer, Computing knowledge in security protocols under convergent equational theories, Proceedings of the 22nd International Conference on Automated Deduction (CADE'09), pp.355-370, 2009.

R. Corin, J. Doumen, and S. Etalle, Analysing Password Protocol Security Against Off-line Dictionary Attacks, Proc. 2nd International Workshop on Security Issues with Petri Nets and other Computational Models, 2004.
DOI : 10.1016/j.entcs.2004.10.007
URL : http://doi.org/10.1016/j.entcs.2004.10.007

V. Cortier and S. Delaune, Deciding Knowledge in Security Protocols for Monoidal Equational Theories, Proc. 14th Int. Conference on Logic for Programming, Artificial Intelligence , and Reasoning (LPAR'07), LNAI, 2007.
DOI : 10.1007/978-3-540-75560-9_16
URL : https://hal.archives-ouvertes.fr/inria-00181620

V. Cortier, S. Delaune, and P. Lafourcade, A survey of algebraic properties used in cryptographic protocols, Journal of Computer Security, vol.14, issue.1, pp.1-43, 2006.
DOI : 10.3233/JCS-2006-14101
URL : https://hal.archives-ouvertes.fr/inria-00000552

S. Delaune, S. Kremer, and M. D. Ryan, Verifying privacy-type properties of electronic voting protocols, Journal of Computer Security, vol.17, issue.4, pp.435-487, 2009.
DOI : 10.3233/JCS-2009-0340

S. Kremer and M. D. Ryan, Analysis of an Electronic Voting Protocol in the Applied Pi Calculus, 14th European Symposium on Programming (ESOP'05), pp.186-200, 2005.
DOI : 10.1007/978-3-540-31987-0_14

P. Lafourcade, D. Lugiez, and R. Treinen, Intruder deduction for the equational theory of Abelian groups with distributive encryption, Information and Computation, vol.205, issue.4, pp.581-623, 2007.
DOI : 10.1016/j.ic.2006.10.008
URL : https://hal.archives-ouvertes.fr/hal-00496353

J. Millen and V. 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://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.3643

T. Okamoto, Receipt-free electronic voting schemes for large scale elections, Proc. 5th Int. Security Protocols Workshop, 1997.
DOI : 10.1007/BFb0028157

M. Rusinowitch and M. Turuani, Protocol insecurity with a finite number of sessions and composed keys is NP-complete, Theoretical Computer Science, vol.299, issue.1-3, pp.451-475, 2003.
DOI : 10.1016/S0304-3975(02)00490-5

P. Let, E. =. , and E. , To ease the induction we strengthen the induction hypothesis and prove a slightly stronger statement We define Q (?) as the smallest set that contains(t 1 , r, tp) | ?] such that f (t 1 , r, tp, t 2 ) ? st R E (?) for some t 2 3. [g(x 1 , . . . , x k ) | x 1 , . . . , x k ], where g ? {open, td, f } and ar(g) = k 4. [f (t 1 , r, tp, x) | x], such that f (t 1 , r, tp, t 2 ) ? st R E (?) for some t 2 5. [x | td(x, y, z), y] 6, pp.8-9, 2002.

P. Let and E. , To ease the induction we strengthen the induction hypothesis and prove a slightly stronger statement We define Q (?) as the smallest set that contains: 1. [t | ?], for every t ? st R E (?) 2. [f (x 1 , . . . , x k ) | x 1 , . . . , x k ], where f ? F and ar(f ) = k 3. [sign(t, x) | x], for every t ? st R E (?) 4. [sign(t, t ) | ?], for every t, t ? st R E (?) 5. [x | blind(x, y), y] 6. [sign(x, z) | sign(blind

P. Let and E. , The proof of item 1 is done by induction on the number of saturation steps of Init(?) =? * (F, E) To ease the induction we strengthen the induction hypothesis and prove a slightly stronger statement We define Q (?) as the smallest set that contains: 1. [t | ?], for every t ? st R E (?) 2. [f (x 1 , . . . , x k ) | x 1 , . . . , x k ], where f ? F and ar(f ) = k 3. [plus(s n (x), t) | x], if s n (t)