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

M. Abadi and C. Fournet, Private authentication, Theoretical Computer Science, vol.322, issue.3, pp.427-476, 2004.
DOI : 10.1016/j.tcs.2003.12.023

M. Abadi and A. D. Gordon, A calculus for cryptographic protocols, Proceedings of the 4th ACM conference on Computer and communications security , CCS '97, pp.1-70, 1999.
DOI : 10.1145/266420.266432

R. Affeldt and H. Comon-lundh, Verification of Security Protocols with a Bounded Number of Sessions based on Resolution for Rigid Variables, Formal to Practical Security. LNCS, State-of-the- Art Survey, pp.1-20, 2009.

S. Anantharaman, P. Narendran, and M. Rusinowitch, Intruders with Caps, Proc. 18th International Conference on Term Rewriting and Applications (RTA'07) (LNCS), pp.20-35, 2007.
DOI : 10.1007/978-3-540-73449-9_4

URL : https://hal.archives-ouvertes.fr/hal-00144178

M. Arapinis, T. Chothia, E. Ritter, and M. D. Ryan, Analysing Unlinkability and Anonymity Using the Applied Pi Calculus, 2010 23rd IEEE Computer Security Foundations Symposium, 2010.
DOI : 10.1109/CSF.2010.15

M. Arapinis, V. Cortier, S. Kremer, and M. D. Ryan, Practical Everlasting Privacy, Proc. 2nd Conference on Principles of Security and Trust (POST'13), pp.21-40, 2013.
DOI : 10.1007/978-3-642-36830-1_2

URL : https://hal.archives-ouvertes.fr/hal-00878630

A. Armando, D. A. Basin, Y. Boichut, Y. Chevalier, L. Compagna et al., The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, Proc. 17th International Conference on Computer Aided Verification (CAV'05) (Lecture Notes in Computer Science, 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, Proc. 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

F. Baader and T. Nipkow, Term rewriting and all that, 1998.

F. Baader and W. Snyder, Unification theory. In Handbook of Automated Reasoning, volume I, chapter 8, pp.445-532, 2001.

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, pp.195-209, 2008.
DOI : 10.1109/CSF.2008.26

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

M. Baudet, V. Cortier, and S. Delaune, YAPA, Proc. 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. Steven, M. Bellovin, and . Merritt, Encrypted Key Exchange: Password-Based Protocols Secure Against Dictionary Attacks, Symposium on Security and Privacy (S&P'92, pp.72-84, 1992.

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, Automatic proof of strong secrecy for security protocols, IEEE Symposium on Security and Privacy, 2004. Proceedings. 2004, pp.86-100, 2004.
DOI : 10.1109/SECPRI.2004.1301317

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

J. Borgström, Equivalences and Calculi for Formal Verifiation of Cryptographic Protocols, 2008.

J. Borgström, S. Briais, and U. Nestmann, Symbolic Bisimulation in the Spi Calculus, Proc. 15th Int. Conference on Concurrency Theory, pp.161-176, 2004.
DOI : 10.1007/3-540-58179-0_73

M. Bruso, K. Chatzikokolakis, and J. Hartog, Analysing Unlinkability and Anonymity Using the Applied Pi Calculus, Proc. 23rd Computer Security Foundations Symposium (CSF'10, pp.107-121, 2010.

R. Chadha, S. ¸. Ciobâcciob?ciobâc, ?. , and S. Kremer, Automated Verification of Equivalence Properties of Cryptographic Protocols, 21st European Symposium on Programming, ESOP 2012, pp.108-127, 2012.
DOI : 10.1007/978-3-642-28869-2_6

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

V. Cheval and B. Blanchet, Proving More Observational Equivalences with ProVerif, Principles of Security and Trust -Second International Conference, pp.226-246, 2013.
DOI : 10.1007/978-3-642-36830-1_12

URL : https://hal.archives-ouvertes.fr/hal-00863377

V. Cheval, H. Comon-lundh, and S. Delaune, Automating Security Analysis: Symbolic Equivalence of Constraint Systems, Proc. International Joint Conference on Automated Reasoning (IJCAR'10), pp.412-426, 2010.
DOI : 10.1007/978-3-642-14203-1_35

V. Cheval, H. Comon-lundh, and S. Delaune, Trace equivalence decision, Proceedings of the 18th ACM conference on Computer and communications security, CCS '11, pp.321-330, 2011.
DOI : 10.1145/2046707.2046744

S. ¸-tefan-ciobâcciob?ciobâc, ?. , S. Delaune, and S. Kremer, Computing knowledge in security protocols under convergent equational theories, Journal of Automated Reasoning, vol.48, issue.2, pp.219-262, 2011.

H. Comon-lundh and S. Delaune, The Finite Variant Property: How to Get Rid of Some Algebraic Properties, Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA'05), pp.294-307, 2005.
DOI : 10.1007/978-3-540-32033-3_22

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), pp.196-210, 2007.
DOI : 10.1007/978-3-540-75560-9_16

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

V. Cortier and S. Delaune, A Method for Proving Observational Equivalence, 2009 22nd IEEE Computer Security Foundations Symposium, pp.266-276, 2009.
DOI : 10.1109/CSF.2009.9

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

J. F. Cas and . Cremers, The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols, Proc. 20th International Conference on Computer Aided Verification (CAV'08), pp.414-418, 2008.

M. Dahl, S. Delaune, and G. Steel, Formal Analysis of Privacy for Vehicular Mix-Zones, Proc. 15th European Symposium on Research in Computer Security (ESORICS'10), pp.55-70, 2010.
DOI : 10.1007/978-3-642-15497-3_4

M. Dahl, S. Delaune, and G. Steel, Formal Analysis of Privacy for Anonymous Location Based Services, Proc. Workshop on Theory of Security and Applications (TOSCA'11, pp.98-112, 2011.
DOI : 10.1007/978-3-642-27375-9_6

S. Delaune, S. Kremer, and O. Pereira, Simulation based security in the applied pi calculus, Proceedings of the 29th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'09) (Leibniz International Proceedings in Informatics) Leibniz-Zentrum f ¨ ur Informatik, pp.169-180, 2009.

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. Delaune, S. Kremer, and M. D. Ryan, Symbolic bisimulation for the applied pi calculus*, Journal of Computer Security, vol.18, issue.2, pp.317-377, 2010.
DOI : 10.3233/JCS-2010-0363

S. Delaune, M. D. Ryan, and B. Smyth, Automatic Verification of Privacy Properties in the Applied pi Calculus, Proceedings of the 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security (IFIPTM'08) (IFIP Conference Proceedings), Yuecel Karabulut, pp.263-278, 2008.
DOI : 10.1007/978-0-387-09428-1_17

D. Dolev and A. Yao, On the Security of Public Key Protocols, Proc. of the 22nd Symp. on Foundations of Computer Science, pp.350-357, 1981.

L. Durante, R. Sisto, and A. Valenzano, Automatic testing equivalence verification of spi calculus specifications, ACM Transactions on Software Engineering and Methodology, vol.12, issue.2, pp.222-284, 2003.
DOI : 10.1145/941566.941570

S. Escobar, C. Meadows, and J. Meseguer, Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties, Foundations of Security Analysis and Design V, pp.1-50, 2009.
DOI : 10.1007/s10990-007-9000-6

S. Escobar, R. Sasse, and J. Meseguer, Folding variant narrowing and optimal variant termination, Journal of Logic and Algebraic Programming, vol.81, pp.7-8, 2012.

A. Fujioka, T. Okamoto, and K. Ohta, A practical secret voting scheme for large scale elections, Advances in Cryptology ? AUSCRYPT '92, pp.244-251, 1992.
DOI : 10.1007/3-540-57220-1_66

J. Goubault-larrecq, Deciding by resolution, Information Processing Letters, vol.95, issue.3, pp.401-408, 2005.
DOI : 10.1016/j.ipl.2005.04.007

A. Halderman and V. Teague, The New South Wales iVote System: Security Failures and Verification Flaws in a Live Online Election, 2015.
DOI : 10.1007/978-3-319-22270-7_3

H. Hans, Deciding framed bisimilarity, Proc. 4th International Workshop on Verification of Infinite-State Systems (INFINITY'02, pp.1-20, 2002.

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

J. Liu and H. Lin, A Complete Symbolic Bisimulation for Full Applied Pi Calculus, Proc. 36th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'10), pp.552-563, 2010.
DOI : 10.1007/978-3-642-11266-9_46

G. Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using FDR In Tools and Algorithms for the Construction and Analysis of Systems, TACAS'96) (LNCS), pp.147-166, 1996.

P. Narendran, F. Pfenning, and R. Statman, Abstract, The Journal of Symbolic Logic, vol.32, issue.02, pp.636-647, 1997.
DOI : 10.1007/BF01084396

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

S. Santiago, S. Escobar, C. Meadows, and J. Meseguer, A Formal Definition of Protocol Indistinguishability and Its Verification Using Maude-NPA, Proc. 10th International Workshop on Security and Trust Management (STM'14), pp.162-177, 2014.
DOI : 10.1007/978-3-319-11851-2_11

A. Tiu and J. Dawson, Automating Open Bisimulation Checking for the Spi Calculus, 2010 23rd IEEE Computer Security Foundations Symposium, pp.307-321, 2010.
DOI : 10.1109/CSF.2010.28

C. Weidenbach, Towards an Automatic Analysis of Security Protocols in First-Order Logic, Proc. 16th International Conference on Automated Deduction (CADE'99), pp.314-328, 1999.
DOI : 10.1007/3-540-48660-7_29

?. Dom-f, ?. E. , and ?. E. , Assume that x ? vars(f ) with f Since x ? dom(? ), we deduce that x ? vars(w(f )? ) and so x ? vars(w? ) by definition of ? . If x ? vars(w) then x ? dom(? ) also implies that x ? vars(w? ) Let us now consider x ? vars(w? ) We know that ? = ?? = ?? hence we deduce that either x ? vars(w?) and x ? dom(?) or there exists y ? vars(w?) such that x ? vars(y?) But w? ? = w??? = w??. Hence either x? = x? or there exists y ? vars(w?) such that x? ? st(y?) In the former, ? completing (w, ?) implies that x ? dom(?) and so x ? dom(? ) In the latter, ? completing (w, ?) also implies that y ? dom(?). Moreover, in combination of ? completing (w , ? ) and w?? = w? ? , we deduce that vars(img(?)) ? vars(img(?)) = ?. Hence x ? st(y?) and so x? = x which allows us to deduce that x ? dom(? ) Therefore, both cases, we have shown that x ? dom(? ) and that there exists y ? dom(?) such that x? ? st(y?). Similarly, we can show that there exists y ? dom(? ) such that x? ? st

?. Let-u and I. St, Thus there exists f ? F ? E such that u ? st(f ) By Lemma C.9, we know that vars(u) ? vars(w(f )). By construction of ? and ?, w?? = w? ? implies that for all x ? vars(w(f )), x?? = x? ? and so u?? = u? ? . We do a similar proof to show that for

T. and S. ?i-?-{1, f n ) such that ?, n}, |w(f i )| ? |w| ? ? = mgu((w| |w(f1)| , w(f 1 )); . . . ; (w| |w(fn)| , w(f n )); T )