M. Abadi, Protection in programming-language translations, Proceedings of the 25th International Colloquium on Automata, Languages and Programming Also Digital Equipment Corporation Systems Research Center report No. 154, pp.868-883, 1998.
DOI : 10.1007/BFb0055109

M. Abadi, Secrecy by typing in security protocols, Journal of the ACM, vol.46, issue.5, pp.749-786, 1999.
DOI : 10.1145/324133.324266

M. Abadi, Security Protocols: Principles and Calculi, Foundations of Security Analysis and Design IV, pp.1-23, 2006.
DOI : 10.1007/978-3-540-74810-6_1

M. Abadi and B. Blanchet, Analyzing security protocols with secrecy types and logic programs, Journal of the ACM, vol.52, issue.1, pp.102-146, 2005.
DOI : 10.1145/1044731.1044735
URL : http://www.di.ens.fr/~blanchet/publications/AbadiBlanchetJACM7037.ps.gz

M. Abadi and B. Blanchet, Computer-Assisted Verification of a Protocol for Certified Email, Science of Computer Programming, vol.58, pp.1-2, 2005.

M. Abadi, B. Blanchet, and H. Comon-lundh, Models and Proofs of Protocol Security: A Progress Report, Computer Aided Verification, 21st International Conference, pp.35-49, 2009.
DOI : 10.1007/978-3-540-24727-2_33

M. Abadi, B. Blanchet, and C. Fournet, Just Fast Keying in the Pi Calculus, ACM Transactions on Information and System Security, vol.10, issue.2, pp.1-59, 2007.

M. Abadi and V. Cortier, Deciding knowledge in security protocols under equational theories, Theoretical Computer Science, vol.367, issue.1-2, pp.2-32, 2006.
DOI : 10.1016/j.tcs.2006.08.032
URL : https://hal.archives-ouvertes.fr/inria-00108372

M. Abadi, C. Fournet, and G. Gonthier, Secure implementation of channel abstractions, Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, pp.105-116, 1998.

M. Abadi, C. Fournet, and G. Gonthier, Authentication primitives and their compilation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, pp.302-315, 2000.
DOI : 10.1145/325694.325734
URL : http://pa.bell-labs.com/~abadi/Papers/auth-popl-preprint-corrected.ps

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, 1998.
DOI : 10.1145/266420.266432

M. Abadi and P. Rogaway, Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)*, Journal of Cryptology, vol.15, issue.2, pp.103-127, 2002.
DOI : 10.1007/s00145-001-0014-7

D. Adrian, K. Bhargavan, Z. Durumeric, P. Gaudry, M. Green et al., Imperfect Forward Secrecy, Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, CCS '15, pp.5-17, 2015.
DOI : 10.1007/3-540-68339-9_29
URL : https://hal.archives-ouvertes.fr/hal-01184171

W. Aiello, S. M. Bellovin, M. Blaze, R. Canetti, J. Ionnidis et al., Just fast keying, ACM Transactions on Information and System Security, vol.7, issue.2, pp.1-30, 2004.
DOI : 10.1145/996943.996946

X. Allamigeon and B. Blanchet, Reconstruction of attacks against cryptographic protocols, 18th IEEE Computer Security Foundations Workshop (CSFW'05), pp.140-154, 2005.
DOI : 10.1109/CSFW.2005.25
URL : http://www.di.ens.fr/~blanchet/publications/AllamigeonBlanchetCSFW05.ps.gz

M. Roberto, D. Amadio, and . Lugiez, On the Reachability Problem in Cryptographic Protocols, CONCUR 2000: Concurrency Theory (11th International Conference) (Lecture Notes in Computer Science), pp.380-394, 2000.

M. Arapinis, J. Liu, E. Ritter, and M. Ryan, Stateful Applied Pi Calculus, Principles of Security and Trust?Third International Conference, pp.22-41, 2014.
DOI : 10.1007/978-3-642-54792-8_2

M. Arapinis, E. Ritter, and M. Ryan, StatVerif: Verification of Stateful Processes, 24th IEEE Computer Security Foundations Symposium. IEEE Computer Society, pp.33-47, 2011.

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

N. Aviram, S. Schinzel, J. Somorovsky, N. Heninger, M. Dankel et al., DROWN: Breaking TLS Using SSLv2, USENIX Security Symposium. USENIX, pp.689-706, 2016.

M. Backes, D. Hofheinz, and D. Unruh, CoSP, Proceedings of the 16th ACM conference on Computer and communications security, CCS '09, pp.66-78, 2009.
DOI : 10.1145/1653662.1653672

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), pp.202-215, 2008.
DOI : 10.1109/SP.2008.23

M. Baldamus, J. Parrow, and B. Victor, Spi calculus translated to /spl pi/-calculus preserving may-tests, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., pp.22-31, 2004.
DOI : 10.1109/LICS.2004.1319597

C. Bansal, K. Bhargavan, and S. Maffeis, Discovering Concrete Attacks on Website Authorization by Formal Analysis, 2012 IEEE 25th Computer Security Foundations Symposium, pp.247-262, 2012.
DOI : 10.1109/CSF.2012.27
URL : https://hal.archives-ouvertes.fr/hal-00863385

G. Barthe, B. Grégoire, and S. Z. Béguelin, Programming Language Techniques for Cryptographic Proofs, Interactive Theorem Proving, First International Conference (Lecture Notes in Computer Science), pp.115-130, 2010.
DOI : 10.1007/978-3-642-14052-5_10
URL : https://hal.archives-ouvertes.fr/inria-00552894

D. Basin, J. Dreier, and R. Casse, 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

M. Baudet, Sécurité des protocoles cryptographiques: aspects logiques et calculatoires, 2007.

M. Baudet, V. Cortier, and S. Delaune, YAPA, Rewriting Techniques and Applications (RTA'09), pp.148-163978, 2009.
DOI : 10.1145/2422085.2422089
URL : https://hal.archives-ouvertes.fr/hal-00732901

M. Baudet, V. Cortier, and S. Kremer, Computationally sound implementations of equational theories against passive adversaries, Information and Computation, vol.207, issue.4, pp.496-520, 2009.
DOI : 10.1016/j.ic.2008.12.005
URL : https://hal.archives-ouvertes.fr/inria-00000555

M. Bellare and P. Rogaway, Entity Authentication and Key Distribution, Advances in Cryptology?CRYPTO '94, pp.232-249, 1993.
DOI : 10.1007/3-540-48329-2_21

J. Bengtson, M. Johansson, J. Parrow, and B. Victor, Psi-calculi: a framework for mobile processes with nominal data and logic, Logical Methods in Computer Science, vol.304, issue.3, 2011.
DOI : 10.1007/s10817-008-9097-2
URL : https://lmcs.episciences.org/696/pdf

G. Berry and G. Boudol, The chemical abstract machine, Theoretical Computer Science, vol.96, issue.1, pp.217-248, 1992.
DOI : 10.1016/0304-3975(92)90185-I
URL : https://hal.archives-ouvertes.fr/inria-00075426

K. Bhargavan, B. Blanchet, and N. Kobeissi, Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate, 2017 IEEE Symposium on Security and Privacy (SP), pp.483-503, 2017.
DOI : 10.1109/SP.2017.26
URL : https://hal.archives-ouvertes.fr/hal-01575920

K. Bhargavan, R. Corin, C. Fournet, and E. Z?linescu, Cryptographically verified implementations for TLS, Proceedings of the 15th ACM conference on Computer and communications security, CCS '08, pp.459-468, 2008.
DOI : 10.1145/1455770.1455828

K. Bhargavan, A. Delignat-lavaud, C. Fournet, M. Kohlweiss, J. Pan et al., Implementing and Proving the TLS 1.3 Record Layer, IEEE Symposium on Security and Privacy (S&P'17, pp.463-482, 2017.

K. Bhargavan, A. Delignat-lavaud, C. Fournet, A. Pironti, and P. Strub, Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS, 2014 IEEE Symposium on Security and Privacy, pp.98-113, 2014.
DOI : 10.1109/SP.2014.14
URL : https://hal.archives-ouvertes.fr/hal-01102259

K. Bhargavan, C. Fournet, R. Corin, and E. Z?linescu, Verified Cryptographic Implementations for TLS, ACM Transactions on Information and System Security, vol.15, issue.1, 2012.
DOI : 10.1145/2133375.2133378
URL : https://hal.archives-ouvertes.fr/hal-00863381

K. Bhargavan, C. Fournet, A. D. Gordon, and R. Pucella, TulaFale: A Security Tool for Web Services In Formal Methods for Components and Objects (FMCO 2003) (Lecture Notes in Computer Science), Frank S, pp.197-222, 2003.

K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse, Verified Interoperable Implementations of Security Protocols, ACM Transactions on Programming Languages and Systems, vol.31, issue.1 5, p.61, 2008.

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, P. Strub et al., Proving the TLS Handshake Secure (As It Is), Advances in Cryptology ? CRYPTO 2014, pp.235-255, 2014.
DOI : 10.1007/978-3-662-44381-1_14
URL : https://hal.archives-ouvertes.fr/hal-01102229

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P. Strub, Implementing TLS with Verified Cryptographic Security, 2013 IEEE Symposium on Security and Privacy, pp.445-459, 2013.
DOI : 10.1109/SP.2013.37
URL : https://hal.archives-ouvertes.fr/hal-00863373

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, A Computationally Sound Mechanized Prover for Security Protocols, IEEE Symposium on Security and Privacy, pp.140-154, 2006.

B. Blanchet, Automatic verification of correspondences for security protocols*, Journal of Computer Security, vol.17, issue.4, pp.363-434, 2009.
DOI : 10.3233/JCS-2009-0339

B. Blanchet, Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif, Foundations and Trends?? in Privacy and Security, vol.1, issue.1-2, 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

B. Blanchet and B. Aziz, A Calculus for Secure Mobility, 8th Asian Computing Science Conference (ASIAN'03) (Lecture Notes in Computer Science), pp.188-204, 2003.
DOI : 10.1007/978-3-540-40965-6_13

B. Blanchet and D. Pointcheval, Automated Security Proofs with Sequences of Games, CRYPTO'06, pp.537-554, 2006.
DOI : 10.1007/11818175_32

C. Bodei, P. Degano, F. Nielson, and H. Nielson, Control Flow Analysis for the Pi-Calculus, CONCUR '98: Concurrency Theory (9th International Conference) (Lecture Notes in Computer Science), pp.84-98, 1998.

M. Boreale, R. D. Nicola, and R. Pugliese, Proof Techniques for Cryptographic Processes, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, pp.157-166, 1999.
DOI : 10.1109/lics.1999.782608

J. Borgström, R. Gutkovas, J. Parrow, B. Victor, and J. Å. Pohjola, A Sorted Semantic Framework for Applied Process Calculi (Extended Abstract), Trustworthy Global Computing, TGC 2013, pp.103-118, 2014.
DOI : 10.1007/978-3-319-05119-2_7

J. Borgström, R. Gutkovas, J. Parrow, B. Victor, and J. Å. Pohjola, A Sorted Semantic Framework for Applied Process Calculi, Logical Methods in Computer Science, vol.12, issue.1, 2016.
DOI : 10.2168/LMCS-12(1:8)2016

S. Briais, Theory and Tool Support for the Formal Verification of Cryptographic Protocols, 2008.

M. G. Buscemi and U. Montanari, CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements, Programming Languages and Systems, 16th European Symposium on Programming, pp.18-32, 2007.
DOI : 10.1007/978-3-540-71316-6_3

M. Carbone and S. Maffeis, On the Expressive Power of Polyadic Synchronisation in pi-calculus, Nordic Journal of Computing, vol.10, issue.2, pp.70-98, 2003.

L. Cardelli, Mobility and Security, Foundations of Secure Computation (NATO Science Series), pp.3-37, 2000.

L. Cardelli and A. D. Gordon, Mobile ambients, Theoretical Computer Science, vol.240, issue.1, pp.177-213, 2000.
DOI : 10.1016/S0304-3975(99)00231-5
URL : https://doi.org/10.1016/s0304-3975(99)00231-5

R. Chadha, S. Ciobaca, and S. Kremer, Automated Verification of Equivalence Properties of Cryptographic Protocols, Programming Languages and Systems -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/hal-00732905

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

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, 45 pages, 2015.

?. Ciobâc?, 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 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-00274158

S. Conchon and F. L. Fessant, Jocaml: mobile agents for Objective-Caml, Proceedings. First and Third International Symposium on Agent Systems Applications, and Mobile Agents, pp.22-29, 1999.
DOI : 10.1109/ASAMA.1999.805390
URL : http://para.inria.fr/~lefessan/biblio/papers/00064-CLF99.ps.gz

S. S. Core, SSH insertion attack. Bugtraq mailing list Available at http://seclists.org/bugtraq, 1965.

Y. Jean-sébastien-coron, C. Dodis, P. Malinaud, and . Puniya, Merkle-Damg??rd Revisited: How to Construct a Hash Function, Advances in Cryptology?CRYPTO 2005, pp.430-448, 2005.
DOI : 10.1007/11535218_26

V. Cortier and S. Kremer, Formal Models and Techniques for Analyzing Security Protocols: A Tutorial, Foundations and Trends?? in Programming Languages, vol.1, issue.3, pp.151-267, 2014.
DOI : 10.1561/2500000001
URL : https://hal.archives-ouvertes.fr/hal-01090874

C. Cremers, M. Horvat, S. Scott, and T. Van-der-merwe, Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication, 2016 IEEE Symposium on Security and Privacy (SP), pp.470-485, 2016.
DOI : 10.1109/SP.2016.35

J. F. Cas and . Cremers, Unbounded verification, falsification, and characterization of security protocols by pattern refinement, 15th ACM conference on Computer and Communications Security (CCS'08, pp.119-128, 2008.

L. Cruz-filipe, I. Lanese, and F. Martins, The stream-based service-centred calculus: a foundation for service-oriented programming, Formal Aspects of Computing, vol.368, issue.1???2, pp.865-918, 2014.
DOI : 10.1016/j.tcs.2006.06.028

M. Curti, P. Degano, C. Priami, and C. T. Baldari, Modelling biochemical pathways through enhanced ??-calculus, Theoretical Computer Science, vol.325, issue.1, pp.111-140, 2004.
DOI : 10.1016/j.tcs.2004.03.066
URL : https://doi.org/10.1016/j.tcs.2004.03.066

M. Dam, Proving trust in systems of second-order processes, Proceedings of the Thirty-First Hawaii International Conference on System Sciences, pp.255-264, 1998.
DOI : 10.1109/HICSS.1998.649220

A. Datta, A. Derek, J. C. Mitchell, and D. Pavlovic, A derivation system and compositional logic for security protocols, Journal of Computer Security, vol.13, issue.3, pp.423-482, 2005.
DOI : 10.3233/JCS-2005-13304

S. Delaune, S. Kremer, and M. D. Ryan, Symbolic bisimulation for the applied pi calculus, 2007.

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

R. A. Demillo, N. A. Lynch, and M. Merritt, Cryptographic protocols, Proceedings of the fourteenth annual ACM symposium on Theory of computing , STOC '82, pp.383-400, 1982.
DOI : 10.1145/800070.802214

T. Dierks and E. Rescorla, The Transport Layer Security (TLS) Protocol Version 1.2. IETF RFC 5246, 2008.

W. Diffie and M. Hellman, New directions in cryptography, IEEE Transactions on Information Theory, vol.22, issue.6, pp.644-654, 1976.
DOI : 10.1109/TIT.1976.1055638

W. Diffie, P. C. Van-oorschot, and M. J. Wiener, Authentication and authenticated key exchanges, Designs, Codes and Cryptography, vol.4, issue.3, pp.107-125, 1992.
DOI : 10.1007/BF00124891
URL : http://www.scs.carleton.ca/~paulv/papers/sts-final.pdf

D. Dolev and A. C. Yao, On the security of public key protocols, IEEE Transactions on Information Theory, vol.29, issue.2, pp.198-208, 1983.
DOI : 10.1109/TIT.1983.1056650

S. Escobar, C. Meadows, and J. Meseguer, A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties, Theoretical Computer Science, vol.367, issue.1-2, pp.1-2, 2006.
DOI : 10.1016/j.tcs.2006.08.035

C. Fournet and G. Gonthier, A hierarchy of equivalences for asynchronous calculi, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, pp.844-855, 1998.
DOI : 10.1007/BFb0055107

A. O. Freier, P. Karlton, and P. C. Kocher, The SSL Protocol: Version 3.0 Internet Draft available at http, 1996.

S. Goldwasser and M. Bellare, Lecture Notes on Cryptography Summer Course " Cryptography and Computer Security " at MIT, 1996.

S. Goldwasser and S. Micali, Probabilistic encryption, Journal of Computer and System Sciences, vol.28, issue.2, pp.270-299, 1984.
DOI : 10.1016/0022-0000(84)90070-9
URL : https://doi.org/10.1016/0022-0000(84)90070-9

S. Goldwasser, S. Micali, and R. Rivest, A Digital Signature Scheme Secure Against Adaptive Chosen-Message Attacks, SIAM Journal on Computing, vol.17, issue.2, pp.281-308, 1988.
DOI : 10.1137/0217017

A. Gordon and A. Jeffrey, Types and effects for asymmetric cryptographic protocols, Journal of Computer Security, vol.12, issue.3-4, pp.435-484, 2004.
DOI : 10.3233/JCS-2004-123-406

D. Hirschkoff, A full formalisation of ??-calculus theory in the calculus of constructions, Theorem Proving in Higher Order Logics, pp.153-169, 1997.
DOI : 10.1007/BFb0028392

K. Honda and N. Yoshida, On reduction-based process semantics, Theoretical Computer Science, vol.151, issue.2, pp.437-486, 1995.
DOI : 10.1016/0304-3975(95)00074-7
URL : https://doi.org/10.1016/0304-3975(95)00074-7

F. Honsell, M. Miculan, and I. Scagnetto, ??-calculus in (Co)inductive-type theory, Theoretical Computer Science, vol.253, issue.2, pp.239-285, 2001.
DOI : 10.1016/S0304-3975(00)00095-5
URL : https://doi.org/10.1016/s0304-3975(00)00095-5

T. Jager, F. Kohlar, S. Schäge, and J. Schwenk, On the Security of TLS-DHE in the Standard Model, CRYPTO 2012, pp.273-293, 2012.
DOI : 10.1007/978-3-642-32009-5_17

R. Kemmerer, C. Meadows, and J. Millen, Three systems for cryptographic protocol analysis, Journal of Cryptology, vol.7, issue.2, pp.79-130, 1994.
DOI : 10.1007/BF00197942

H. Krawczyk, SKEME: a versatile secure key exchange mechanism for Internet, Proceedings of Internet Society Symposium on Network and Distributed Systems Security, pp.114-127, 1996.
DOI : 10.1109/NDSS.1996.492418

H. Krawczyk, K. G. Paterson, and H. Wee, On the Security of the TLS Protocol: A Systematic Analysis, CRYPTO 2013, pp.429-448, 2013.
DOI : 10.1007/978-3-642-40041-4_24

S. Kremer and R. Künnemann, Automated Analysis of Security Protocols with Global State, IEEE Symposium on Security and Privacy, pp.163-178, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00955869

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

A. Lapadula, R. Pugliese, and F. Tiezzi, A Calculus for Orchestration of Web Services, Programming Languages and Systems, 16th European Symposium on Programming, pp.33-47, 2007.
DOI : 10.1007/978-3-540-71316-6_4

B. Liblit and A. Aiken, Type systems for distributed data structures, Proceedings of the 27th ACM Symposium on Principles of Programming Languages, pp.199-213, 2000.

P. Lincoln, J. Mitchell, M. Mitchell, and A. Scedrov, A probabilistic poly-time framework for protocol analysis, Proceedings of the 5th ACM conference on Computer and communications security , CCS '98, pp.112-121, 1998.
DOI : 10.1145/288090.288117

J. Liu, A Proof of Coincidence of Labeled Bisimilarity and Observational Equivalence in Applied Pi Calculus, 2011.

J. Liu and H. Lin, A complete symbolic bisimulation for full applied pi calculus, Theoretical Computer Science, vol.458, pp.76-112, 2012.
DOI : 10.1016/j.tcs.2012.07.034

G. Lowe, Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR, Tools and Algorithms for the Construction and Analysis of Systems, pp.147-166, 1996.
DOI : 10.1007/3-540-61042-1_43

R. Lucchi and M. Mazzara, A pi-calculus based semantics for WS-BPEL, The Journal of Logic and Algebraic Programming, vol.70, issue.1, pp.96-118, 2007.
DOI : 10.1016/j.jlap.2006.05.007

J. Martinho and A. Ravara, Encoding Cryptographic Primitives in a Calculus with Polyadic Synchronisation, Journal of Automated Reasoning, vol.33, issue.2, pp.3-4, 2011.
DOI : 10.1007/s002360050036

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

A. J. Menezes, P. C. Van-oorschot, and S. A. Vanstone, Handbook of Applied Cryptography, 1996.
DOI : 10.1201/9781439821916

J. Michael and . Merritt, Cryptographic Protocols, 1983.

R. Milner, Communication and Concurrency, 1989.

R. Milner, Functions as processes, Mathematical Structures in Computer Science, vol.4, issue.02, pp.119-141, 1992.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075405

R. Milner, Communicating and Mobile Systems: the ? -Calculus, 1999.

R. Milner and D. Sangiorgi, Barbed bisimulation, Automata, Languages and Programming: 19th International Colloquium Wien, Austria, pp.685-695, 1992.
DOI : 10.1007/3-540-55719-9_114

C. John and . Mitchell, Foundations for Programming Languages, 1996.

J. C. Mitchell, M. Mitchell, and U. Stern, Automated Analysis of Cryptographic Protocols Using Mur?, Proceedings of the 1997 IEEE Symposium on Security and Privacy, pp.141-151, 1997.

G. Kenneth, T. Paterson, T. Ristenpart, and . Shrimpton, Tag size does matter: Attacks and proofs for the TLS record protocol, ASIACRYPT, pp.372-389, 2011.

C. Lawrence and . Paulson, The Inductive Approach to Verifying Cryptographic Protocols, Journal of Computer Security, vol.6, issue.12, pp.85-128, 1998.

A. Pfitzmann and M. Köhntopp, Anonymity, Unobservability, and Pseudonymity ??? A Proposal for Terminology, International Workshop on Design Issues in Anonymity and Unobservability, pp.1-9, 2001.
DOI : 10.1007/3-540-44702-4_1

B. Pfitzmann, M. Schunter, and M. Waidner, Cryptographic Security of Reactive Systems, Electronic Notes in Theoretical Computer Science, vol.32, pp.59-77, 2000.
DOI : 10.1016/S1571-0661(04)00095-7

C. Benjamin, D. N. Pierce, and . Turner, Pict: A Programming Language Based on the Pi-Calculus, Proof, Language and Interaction: Essays in Honour of Robin Milner (Foundations of Computing), pp.455-494, 2000.

D. Mark, B. Ryan, and . Smyth, Applied pi calculus, Formal Models and Techniques for Analyzing Security Protocols, pp.112-142, 2011.

Y. A. Peter, S. A. Ryan, and . Schneider, An attack on a recursive authentication protocol. A cautionary tale, Inform. Process. Lett, vol.65, issue.1, pp.7-10, 1998.

D. Sangiorgi, Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms, 1993.

D. Sangiorgi, On the bisimulation proof method, Mathematical Structures in Computer Science, vol.8, issue.5, pp.447-479, 1998.
DOI : 10.1017/S0960129598002527

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

B. Schmidt, S. Meier, C. Cremers, and D. 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

S. Schneider, Security properties and CSP, Proceedings 1996 IEEE Symposium on Security and Privacy, pp.174-187, 1996.
DOI : 10.1109/SECPRI.1996.502680
URL : http://www.cs.rhbnc.ac.uk/research/formal/steve/papers/oakland96.ps.gz

B. Schneier, Applied Cryptography: Protocols, Algorithms, and Source Code in C, 1996.

G. Stuart, V. D. Stubblebine, and . Gligor, On Message Integrity in Cryptographic Protocols, Proceedings of the 1992 IEEE Symposium on Research in Security and Privacy, pp.85-104, 1992.

J. Thayer-fábrega, J. C. Herzog, and J. D. Guttman, Strand Spaces: Why is a Security Protocol Correct, Proceedings of the 1998 IEEE Symposium on Security and Privacy, pp.160-171, 1998.

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

M. Vanhoef and F. Piessens, All your biases belong to us: Breaking RC4 in WPA-TKIP and TLS, USENIX Security Symposium. USENIX, pp.97-112, 2015.

B. Victor, The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes, 1998.

H. Peter, F. R. Welch, and . Barnes, Communicating Mobile Processes: Introducing occam-pi. In Communicating Sequential Processes. The First 25 Years, Lecture Notes in Computer Science), vol.3525, pp.175-210, 2005.

L. Wischik and P. Gardner, Strong Bisimulation for the Explicit Fusion Calculus, Foundations of Software Science and Computation Structures 7th International Conference, pp.484-498, 2004.
DOI : 10.1007/978-3-540-24727-2_34

C. Andrew and . Yao, Theory and Applications of Trapdoor Functions, Proceedings of the 23rd Annual Symposium on Foundations of Computer Science (FOCS 82, pp.80-91, 1982.