. Deepsec, Deciding equivalence properties in security protocols. https: //deepsec-prover.github.io, 2018.

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, 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

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://cs.ucsb.edu/~ravenben/papers/prelims/logicofauth.pdf

M. Abadi and A. D. Gordon, A Calculus for Cryptographic Protocols: The Spi Calculus, Information and Computation, vol.148, issue.1, pp.1-70, 1999.
DOI : 10.1006/inco.1998.2740

B. Adida, Helios: web-based open-audit voting, 17th conference on Security symposium (SS'08), pp.335-348, 2008.

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, pp.107-121, 2010.
DOI : 10.1109/CSF.2010.15

M. Arapinis, V. Cortier, and S. Kremer, When Are Three Voters Enough for Privacy Properties?, Proceedings of the 21st European Symposium on Research in Computer Security (ESORICS'16), pp.241-260, 2016.
DOI : 10.1007/978-3-642-36830-1_12
URL : https://hal.archives-ouvertes.fr/hal-01351398

M. Arapinis, L. Mancini, E. Ritter, M. Ryan, N. Golde et al., New privacy issues in mobile telephony, Proceedings of the 2012 ACM conference on Computer and communications security, CCS '12, pp.205-216, 2012.
DOI : 10.1145/2382196.2382221

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, 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

D. Baelde, S. Delaune, and L. Hirschi, Partial order reduction for security protocols, 26th International Conference on Concurrency Theory (CONCUR'15), volume 42 of Leibniz International Proceedings in Informatics Leibniz-Zentrum für Informatik, pp.497-510, 2015.

D. A. 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

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

B. Blanchet, M. Abadi, and C. Fournet, Automated Verification of Selected Equivalences for Security Protocols, Symposium on Logic in Computer Science (LICS'05), pp.331-340, 2005.

B. Blanchet and B. Smyth, Automated reasoning for equivalences in the applied pi calculus with barriers, 29th Computer Security Foundations Symposium (CSF'16), pp.310-324, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01423742

B. Blanchet, B. Smyth, and V. Cheval, Automatic Cryptographic Protocol Verifier, User Manual and Tutorial, 2016. [18] M. Boreale and L. Trevisan. A complexity analysis of bisimilarity for value-passing processes, Theor. Comput. Sci, vol.238, issue.12, pp.313-345, 2000.

R. Chadha, V. Cheval, S. ¸. Ciobâc?, and S. Kremer, Automated verification of equivalence properties of cryptographic protocol, ACM Transactions on Computational Logic, vol.23, issue.4, pp.1-32, 2016.

V. Cheval, APTE: An Algorithm for Proving Trace Equivalence, 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), pp.587-592, 2014.
DOI : 10.1007/978-3-642-54862-8_50

V. Cheval and B. Blanchet, Proving More Observational Equivalences with ProVerif, Proc. 2nd 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

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, 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

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

R. Chrétien, V. Cortier, and S. Delaune, Decidability of Trace Equivalence for Protocols with Nonces, 2015 IEEE 28th Computer Security Foundations Symposium, pp.170-184, 2015.
DOI : 10.1109/CSF.2015.19

R. Chrétien, V. Cortier, and S. Delaune, From Security Protocols to Pushdown Automata, ACM Transactions on Computational Logic, vol.17, issue.1, pp.1-45, 2015.
DOI : 10.1109/CSF.2010.28

S. ¸. Ciobâc?-a, S. Delaune, and S. Kremer, Computing Knowledge in Security Protocols Under Convergent Equational Theories, Journal of Automated Reasoning, vol.299, issue.4, pp.219-262, 2012.
DOI : 10.1016/S0304-3975(02)00490-5

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

B. Conchinha, D. A. Basin, and C. Caleiro, Efficient Decision Procedures for Message Deducibility and Static Equivalence, Proc. 7th International Workshop on Formal Aspects of Security and Trust (FAST'10), pp.34-49, 2010.
DOI : 10.3233/JCS-2005-13306
URL : http://sqig.math.ist.utl.pt/pub/CaleiroC/10-CBC-efficient.pdf

V. Cortier, S. Delaune, and A. Dallon, SAT-Equiv: An Efficient Tool for Equivalence Properties, 2017 IEEE 30th Computer Security Foundations Symposium (CSF), pp.481-494, 2017.
DOI : 10.1109/CSF.2017.15
URL : https://hal.archives-ouvertes.fr/hal-01624274

V. Cortier, N. Grimm, J. Lallemand, and M. Maffei, A Type System for Privacy Properties, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security , CCS '17, 2017.
DOI : 10.1145/2908080.2908092
URL : https://hal.archives-ouvertes.fr/hal-01626109

V. Cortier and B. Smyth, Attacking and fixing Helios: An analysis of ballot secrecy, Journal of Computer Security, vol.21, issue.1, pp.89-148, 2013.
DOI : 10.3233/JCS-2012-0458
URL : https://hal.archives-ouvertes.fr/hal-00732899

C. J. Cremers, The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols, Proc. 20th International Conference on Computer Aided Verification, pp.414-418, 2008.
DOI : 10.1007/978-3-540-70545-1_38

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

D. Dolev and A. Yao, On the security of public key protocols, Proc. of the 22nd Symp. on Foundations of Computer Science (FOCS'81), pp.350-357, 1981.

N. A. Durgin, P. Lincoln, and J. C. Mitchell, Multiset rewriting and the complexity of bounded security protocols, Journal of Computer Security, vol.12, issue.2, pp.247-311, 2004.
DOI : 10.3233/JCS-2004-12203

P. T. Force, PKI for machine readable travel documents offering ICC read-only access International Civil Aviation Organization, 2004.

L. Hirschi, D. Baelde, and S. Delaune, A Method for Verifying Privacy-Type Properties: The Unbounded Case, 2016 IEEE Symposium on Security and Privacy (SP), pp.564-581
DOI : 10.1109/SP.2016.40

R. Milner, J. Parrow, and D. Walker, A calculus of mobile processes, I, Information and Computation, vol.100, issue.1, pp.1-40, 1992.
DOI : 10.1016/0890-5401(92)90008-4

C. Papadimitriou, Computational complexity, 2003.

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. Y. Ryan and S. A. Schneider, Pr??t ?? Voter with Re-encryption Mixes, 11th European Symp. On Research In Computer Security (ESORICS'06), pp.313-326, 2006.
DOI : 10.1007/11863908_20
URL : http://www.cs.ncl.ac.uk/research/pubs/trs/papers/956.pdf

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

B. Schmidt, S. Meier, C. Cremers, and D. Basin, The TAMARIN prover for the symbolic analysis of security protocols, 25th International Conference on Computer Aided Verification (CAV'13), pp.696-701, 2013.

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

A. Tiu, N. Nguyen, and R. Horne, SPEC: An Equivalence Checker for Security Protocols, 14th Asian Symposium on Programming Languages and Systems (APLAS'16), pp.87-95, 2016.
DOI : 10.1109/CSF.2010.28