M. Abadi, Security Protocols and their Properties, Foundations of Secure Computation for the 20th International Summer School on Foundations of Secure Computation, pp.39-60, 2000.

M. Abadi and C. Fournet, Mobile Values, New Names, and Secure Communication, 28th ACM SIGPLAN-SIGACT 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 P. Rogaway, Reconciling Two Views of Cryptography, International Conference on Theoretical Computer Science (IFIP TCS2000, pp.3-22, 2000.
DOI : 10.1007/3-540-44929-9_1

B. Adida, Helios: Web-based Open-Audit Voting, 17th USENIX Security symposium (SS'08). USENIX Association, pp.335-348, 2008.

T. Antonopoulos, P. Gazzillo, M. Hicks, E. Koskinen, T. Terauchi et al., Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels, 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pp.362-375, 2017.

M. Arapinis, T. Chothia, E. Ritter, and M. Ryan, Untraceability in the applied pi-calculus, 2009 International Conference for Internet Technology and Secured Transactions, (ICITST), pp.1-6, 2009.
DOI : 10.1109/ICITST.2009.5402514

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://www.cs.bham.ac.uk/%7Etpc/Papers/csf10.pdf

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

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, 17th International Conference on Computer Aided Verification, pp.281-285, 2005.
DOI : 10.1007/11513988_27
URL : https://hal.archives-ouvertes.fr/inria-00000408

M. Backes, C. Hri?cu, 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. Backes, C. Hri?cu, and M. Maffei, Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations, Journal of Computer Security, vol.22, issue.2, pp.301-353, 2014.
DOI : 10.3233/JCS-130493
URL : https://hal.archives-ouvertes.fr/hal-01102192

D. Baelde, S. Delaune, and L. Hirschi, Partial Order Reduction for Security Protocols, 26th International Conference on Concurrency Theory (CONCUR'15) (LIPIcs) Leibniz-Zentrum für Informatik, pp.497-510, 2015.

G. Barthe, C. Fournet, B. Grégoire, P. Strub, N. Swamy et al., Probabilistic relational verification for cryptographic implementations, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pp.193-206, 2014.
DOI : 10.1145/2535838.2535847
URL : https://hal.archives-ouvertes.fr/hal-00935743

G. Barthe, B. Grégoire, and S. Zanella-béguelin, Formal certification of code-based cryptographic proofs, 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.90-101, 2009.
DOI : 10.1145/1480881.1480894

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

J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis, Refinement types for secure implementations, ACM Transactions on Programming Languages and Systems, vol.33, issue.2, pp.1-845, 2011.
DOI : 10.1145/1890028.1890031
URL : https://hal.archives-ouvertes.fr/hal-01294973

N. Benton, Simple Relational Correctness Proofs for Static Analyses and Program Transformations, 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.14-25, 2004.
DOI : 10.1145/982962.964003
URL : http://research.microsoft.com/~nick/correctnesspopl2004.pdf

B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., 2001.
DOI : 10.1109/CSFW.2001.930138
URL : http://www.mpi-sb.mpg.de/~blanchet/publications/./BlanchetCSFW01.ps.gz

B. Blanchet, Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends in Privacy and Security 1, pp.1-2, 2016.
DOI : 10.1561/3300000004
URL : https://hal.archives-ouvertes.fr/hal-01423760

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

M. Boreale, R. De-nicola, and R. Pugliese, Proof Techniques for Cryptographic Processes, SIAM Journal on Computing, vol.31, issue.3, pp.947-986, 2002.
DOI : 10.1137/S0097539700377864
URL : ftp://rap.dsi.unifi.it/pub/papers/BDP-spi.ps.gz

M. Bugliesi, S. Calzavara, F. Eigner, and M. Maffei, Resource-Aware Authorization Policies for Statically Typed Cryptographic Protocols, 2011 IEEE 24th Computer Security Foundations Symposium, pp.83-98, 2011.
DOI : 10.1109/CSF.2011.13

M. Bugliesi, S. Calzavara, F. Eigner, and M. Maffei, Logical Foundations of Secure Resource Management in Protocol Implementations, 2nd International Conference on Principles of Security and Trust, pp.105-125, 2013.
DOI : 10.1007/978-3-642-36830-1_6

M. Bugliesi, S. Calzavara, F. Eigner, and M. Maffei, Affine Refinement Types for Secure Distributed Programming, ACM Transactions on Programming Languages and Systems, vol.37, issue.4, pp.11-66, 2015.
DOI : 10.1007/978-3-642-11957-6_29

M. Bugliesi, R. Focardi, and M. Maffei, Authenticity by tagging and typing, Proceedings of the 2004 ACM workshop on Formal methods in security engineering , FMSE '04, pp.1-12, 2004.
DOI : 10.1145/1029133.1029135

M. Bugliesi, R. Focardi, and M. Maffei, Analysis of Typed Analyses of Authentication Protocols, 18th IEEE Computer Security Foundations Workshop (CSFW'05), pp.112-125, 2005.
DOI : 10.1109/CSFW.2005.8

M. Bugliesi, R. Focardi, and M. Maffei, Dynamic types for authentication*, Journal of Computer Security, vol.15, issue.6, pp.563-617, 2007.
DOI : 10.3233/JCS-2007-15602

?. Ciobâc?, D. Lucanu, V. Rusu, and G. Rosu, A languageindependent proof system for full program equivalence. Formal Asp, Comput, vol.28, pp.3-469, 2016.

R. Chadha, S. Ciobâc?, and S. Kremer, Automated Verification of Equivalence Properties of Cryptographic Protocols, Programming Languages and Systems ?21th European Symposium on Programming (ESOP'12), pp.108-127, 2012.
DOI : 10.1007/978-3-642-28869-2_6
URL : https://hal.archives-ouvertes.fr/hal-01306561

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
URL : http://www.loria.fr/%7Echevalvi/files/Cheval-tacas14.pdf

V. Cheval, V. Cortier, and A. Plet, Lengths May Break Privacy ??? Or How to Check for Equivalences with Length, 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

J. Clark and J. Jacob, A Survey of Authentication Protocol Literature: Version 1.0, 1997.

H. Comon-lundh and V. Cortier, Computational soundness of observational equivalence, Proceedings of the 15th ACM conference on Computer and communications security, CCS '08, pp.109-118, 2008.
DOI : 10.1145/1455770.1455786
URL : https://hal.archives-ouvertes.fr/inria-00323199

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

V. Cortier, F. Eigner, S. Kremer, M. Maffei, and C. Wiedling, Type-Based Verification of Electronic Voting Protocols, 4th International Conference on Principles of Security and Trust, pp.303-323, 2015.
DOI : 10.1007/978-3-662-46666-7_16
URL : https://hal.archives-ouvertes.fr/hal-01103545

V. Cortier, A. Filipiak, S. Gharout, and J. Traore, Designing and Proving an EMV-Compliant Payment Protocol for Mobile Devices, 2017 IEEE European Symposium on Security and Privacy (EuroS&P), pp.467-480, 2017.
DOI : 10.1109/EuroSP.2017.19
URL : https://hal.archives-ouvertes.fr/hal-01408584

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, N. Grimm, J. Lallemand, and M. Maffei, ). https://secpriv.tuwien.ac.at/tools/typeeq [40] Véronique Cortier Relating Two Standard Notions of Secrecy, Michaël Rusinowitch, and Eugen Z?linescu, pp.303-318, 2006.

V. Cortier and B. Smyth, Attacking and Fixing Helios: An Analysis of Ballot Secrecy, 24th IEEE Computer Security Foundations Symposium (CSF'11, pp.297-311, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00732899

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

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

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

F. Eigner and M. Maffei, Differential Privacy by Typing in Security Protocols, 2013 IEEE 26th Computer Security Foundations Symposium, pp.272-286, 2013.
DOI : 10.1109/CSF.2013.25

R. Focardi and M. Maffei, Types for Security Protocols, Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security Series, pp.143-181, 2011.
DOI : 10.4204/EPTCS.7.0.1
URL : http://www.lbs.cs.uni-saarland.de/resources/ios2010.pdf

D. Andrew, A. Gordon, and . Jeffrey, Authenticity by Typing for Security Protocols, Journal of Computer Security, vol.11, issue.4, pp.451-519, 2003.

N. Grimm, K. Maillard, C. Fournet, C. Hri?cu, M. Maffei et al., Nikhil Swamy, and Santiago Zanella-Béguelin. 2017. A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations, 2017.

G. Lowe, Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR, Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96), pp.147-166, 1996.
DOI : 10.1007/3-540-61042-1_43
URL : http://www.cs.ubc.ca/~ajh/courses/cpsc513/NSFDR.ps

D. Lucanu and V. Rusu, Program equivalence by circular reasoning. Formal Asp, Comput, vol.27, issue.4, pp.701-726, 2015.
DOI : 10.1007/978-3-642-38613-8_25
URL : https://hal.archives-ouvertes.fr/hal-00820871

M. Maffei, K. Pecina, and M. Reinert, Security and Privacy by Declarative Design, 2013 IEEE 26th Computer Security Foundations Symposium, pp.81-96, 2013.
DOI : 10.1109/CSF.2013.13

S. Meier and B. Schmidt, The TAMARIN Prover for the Symbolic Analysis of Security Protocols, Computer Aided Verification, 25th International Conference, CAV 2013, pp.696-701
DOI : 10.1007/978-3-642-39799-8_48

P. Roenne, Private communication, 2016.

S. Santiago, S. Escobar, C. A. Meadows, and J. Meseguer, A Formal Definition of Protocol Indistinguishability and Its Verification Using Maude-NPA, STM 2014, pp.162-177, 2014.
DOI : 10.1007/978-3-319-11851-2_11

B. Schmidt, S. Meier, C. J. Cremers, and D. A. Basin, Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties, 2012 IEEE 25th Computer Security Foundations Symposium, pp.78-94, 2012.
DOI : 10.1109/CSF.2012.25

M. Sousa and I. Dillig, Cartesian Hoare Logic for Verifying k-Safety Properties, 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, pp.57-69, 2016.
DOI : 10.1145/2980983.2908092

H. Yang, Relational separation logic, Theoretical Computer Science, vol.375, issue.1-3, pp.1-3, 2007.
DOI : 10.1016/j.tcs.2006.12.036
URL : https://doi.org/10.1016/j.tcs.2006.12.036