M. Abdalla, P. Fouque, and D. Pointcheval, Password-based authenticated key exchange in the three-party setting, IEE Proceedings - Information Security, vol.153, issue.1, pp.27-39, 2006.
DOI : 10.1049/ip-ifs:20055073

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

M. Arapinis, V. Cheval, and S. Delaune, Verifying Privacy-Type Properties in a Modular Way, 2012 IEEE 25th Computer Security Foundations Symposium, pp.95-109, 2012.
DOI : 10.1109/CSF.2012.16

M. Arapinis, V. Cheval, and S. Delaune, Composing Security Protocols: From Confidentiality to Privacy, LNCS, vol.9036, issue.15, pp.324-343, 2015.
DOI : 10.1007/978-3-662-46666-7_17

G. Barthe, J. M. Crespo, Y. Lakhnech, and B. Schmidt, Mind the Gap: Modular Machine-Checked Proofs of One-Round Key Exchange Protocols, Advances in Cryptology ? EUROCRYPT 2015, pp.689-718, 2015.
DOI : 10.1007/978-3-662-46803-6_23

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., EasyCrypt: A Tutorial, Foundations of Security Analysis and Design VII, pp.146-166, 2014.
DOI : 10.1145/1594834.1480894

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

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Computer-Aided Security Proofs for the Working Cryptographer, Advances in Cryptology ? CRYPTO 2011, pp.71-90, 2011.
DOI : 10.1007/978-3-642-22792-9_5

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

M. Bellare, D. Pointcheval, and P. Rogaway, Authenticated Key Exchange Secure against Dictionary Attacks, LNCS, vol.1807, issue.00, pp.139-155, 2000.
DOI : 10.1007/3-540-45539-6_11

URL : http://seclab.cs.ucdavis.edu/papers/Rogaway/dict.pdf

M. Bellare and P. Rogaway, The Security of Triple Encryption and a Framework??for??Code-Based??Game-Playing??Proofs, LNCS, vol.28, issue.4, pp.409-426, 2004.
DOI : 10.1002/j.1538-7305.1949.tb00928.x

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, B. Blanchet, and N. Kobeissi, Verified models and reference implementations for the TLS 1.3 standard candidate Available at https://hal.inria.fr/hal-01528752. CryptoVerif scripts available at https://github, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01575920

B. Blanchet, Computationally sound mechanized proofs of correspondence assertions Extended version available as ePrint Report, CSF'07, pp.97-111, 2007.

B. Blanchet, A Computationally Sound Mechanized Prover for Security Protocols, IEEE Transactions on Dependable and Secure Computing, vol.5, issue.4, pp.193-207, 2008.
DOI : 10.1109/TDSC.2007.1005

B. Blanchet, Automatically Verified Mechanized Proof of One-Encryption Key Exchange, 2012 IEEE 25th Computer Security Foundations Symposium, pp.325-339, 2012.
DOI : 10.1109/CSF.2012.8

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

B. Blanchet, CryptoVerif: A computationally-sound security protocol verifier, 2017.

C. Brzuska, M. Fischlin, N. P. Smart, B. Warinschi, and S. C. Williams, Less is more: relaxed yet composable security notions for key exchange, International Journal of Information Security, vol.23, issue.4, pp.267-297, 2013.
DOI : 10.1007/s00145-009-9052-3

URL : http://eprint.iacr.org/2012/242.pdf

C. Brzuska, M. Fischlin, B. Warinschi, and S. Williams, Composability of bellare-rogaway key exchange protocols, Proceedings of the 18th ACM conference on Computer and communications security, CCS '11, pp.51-62, 2011.
DOI : 10.1145/2046707.2046716

R. Canetti, Universally composable security: A new paradigm for cryptographic protocols An updated version is available at Cryptology ePrint Archive, FOCS'01, pp.136-145067, 2000.

R. Canetti and J. Herzog, Universally Composable Symbolic Analysis of Mutual Authentication and Key-Exchange Protocols, LNCS, vol.3876334, issue.06, pp.380-403, 2004.
DOI : 10.1007/11681878_20

R. Canetti and H. Krawczyk, Analysis of key-exchange protocols and their use for building secure channels Long version at https://ia, LNCS, vol.2045, issue.01, pp.453-474040, 2001.

R. Canetti and T. Rabin, Universal Composition with Joint State, Crypto'03, pp.265-281, 2003.
DOI : 10.1007/978-3-540-45146-4_16

URL : http://eprint.iacr.org/2002/047.ps.gz

?. Ciobâc? and V. Cortier, Protocol composition for arbitrary primitives, CSF'10, pp.322-336, 2010.

V. Cortier and S. Delaune, Safely composing security protocols. Formal Methods in System Design, pp.1-36, 2009.
DOI : 10.1007/978-3-540-77050-3_29

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

A. Datta, A. Derek, J. C. Mitchell, and A. Roy, Protocol Composition Logic (PCL), Electronic Notes in Theoretical Computer Science, vol.172, pp.311-358, 2007.
DOI : 10.1016/j.entcs.2007.02.012

URL : https://doi.org/10.1016/j.entcs.2007.02.012

A. Datta, A. Derek, J. C. Mitchell, and B. Warinschi, Computationally Sound Compositional Logic for Key Exchange Protocols, 19th IEEE Computer Security Foundations Workshop (CSFW'06), pp.321-334, 2006.
DOI : 10.1109/CSFW.2006.9

S. Delaune, S. Kremer, and O. Pereira, Simulation based security in the applied pi calculus, FSTTCS'09 of Leibniz International Proceedings in Informatics Leibniz-Zentrum für Informatik, pp.169-180, 2009.

S. Delaune, S. Kremer, and M. D. Ryan, Composition of Password-Based Protocols, 2008 21st IEEE Computer Security Foundations Symposium, pp.239-251, 2008.
DOI : 10.1109/CSF.2008.6

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

B. Dowling, M. Fischlin, F. Günther, and D. Stebila, A cryptographic analysis of the TLS 1.3 handshake protocol candidates Full version available at https://ia, CCS'15, pp.1197-1210, 2015.

B. Dowling, M. Fischlin, F. Günther, and D. Stebila, A cryptographic analysis of the TLS 1.3 draft-10 full and pre-shared key handshake protocol, Cryptology ePrint Archive, p.81, 2016.

M. Fischlin and F. Günther, Multi-Stage Key Exchange and the Case of Google's QUIC Protocol, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS '14, pp.1193-1204, 2014.
DOI : 10.1145/2660267.2660308

T. Groß and S. Mödersheim, Vertical protocol composition, CSF'11, pp.235-250, 2011.

J. D. Guttman and F. J. Fábrega, Protocol independence through disjoint encryption, Proceedings 13th IEEE Computer Security Foundations Workshop. CSFW-13, pp.24-34, 2000.
DOI : 10.1109/CSFW.2000.856923

R. Küsters and M. Tuengerthal, Composition theorems without pre-established session identifiers, Proceedings of the 18th ACM conference on Computer and communications security, CCS '11, pp.41-50, 2011.
DOI : 10.1145/2046707.2046715

S. Mödersheim and L. Viganò, Secure Pseudonymous Channels, ESORICS'09, pp.337-354, 2009.
DOI : 10.1007/978-3-540-75227-1_6

S. Mödersheim and L. Viganò, Sufficient conditions for vertical composition of security protocols, Proceedings of the 9th ACM symposium on Information, computer and communications security, ASIA CCS '14, pp.435-446, 2014.
DOI : 10.1145/2590296.2590330

E. Rescorla, The Transport Layer Security (TLS) protocol version 1.3, draft-ietf-tls-tls13-28, 2018.

V. Shoup, Sequences of games: a tool for taming complexity in security proofs, Cryptology ePrint Archive Report, vol.332332, 2004.

T. Y. Woo and S. S. Lam, A semantic model for authentication protocols, Proceedings 1993 IEEE Computer Society Symposium on Research in Security and Privacy, pp.178-194, 1993.
DOI : 10.1109/RISP.1993.287633