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.
URL : https://hal.archives-ouvertes.fr/hal-00918401

M. Arapinis, V. Cheval, and S. Delaune, Verifying privacy-type properties in a modular way, 25th IEEE Computer Security Foundations Symposium (CSF'12), pp.95-109, 2012.

, Composing security protocols: from confidentiality to privacy, 4th International Conference on Principles of Security and Trust, ser. Lecture Notes in Computer Science, vol.9036, pp.324-343, 2015.

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, ser. Lecture Notes in Computer, vol.9057, pp.689-718, 2015.

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., in Foundations of Security Analysis and Design VII, ser. Lecture Notes in Computer Science, vol.8604, pp.146-166, 2014.

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Computeraided security proofs for the working cryptographer, Advances in Cryptology-CRYPTO 2011, ser. Lecture Notes in Computer Science, P. Rogaway, vol.6841, pp.71-90, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01112075

M. Bellare, D. Pointcheval, and P. Rogaway, Authenticated key exchange secure against dictionary attacks, Advances in Cryptology-EUROCRYPT'00, ser. Lecture Notes in Computer Science, B. Preneel, vol.1807, pp.139-155, 2000.

M. Bellare and P. Rogaway, The security of triple encryption and a framework for code-based game-playing proofs, Advances in Cryptology-Eurocrypt, vol.4004, pp.409-426, 2006.

K. Bhargavan, B. Blanchet, and N. Kobeissi, Verified models and reference implementations for the TLS 1.3 standard candidate, IEEE Symposium on Security and Privacy (S&P'17), pp.483-503, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01575920

, Verified models and reference implementations for the TLS 1.3 standard candidate, 2017.

B. Blanchet, Computationally sound mechanized proofs of correspondence assertions, 20th IEEE Computer Security Foundations Symposium (CSF'07), vol.128, pp.97-111, 2007.

, A computationally sound mechanized prover for security protocols, IEEE Transactions on Dependable and Secure Computing, vol.5, issue.4, pp.193-207, 2008.

, Automatically verified mechanized proof of one-encryption key exchange, 25th IEEE Computer Security Foundations Symposium (CSF'12), pp.325-339, 2012.

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

, Composition theorems for CryptoVerif and application to TLS 1.3, 2018.

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.12, issue.4, pp.267-297, 2013.

C. Brzuska, M. Fischlin, B. Warinschi, and S. Williams, Composability of Bellare-Rogaway key exchange protocol, 18th ACM conference on Computer and communications security (CCS'11)

R. Canetti, Universally composable security: A new paradigm for cryptographic protocols, 42nd Symposium on Foundations of Computer Science (FOCS), pp.136-145, 2001.

R. Canetti and J. Herzog, Universally composable symbolic analysis of mutual authentication and key exchange protocols, Theory of Cryptography Conference (TCC'06), ser. Lecture Notes in Computer, vol.3876, pp.380-403, 2006.

R. Canetti and H. Krawczyk, Analysis of key-exchange protocols and their use for building secure channels, Advances in Cryptology-EUROCRYPT 2001, ser. Lecture Notes in Computer Science, B. Pfitzmann, vol.2045, pp.453-474, 2001.

R. Canetti and T. Rabin, Universal composition with joint state, Advances in Cryptology-CRYPTO 2003, ser. Lecture Notes in Computer Science, D. Boneh, vol.2729, pp.265-281, 2003.

S. ¸. and V. Cortier, Protocol composition for arbitrary primitives, 23rd IEEE Computer Security Foundations Symposium (CSF'10), pp.322-336, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00525781

V. Cortier and S. Delaune, Safely composing security protocols, Formal Methods in System Design, vol.34, issue.1, pp.1-36, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00157889

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.

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.

S. Delaune, S. Kremer, and O. Pereira, Simulation based security in the applied pi calculus, 29th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'09), ser. Leibniz International Proceedings in Informatics, vol.4, pp.169-180, 2009.

S. Delaune, S. Kremer, and M. D. Ryan, Composition of passwordbased protocols, 21st IEEE Computer Security Foundations Symposium (CSF'08), pp.239-251, 2008.
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, ACM Conference on Computer and Communications Security (CCS'15), pp.1197-1210, 2015.

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

M. Fischlin and F. Günther, Multi-stage key exchange and the case of Google's QUIC protocol, ACM SIGSAC Conference on Computer and Communications Security (CCS'14), pp.1193-1204, 2014.

T. Groß and S. Mödersheim, Vertical protocol composition, 24th IEEE Computer Security Foundations Symposium (CSF'11), pp.235-250, 2011.

J. D. Guttman and F. J. Fábrega, Protocol independence through disjoint encryption, 13th IEEE Computer Security Foundations Workshop (CSFW'00), pp.24-34, 2000.

R. Küsters and M. Tuengerthal, Composition theorems without preestablished session identifiers, 18th ACM Conference on Computer and Communications Security, pp.41-50, 2011.

S. Mödersheim and L. Viganò, Secure pseudonymous channels, Computer Security-ESORICS 2009: 14th European Symposium on Research in Computer Security, ser. Lecture Notes in Computer Science, vol.5789, pp.337-354, 2009.

, Sufficient conditions for vertical composition of security protocols, 9th ACM Symposium on Information, Computer and Communications Security (AsiaCCS'14), pp.435-446, 2014.

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

T. Y. Woo and S. S. Lam, A semantic model for authentication protocols, IEEE Symposium on Research in Security and Privacy, pp.178-194, 1993.