M. Abadi and C. Fournet, Mobile values, new names, and secure communication, Proc. of the 28th ACM 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. Arapinis, V. Cheval, and S. Delaune, Composing Security Protocols: From Confidentiality to Privacy, Proceedings of the 4th International Conference on Principles of Security and Trust (POST'15), 2015.
DOI : 10.1007/978-3-662-46666-7_17

URL : http://arxiv.org/abs/1407.5444

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

B. Barak, R. Canetti, J. Buus-nielsen, and R. Pass, Universally Composable Protocols with Relaxed Set-Up Assumptions, 45th Annual IEEE Symposium on Foundations of Computer Science, pp.186-195, 2004.
DOI : 10.1109/FOCS.2004.71

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

F. Bohl and D. Unruh, Symbolic universal composability, Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium, CSF '13, pp.257-271, 2013.

A. Boldyreva, M. Fischlin, A. Palacio, and B. Warinschi, A Closer Look at PKI: Security and Efficiency, Public Key Cryptography -PKC 2007, 10th International Conference on Practice and Theory in Public- Key Cryptography Proceedings, pp.458-475, 2007.
DOI : 10.1007/978-3-540-71677-8_30

URL : http://www.cc.gatech.edu/~aboldyre/papers/pki.pdf

C. Boyd, C. Cremers, M. Feltz, K. G. Paterson, B. Poettering et al., ASICS: Authenticated Key Exchange Security Incorporating Certification Systems, Computer Security -ESORICS 2013 -18th European Symposium on Research in Computer Security Proceedings, pp.381-399, 2013.
DOI : 10.1007/978-3-642-40203-6_22

URL : http://eprint.iacr.org/2013/398.pdf

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, P. Nigel, B. Smart, . Warinschi et al., 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. C. 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

C. Brzuska, M. Fischlin, B. Warinschi, C. Stephen, and . 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

J. Camenisch, R. R. Enderlein, S. Krenn, R. Küsters, and D. Rausch, Universal Composition with Responsive Environments, Advances in Cryptology -ASIACRYPT 2016 -22nd International Conference on the Theory and Application of Cryptology and Information Security Proceedings, Part II, volume 10032 of Lecture Notes in Computer Science, pp.807-840, 2016.
DOI : 10.1007/978-3-319-11698-3_9

R. Canetti, Universally composable security: a new paradigm for cryptographic protocols, Proceedings 2001 IEEE International Conference on Cluster Computing, pp.14-17, 2001.
DOI : 10.1109/SFCS.2001.959888

URL : http://eprint.iacr.org/2000/067.pdf

R. Canetti, L. Cheung, D. Kirli-kaynar, M. Liskov, N. A. Lynch et al., Time-Bounded Task-PIOAs: A Framework for Analyzing Security Protocols, Lecture Notes in Computer Science, vol.4167, pp.238-253, 2006.
DOI : 10.1007/11864219_17

URL : http://www.dice.ucl.ac.be/~pereira/DISC06.pdf

V. Cheval, V. Cortier, and E. Le-morvan, Secure Refinements of Communication Channels, Prahladh Harsha and G. Ramalingam 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015), volume 45 of Leibniz International Proceedings in Informatics (LIPIcs) Schloss Dagstuhl?Leibniz-Zentrum fuer Informatik, pp.575-589
URL : https://hal.archives-ouvertes.fr/hal-01215265

S. ¸-tefan-ciobâc?-a and V. Cortier, Protocol composition for arbitrary primitives, Proceedings of the 23rd IEEE Computer Security Foundations Symposium (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-00157889

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

S. Delaune, S. Kremer, O. Pereira, and I. Kanpur, Simulation based security in the applied pi calculus, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2009 Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.169-180, 2009.

N. Dershowitz and J. Jouannaud, Rewrite Systems, pp.243-320, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

Y. Dodis, J. Katz, A. Smith, and S. Walfish, Composability and On-Line Deniability of Authentication, Proceedings of the 6th Theory of Cryptography Conference on Theory of Cryptography, TCC '09, pp.146-162, 2009.
DOI : 10.1007/978-3-540-24691-6_29

T. Gibson-robinson, A. Kamil, and G. Lowe, Verifying layered security protocols, Journal of Computer Security, vol.7, issue.2,3, p.2015
DOI : 10.3233/JCS-1999-72-304

D. Hofheinz, E. Kiltz, and V. Shoup, Practical Chosen Ciphertext Secure Encryption from Factoring, Journal of Cryptology, vol.26, issue.6, pp.102-118, 2013.
DOI : 10.1109/TIT.1980.1056264

URL : http://homepages.cwi.nl/~kiltz/papers/faccca.pdf

R. Kusters, Simulation-Based Security with Inexhaustible Interactive Turing Machines, 19th IEEE Computer Security Foundations Workshop (CSFW'06), pp.309-320, 2006.
DOI : 10.1109/CSFW.2006.30

URL : http://infsec.uni-trier.de/publications/paper/Kuesters-CSFW-2006.pdf

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

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, 2013.
DOI : 10.1007/978-3-642-39799-8_48

S. Moedersheim 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

B. Pfitzmann and M. Waidner, Composition and integrity preservation of secure reactive systems, Proceedings of the 7th ACM conference on Computer and communications security , CCS '00, pp.245-254, 2000.
DOI : 10.1145/352600.352639

T. Shrimpton, M. Stam, and B. Warinschi, A Modular Treatment of Cryptographic APIs: The Symmetric-Key Case, Annual Cryptology Conference, pp.277-307, 2016.
DOI : 10.1109/CSF.2016.27

A. Appendix, Some more examples A.1. Continuing Example