V. Cortier, S. Kremer, and B. Warinschi, A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems, Journal of Automated Reasoning, vol.13, issue.1, pp.225-259, 2010.
DOI : 10.3233/JCS-2005-13307
URL : https://hal.archives-ouvertes.fr/inria-00525776

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

A. Armando, R. Carbone, L. Compagna, J. Cuéllar, and M. L. Tobarra, Formal analysis of SAML 2.0 web browser single sign-on, Proceedings of the 6th ACM workshop on Formal methods in security engineering, FMSE '08, pp.1-10, 2008.
DOI : 10.1145/1456396.1456397

P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and B. Roscoe, The Modelling and Analysis of Security Protocols, 2000.

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.5150

C. 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.
DOI : 10.1007/978-3-540-70545-1_38

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

B. Blanchet, M. Abadi, and C. Fournet, Automated verification of selected equivalences for security protocols, The Journal of Logic and Algebraic Programming, vol.75, issue.1, pp.3-51, 2008.
DOI : 10.1016/j.jlap.2007.06.002

S. Meier, B. Schmidt, C. Cremers, and D. Basin, The TAMARIN Prover for the Symbolic Analysis of Security Protocols, Proc. International Conference on Computer Aided Verification (CAV'13), pp.696-701, 2013.
DOI : 10.1007/978-3-642-39799-8_48

D. Basin, J. Dreier, and R. Sasse, Automated Symbolic Proofs of Observational Equivalence, Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, CCS '15, pp.1144-1155, 2015.
DOI : 10.1007/978-3-540-79966-5_1
URL : https://hal.archives-ouvertes.fr/hal-01337409

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

V. Cheval, V. Cortier, and S. Delaune, Deciding equivalence-based properties using constraint solving, Theoretical Computer Science, vol.492, pp.1-39, 2013.
DOI : 10.1016/j.tcs.2013.04.016
URL : https://hal.archives-ouvertes.fr/hal-00881060

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

Y. Chevalier and M. Rusinowitch, Decidability of Equivalence of Symbolic Derivations, Journal of Automated Reasoning, vol.17, issue.3
DOI : 10.1145/219282.219298
URL : https://hal.archives-ouvertes.fr/inria-00527630

A. Tiu and J. E. 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

R. Chadha, S. ¸. Ciobâc?-a, and S. Kremer, Automated verification of equivalence properties of cryptographic protocols, Proc. 21th European Symposium on Programming (ESOP'12), pp.2012-108
URL : https://hal.archives-ouvertes.fr/hal-00732905

M. Arapinis, T. Chothia, E. Ritter, and M. Ryan, Analysing Unlinkability and Anonymity Using the Applied Pi Calculus, 2010 23rd IEEE Computer Security Foundations Symposium, pp.107-121, 2010.
DOI : 10.1109/CSF.2010.15
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.172.5739

V. Cheval and B. Blanchet, Proving More Observational Equivalences with ProVerif, Proc. 2nd International Conference on Principles of Security and Trust (POST'13), pp.226-246, 2013.
DOI : 10.1007/978-3-642-36830-1_12
URL : https://hal.archives-ouvertes.fr/hal-00863377

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.1266

V. Cheval, V. Cortier, and A. Plet, Lengths May Break Privacy ??? Or How to Check for Equivalences with Length, Proc. 25th International Conference on Computer Aided Verification (CAV'13), pp.708-723, 2013.
DOI : 10.1007/978-3-642-39799-8_50
URL : https://hal.archives-ouvertes.fr/hal-00881065

G. Bana and H. , Comon-Lundh, A computationally complete symbolic attacker for equivalence properties, Proc. ACM Conference on Computers and Communications Security, 2014.
DOI : 10.1145/2660267.2660276

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

H. Comon-lundh, V. Cortier, and E. Zalinescu, Deciding security properties for cryptographic protocols. application to key cycles, ACM Transactions on Computational Logic, vol.11, issue.2
DOI : 10.1145/1656242.1656244
URL : https://hal.archives-ouvertes.fr/inria-00525775

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
URL : http://kar.kent.ac.uk/46878/1/CCD-ccs11.pdf

V. Cheval, Automatic verification of cryptographic protocols: privacy-type properties, Thèse de doctorat, 2012.
URL : https://hal.archives-ouvertes.fr/tel-00861389

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

N. Dershowitz and J. Jouannaud, Rewrite Systems, Handbook of Theoretical Computer Science, vol.B, issue.6, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

H. Comon and P. Lescanne, Equational problems anddisunification, Journal of Symbolic Computation, vol.7, issue.3-4, pp.371-425, 1989.
DOI : 10.1016/S0747-7171(89)80017-3
URL : http://doi.org/10.1016/s0747-7171(89)80017-3

V. Cheval, H. Comon-lundh, and S. Delaune, Automating Security Analysis: Symbolic Equivalence of Constraint Systems, Proc. 5th International Joint Conference on Automated Reasoning (IJ- CAR'10), pp.412-426, 2010.
DOI : 10.1007/978-3-642-14203-1_35
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.388.3094

V. Cheval, APTE: An Algorithm for Proving Trace Equivalence, Proc. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), 2014.
DOI : 10.1007/978-3-642-54862-8_50
URL : http://kar.kent.ac.uk/46724/1/Cheval-tacas14.pdf

D. Basin, S. Mödersheim, and L. Viganò, Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols, Proc. 10th ACM Conference on Computer and Communications Security (CCS'03), pp.335-344, 2003.

D. Baelde, S. Delaune, and L. Hirschi, A Reduced Semantics for Deciding Trace Equivalence Using Constraint Systems, Proc. 3rd Conference on Principles of Security and Trust POST'14, 2014.
DOI : 10.1007/978-3-642-54792-8_1
URL : http://arxiv.org/abs/1401.2854